On Tue, 29 Apr 2014, Thomas Sewell wrote:
I tried an adjustment a while ago in which I had the goal state print
incrementally. Even if some of the subgoals took a while to print, you'd
see the line with "goal (12 subgoals)" immediately, and then the
subgoals as they were formatted. The short summary is that this helped a
little sometimes, but I often still saw an empty Output panel for
seconds after moving the cursor to a line that the continuous checker
had already processed.
I strongly suspect that the print request was waiting in a queue
somewhere. The system would become responsive again once it finished
doing something else.
That is the normal future task farm, with its restricted worker thread
pool. All PIDE execution works via some Future.fork, with different
priorities in the queue. Proof tasks have low priority, print tasks have
high priority. Once a task is running on some thread, it continues and
cannot be preempted by newer tasks with higher priority.
The basic assumption is that each proof task does not run too long, and if
it does it is something to be improved in the application to make it more
smooth. In contrast, Proof General makes it more easy to produce huge and
heavy proof scripts that can be hardly handled by anyone else later.
On incremental printing: it's easy to implement by generalising a couple
of the relevant Pretty operations to produce a Seq.seq internally rather
than a list.
That would probably violate some implicit assumptions about print modes,
which are a slightly odd intrusion into the purity of Pretty.T.
What was the reason for incremental printing anyway? Just performance for
huge goal states? There are other bottle-necks concerning that, and if
goals really do get that big one should think about other ways to expose
them, not by "printing" in the old-fashioned way.
Incrementality might have other reasons and actual benefits. In the early
years of PIDE I had more ambitions for that, but it caused so many
additional problems in the document model and the GUI that I removed most
of it for the sake of delivering something that is sufficiently stable to
be usable in practice.
It looked promising initially, but then became really annoying, because
Isabelle/jEdit or PIDE resets the Output buffer each time it gets more
to display. So if you scroll down to look for something, you get
scrolled back up for each time a subgoal prints, which can give the
sensation that the editor is fighting you.
There is a deeper conceptual problem here. Several independent entities
want to update content of some GUI component: output window, tree view
etc. This requires a "merge" of these change of the GUI state, but that
is usually only done by a hard reset on one side, ignoring the other side.
You can see that in jEdit's SideKick tree view, Isabelle/jEdit's Output
dockable with scrollbar and folds, or even just in a plain Terminal with
the scrollbar.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
