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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
