[isabelle-dev] NEWS: abbrevs and symbols dockable

[Makarius]

*** 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