From: MACKENZIE Carlin <firstname.lastname@example.org>
I would like to run a parser, say "isabelle-context", from isabelle_sidekick.scala on a theory file and examine the output. Could someone advise on how to do this? I'm not sure where to look for an example call in the code
The University of Edinburgh
The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
From: Makarius <email@example.com>
What do you mean by "examine the output"? Should the Prover IDE show it to the
user, or a Scala program of yours work with it?
If you just want to experiment with Isabelle/Scala snippets, you can do it in
the jEdit plugin "Console", sub-plugin "Scala": it is a REPL of the Scala
interpreter running on the JVM of Isabelle/jEdit with access to the name space
of the running application.
Here is an example derived from the Sidekick parser for "isabelle-context"
--- it assumes that the active editor buffer shows a proper theory, e.g.
src/HOL/ex/Seq.thy from the Documentation panel:
scala> val buffer = view.getBuffer
buffer: org.gjt.sp.jedit.Buffer = Seq.thy ($ISABELLE_HOME/src/HOL/ex/)
scala> val name = PIDE.resources.theory_node_name(buffer).get
name: isabelle.Document.Node.Name = HOL-ex.Seq
scala> val syntax = Isabelle.buffer_syntax(buffer).get
syntax: isabelle.Outer_Syntax =
scala> val structure = Document_Structure.parse_blocks(syntax, name,
structure: List[isabelle.Document_Structure.Document] =
List(Atom(60), Atom(26), Atom(2), Block(theory,theory Seq
This assumes a basic understanding of concepts defined in
Isabelle/Scala/jEdit. To help with that, you can explore the whole project
with the static semantics in IntelliJ IDEA: see also the "system" manual
section 5.5. about "isabelle scala_project".
Last updated: Sep 25 2021 at 09:17 UTC