*** 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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
