[isabelle-dev] Grouping of Isabelle Symbols

[Makarius]

On Wed, 21 Nov 2012, Christian Sternagel wrote:

> Is there a plan to make the grouping of changeset 0226d408058b available in 
> Isabelle/Scala through isabelle.Symbol?

It is available as isabelle.Symbol.groups, as can be seen in the parent 
changeset a96bd08258a2.

Meta-note 1: When preparing a linear list of changesets to be pushed, 
there cannot get anything in between later, by construction of Mercurial. 
So the author can assume that the reader will always see this small linear 
segment.  So one can build them semantically on top of each other, without 
saying "see <parent id>" all the time.

Meta-note 2: I've split the changesets into two, because we don't have 
this principle that "features" and "changesets" correspond.  An insider 
joke by Florian Haftmann says, said "a single changeset does not make any 
sense".  I.e. it is agnostic, or rather modular in a historic sense, 
sitting there happily in a locally self-contained way within a larger 
historical context.  "Features" that are delivered to end-users then 
emerge as a limit-construction over many changesets, and are finally 
announced in NEWS.


> I could make use of it in the Symbols.bsh macro of
>
>  https://isabelle.in.tum.de/community/Extending_Isabelle/jEdit
>
> cheers
>
> chris
>
> PS: Is it possible to somehow use Scala when writing jEdit macros?

Good question.

jEdit uses Beanshell both for macros and system integration (gluing 
plugins together).  Thus it has access to the JVM name space in the Java 
way, but that is often insufficient for Scala with all its extra JVM stuff 
generated by the compiler.  It is not feasible to make Isabelle/Scala 
interfaces accessible by Java by default, only in special situations where 
there is no other way.


 	Makarius