Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Manually using a SideKick parser


view this post on Zulip 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.

view this post on Zulip 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: Sep 25 2021 at 09:17 UTC