Email Gateway (Nov 18 2020 at 12:29): Email Gateway (Nov 18 2020 at 12:29):From: MACKENZIE Carlin <s1724780@sms.ed.ac.uk>
Dear all,
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
Thank you,
Carlin MacKenzie
The University of Edinburgh
The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
Email Gateway (Nov 19 2020 at 11:47):From: Makarius <makarius@sketis.net>
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"
https://isabelle.sketis.net/repos/isabelle/file/Isabelle2020/src/Tools/jEdit/src/isabelle_sidekick.scala#l153
--- 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 =
keywords
...
scala> val structure = Document_Structure.parse_blocks(syntax, name,
buffer.getText(0, buffer.getLength))
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".
Makarius
Last updated: Jan 04 2025 at 20:18 UTC