[isabelle-dev] NEWS: Improved completion mechanism
Christian Sternagel
c.sternagel at gmail.com
Fri Sep 6 10:20:26 CEST 2013
On 09/04/2013 02:24 AM, Makarius wrote:
> 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.
I could reproduce the issue with both minor modes you mention.
>
> * 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.
Also with editor_input_delay = 1000, I could reproduce it in a few seconds.
cheers
chris
More information about the isabelle-dev
mailing list