* Improved completion based on context information about embedded
languages: keywords are only completed for outer syntax, symbols for
languages that support them. E.g. no symbol completion for ML source,
but within ML strings, comments, antiquotations.
This refers to Isabelle/5ff4742f27ec. No more accidental symbol
completion of "fn x => x" in ML! (Many years ago someone proposed an
opportunistic change the ML syntax to avoid this annoyance). Similar for
Isabelle document sources, with latex macros etc. Consequently the option
jedit_completion_immediate may be used more aggresively.
One snag is remaining: \foo within a string literal is malformed, and the
language context is lost. Thus it becomes hard to use backslash
completions within ML strings, for example. The Symbols panel always
works as fall-back, indepently of the language context.
As usual, I am dependent on early adopters to point out other problems
that I did not see myself. As the one who implements interaction schemes,
I am biased to a way of working that works, not one that fails (or hangs).
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
