Re: [isabelle] Isabelle2018-RC0 sometimes sluggish behavior of JEdit



On 18/06/18 18:22, Eugene W. Stark wrote:
> 
> I sometimes open a new "Plain View"
> to examine one part of the code while editing another in the main window.  If the
> portion of the code shown in the new view is a bit beyond the portion being edited,
> then due to continuous checking changes made in the main window force the re-checking
> of the code up through the portion shown in the new view.  This is to be expected.
> However, I am wondering right now if somehow when I "close" the extra view and go
> back to working only with the main window, it is somehow the case that the extra view
> is not deleted, but just becomes invisible and its presence is still causing the
> extra checking to be done.  If so, that would explain the sluggish behavior.
> 
> I realized that I might be able to test this by turning off continuous checking to
> see if that relieved the sluggish behavior, but in Isabelle2018-RC0 the "continuous'
> checking" box is no longer where I remembered it to be and I don't know how to find
> this option setting quickly now.

The check box is still in the Theories panel as before.

You can also use the Console/Scala plugin to query the information
underlying the "PIDE document node perspective". E.g. like this:

(1) jEdit information:

JEdit_Lib.jedit_text_areas(view.getBuffer).foreach(println)


(2) PIDE information:

val view_ranges = GUI_Thread.future { val model =
Document_Model.get(view.getBuffer).get;
model.document_view_ranges(model.snapshot()) }

view_ranges
res2: isabelle.Future[List[isabelle.Text.Range]] = List([0..530],
[1363..1771])

There needs to be some elapsed time between defining view_ranges and
printing it once again on the toplevel.


I have experimented with this and some plain view -- it looks fine so far.


Also note that there is further complexity if you have "auxiliary
files", e.g. 'ML_file' commands in theories being edited.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.