*** 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
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").
isabelle-dev mailing list