[isabelle-dev] NEWS: more PIDE structure parsing

Makarius makarius at sketis.net
Fri Aug 5 19:36:45 CEST 2016


*** Prover IDE -- Isabelle/Scala/jEdit ***

* Isabelle/ML and Standard ML files are presented in Sidekick with the
tree structure of section headings: this special comment format is
described in "implementation" chapter 0, e.g. (*** section ***).

* Refined folding mode "isabelle" based on Isar syntax: 'next' and 'qed'
are treated as delimiters for fold structure; 'begin' and 'end'
structure of theory specifications is treated as well.

* Sidekick parser "isabelle-context" shows nesting of context blocks
according to 'begin' and 'end' structure.


This refers to current Isabelle/1555dc12cfb6. It is a continuation of
more formal treatment of sources, with text folds, tree views, and
indentation.

Note that Sidekick plugin options can make the parser persistent for a
given mode, e.g. "isabelle" (document sections) vs. "isabelle-context"
(context blocks) for theory files (mode "isabelle").


	Makarius


More information about the isabelle-dev mailing list