*** Prover IDE -- Isabelle/Scala/jEdit *** * Dockable window "Symbols" also provides access to 'abbrevs' from the outer syntax of the current theory buffer. This provides clickable syntax templates, including entries with empty abbrevs name (which are inaccessible via keyboard completion).
* Additional abbreviations for syntactic completion may be specified within the theory header as 'abbrevs'. The theory syntax for 'keywords' has been simplified accordingly: optional abbrevs need to go into the new 'abbrevs' section. * Global abbreviations via $ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs are no longer supported. Minor INCOMPATIBILITY, use 'abbrevs' within theory header instead. This refers to Isabelle/2683c3be36eb (and AFP/88ebc309096a). Examples for abbrevs within theory headers are here: src/HOL/Nonstandard_Analysis/HLim.thy src/HOL/Nonstandard_Analysis/HSEQ.thy AFP/thys/HereditarilyFinite/HF.thy After importing such theories, the "Symbols" dockable will update its "Abbrevs" tab dynamically, according to the buffer syntax. (I have also added an event handler for the global font size, and re-unified the symbol GUI rendering with the completion popup.) With this convenient way to provide input methods (i.e. keyboard completion or clickable buttons) via regular theory libraries, we can become more ambitious with fancy notation -- in only *one* version with the full glory of symbols, sub-/superscripts, bold, bells, whistles. A still open problem is how to input the place holder character (ASCII bell) for templates in specifications of 'abbrevs'. Right now it can be copied from the 'abbrevs' section of src/Pure/Pure.thy or produced via the following BeanShell snippet: buffer.insert(textArea.getCaretPosition(), "\u0007") Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev