[isabelle-dev] NEWS: fundamental PIDE GUI changes

Makarius makarius at sketis.net
Mon Dec 7 16:33:56 CET 2015


This is a summary of some fundamental changes in the dynamics PIDE edits 
and GUI updates, according to current Isabelle/ba051060d46b:


* Improved scheduling for urgent print tasks (e.g. command state output,
interactive queries) wrt. long-running background tasks.

* The State panel manages explicit proof state output, with dynamic
auto-update according to cursor movement. Alternatively, the jEdit
action "isabelle.update-state" (shortcut S+ENTER) triggers manual
update.

* The Output panel no longer shows proof state output by default, to
avoid GUI overcrowding. INCOMPATIBILITY, use the State panel instead or
enable option "editor_output_state".

* The text overview column (status of errors, warnings etc.) is updated
asynchronously, leading to much better editor reactivity. Moreover, the
full document node content is taken into account. The width of the
column is scaled according to the main text area font, for improved
visibility.

* The main text area no longer changes its color hue in outdated
situations. The text overview column takes over the role to indicate
unfinished edits in the PIDE pipeline. This avoids flashing text display
due to ad-hoc updates by auxiliary GUI components, such as the State
panel.



After so many years of PIDE, these changes are quite substantial. It is 
important to look carefully how this now works, and report remaining 
problems.

Last week I had a two-day Isabelle course at Univ. Bonn with 15 students 
of mathematics, and it all worked quite smoothly.  That does not prove the 
absence of counter-examples, though.


 	Makarius


More information about the isabelle-dev mailing list