Julin Shaji (Feb 12 2025 at 15:44): Julin Shaji (Feb 12 2025 at 15:44):What is \<open> used for in isabelle?
Is it to aid some sort of literate source files that will be formatted differently when exported to html?
Julin Shaji (Feb 12 2025 at 15:46):For example, section \<open>Network model\<close> from
https://gist.github.com/ept/b6872fc541a68a321a26198b53b3896b
Fabian Huch (Feb 12 2025 at 15:56):It is just a delimiter
Mathias Fleury (Feb 12 2025 at 17:20):It looks like ‹ ...› if you visualize it in Isabelle/jEdit (and you should instead of reading gists)
Julin Shaji (Feb 13 2025 at 16:43):I saw in a youtube video (forgot which one) where they were typing ‹ without fully typing in \<open>. Is there a short way of typing that?
John Hughes (Feb 13 2025 at 17:20):Finally a question I can answer!
In jEdit , type a double-quote and pause briefly. A menu will pop up, with the (probably) first option looking like
<[]> (template)
where the double-brackets are really a box, and the angle-brackets are actually smaller ones. That first option will be highlighted. Pressing "tab" causes an open-close pair of exactly the kind you want to appear:
image.png
with your cursor positioned so that your subsequent typing appears within them.
If that option isn't the first one, you can use arrow keys to move down and then press tab. If you do this a few times, the option will soon move to the top of the list, and you'll be in the world of instant cartouches. Well..nearly instant; you still have to wait just a moment for the popup to appear.
Jan van Brügge (Feb 13 2025 at 18:52):You can also set completion delay to zero in the jedit settings, then you do not have to wait
Julin Shaji (Feb 14 2025 at 04:46):John Hughes said:
In jEdit , type a double-quote and pause briefly. A menu will pop up, with the (probably) first option looking like
Thanks! This is what I was looking for.
Julin Shaji (Feb 14 2025 at 04:52):So cartouche means the special symbols?
Mathias Fleury (Feb 14 2025 at 05:09):Makarius names those symbol cartouches
Last updated: Mar 09 2025 at 12:28 UTC