Re: [isabelle] Comparing Isabelle/Scala with scala-isabelle. Was: Isabelle code for getting in-memory representation (abstract syntax trees) for complete theory file (tree of loaded theories)

On 09/02/2021 20:33, Makarius wrote:
> The proper way is to define Isabelle/Isar commands in Isabelle/ML, and let the
> Isabelle/Scala front-end work in a high-level way with it.
> Chapter 4 of the "system" manual describes a fairly simple and declarative
> server protocol to work with Isabelle documents: the socket-version works via
> JSON (e.g. for Python), but it is easier to work with the same in
> Isabelle/Scala (the Headless PIDE session).

Some further side-remarks specifically for Isabelle2021 (see NEWS):

* General support for Isabelle/Scala system services, configured via the
shell function "isabelle_scala_service" in etc/settings (e.g. of an
Isabelle component); see implementations of class
Isabelle_System.Service in Isabelle/Scala. This supersedes former
"isabelle_scala_tools" and "isabelle_file_format": minor

Various examples may be found by using Isabelle/jEdit hypersearch for the text
"isabelle_scala_service" within all "settings" files in the $ISABELLE_HOME
directory (and all subdirectories).

An alternative is to search for class instances of "Isabelle_System.Service"
in *.scala files within $ISABELLE_HOME.

As an abstract example, a user-defined Isabelle/Scala module could register
its own command-line tools or Isabelle server commands (for JSON access). The
Scala implementation does the main system integration; if some mathematical
logic is required, it will be done in an auxiliary theory context for the tool
(e.g. embedded ML files to define Isar commands).

As a concrete example, consider Isabelle/Naproche in Isabelle2021-RC5. Follow
the Documentation pointer to $ISABELLE_NAPROCHE/Ex.thy --- it contains some
hints about the implementation at the bottom. Apart from Isabelle/ML and
Isabelle/Scala, this involves another program implemented in Haskell. The
latter uses Isabelle/Haskell library for basic communication with
Isabelle/PIDE (even with properly checked antiquotations instead of freely
invented string literals).


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.