[isabelle-dev] NEWS: Improved completion based on context information

Makarius makarius at sketis.net
Fri Feb 21 17:51:12 CET 2014


* 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


More information about the isabelle-dev mailing list