Anthony Bordg (Jul 03 2019 at 21:54): Anthony Bordg (Jul 03 2019 at 21:54):Note the Query feature at the bottom of the Isabelle jEdit user interface. If you mouse over the Find window, it tells you how to search through the library. Of course, you can also browse the html files of the libraries in Isabelle/HOL.
Anthony Bordg (Jul 05 2019 at 08:03):I continue my series for newcomers.
Isabelle allows a rich syntactic sugar in your code. Just click on Symbols at the bottom of the user interface, and then click on one of the many categories of symbols available.
Anthony Bordg (Jul 05 2019 at 08:24):If you need to replace a name (of a definition, lemma ...) with a new one, you can change all the occurrences at once. Just open the Search menu, then the Find menu, in the Search and Replace interface enter the current name in the Search for window, the new name in the Replace with window, check the Whole word option, and finally click on Replace All.
Anthony Bordg (Jul 05 2019 at 08:39):In a file, if you mouse over any definition, lemma, tactic or keyword used in this file, while you press the cmd key, then you will be redirected towards its specification in the library. It's very useful when names are not completely self-explanatory.
Josh Chen (Jul 05 2019 at 08:48):In a file, if you mouse over any definition, lemma, tactic or keyword used in this file, while you press the cmd key, then you will be redirected towards its specification in the library. It's very useful when names are not completely self-explanatory.
(For newcomers:) Note that this only works if the file is available for processing; in particular, it won't work on source files of the session you're currently working in.
Anthony Bordg (Jul 05 2019 at 08:52):If you want to rename all the occurrences of a bound variable in a statement, click on the variable name then press the combination cmd + shift + return (the color of the occurrences will change) and enter the new name. It's useful for instance when isabelle generates a subgoal containing a bound variable whose name clashes with a previous variable in the current context.
Anthony Bordg (Jul 05 2019 at 09:01):I encourage everyone to share their tips.
Anthony Bordg (Jul 05 2019 at 21:59):An additional tip: if you highlight some code before opening the Search menu, then the Search for window will be already filled with this code, so you don't even need to copy/paste.
Anthony Bordg (Jul 06 2019 at 09:22):If you're a newcomer, you should be aware of the colours code :rainbow: displayed in Isabelle. In addition to error messages, the colours displayed give useful clues to understand errors or more generally to understand what is going on in Isabelle.
Open the menus Plugins, Plugin Options, Rendering to see the colours code.
Also, one can have a look at this stackoverflow question and the answer provided: What do colour codes mean in Isabelle/jEdit ?.
Kevin Kappelmann (Oct 09 2019 at 15:14):Is there already or can I define a shortcut in jEdit that achieves the same result as performing CTRL+Click on an object?
Last updated: Apr 19 2024 at 08:19 UTC