[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