[isabelle-dev] NEWS: Improved completion mechanism
makarius at sketis.net
Tue Sep 3 19:24:50 CEST 2013
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.
More information about the isabelle-dev