[isabelle-dev] NEWS: completion of explicit symbols

[Makarius]

*** Prover IDE -- Isabelle/Scala/jEdit ***

* Completion of symbols via prefix of \<name> or \<^name> or \name is
always possible, independently of the language context. It is never
implicit: a popup will show up unconditionally.


This refers to Isabelle/1ca11ddfcc70, but the later change 15952a05133c is 
also relevant.

There have been recent changes to allow control symbols in situations that 
were just plain-text before.  E.g. \<^item>, \<^medskip> in document 
source, or \<^undefined> in ML.  So the old policy to have symbols 
strictly on or off in the language context did no longer fit.

The change reduces surprise of immediate replacement of an unclear prefix 
of e.g. \alpha, leaving some verbatim suffix of it in the text.

Moreover, backslash sequences in e.g. @{term "..."} are now robust, 
because the change of language context in error situations does not affect 
the potential of completion.


 	Makarius