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

[Makarius]

On Fri, 21 Feb 2014, Makarius wrote:

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

This is gradually improving further, now at Isabelle/945ad7eaf37f. 
Notably:

   * "`" produces a completion popup for a text cartouche, even though it
     remains to be seen where it gets actually used apart from the @{rail}
     antiquotation.

   * "@{" completes to a closed antiquotation with the caret at the proper
     spot to continue.  Proof General users may have to unlearn C-c C-a C-a
     and get used to clear text completion (with semantic language
     context).

Moreover:

   * Semantic completion, based on failed name space lookups produced by
     the prover.  E.g. after typing

       ML {* @{t} *}

     with the curser touching the "t", there will be a red box to indicate
     the possibility to use explicit C+b completion from this semantic
     information.

This works for all newer mechanisms that use Name_Space.check, instead of 
the old form Name_Space.intern followed by manual table lookup. 
Unfortunately, the most interesting name space, the one of facts, is still 
a bit convoluted, and I need to find ways to retrofit it into that model. 
(As usual the actual mechanism is easier to implement, than working 
through thick sediments of slight oddities in the system to make it all 
work in practice.)


 	Makarius