[isabelle-dev] NEWS: Improved completion mechanism

[Makarius]

On Tue, 3 Sep 2013, Christian Sternagel wrote:

> Just for the record: the above mentioned hand also sometimes happens 
> when typing V ... E ... R ... Y ... slowly ;). It is just more frequent 
> when typing faster (mainly because a hang only ever happens directly 
> after having pressed a key).

OK, a few more hints what can be done right now.

For practical use, you can try with the Isabelle/Scala option 
jedit_completion = false (via Plugin Options / Completion / Completion). 
This means there won't be any automatic popup or immdediate replacement 
anymore, just explicit C+b completion.

Moreover, to pin down the problem:

   * Try with the "minor modes" of Isabelle/jEdit, e.g. the NEWS file (via 
Documentation panel), or ~~/etc/options or some session ROOT file. 
Completion works there as well, according to the syntax of these files. 
Note that NEWS only completes on symbols, e.g. \forall.  See also 
~~/src/Tools/jEdit/src/isabelle.scala for the basic wiring of all isabelle 
modes for jEdit.

   * Try with the major "isabelle" mode, but with PIDE edits switched 
de-facto off, by setting editor_input_delay to a very high value (in 
seconds).  Thus the document model pipeline will not interfere with 
physical text buffer editing.


 	Makarius