Re: [isabelle] replace "isabelle tty"

Hi Lars,

with great interest I studied your code [1] (cited below), followed the function calls into ~~/src/Pure/System, ~~/src/Pure/PIDE etc and tried to understand.

So far I understood, that
(1) Session.protocol_handler starts a persistent session
(2) Isabelle_Process.protocol_command takes a string list, interpretes the strings, accordingly executes a predefined collection of ML functions and returns results as strings.

However, I could not yet find out, how to use isabelle_process or the isabelle wrapper (or what else?) to feed the strings such that they drive (1) and (2).

Could you, please, help once more?


On 14-11-18 05:24 PM, Lars Hupel wrote:
On 14-11-18 06:31 PM, Walther Neuper wrote:
thanks a lot for the quick replies!

(1) Is the code around the removed "isabelle tty" already stable enough
to start replacement of "isabelle tty" in our project now ?
I would say yes, even though a canonical discipline on how to write an
application using only a minimal subset of the features of PIDE has not
emerged yet.
Very good. so let's start.
(d) the functions f wrote data in XML-format, which was read from
stdout by a Java XML parser.
firstly, I'm going to assume that your front end is running on the JVM.
Our protocol is very primitive, it is NOT asynchronous:
(c) the client requests were ML functions   f : a1 -> .. -> an -> unit
      written to stdin as text "ML {* f a1 .. an *}"
This is more interesting. Is the scope of what these functions do
limited, or can the user somehow specify arbitrary functions?
The set of functions f is fixed and cannot be expanded by the user,

If the scope is limited, then you can do something like [1] and treat
the prover process as some sort of "REPL" which only understands a fixed
set of commands and acts accordingly. Notably, the support of multiple
clients in a single Isabelle session is almost trivial.
The other relevant bit in the code I wrote at EPFL is [2], although it
is cluttered with rather ad hoc session management required by the
system I was integrating with. If you're inclined, I can put together a
smaller example which should be sufficient to demonstrate the general
So I'll go to study [1,2].
My hope is still, to stay within Java, because you say
The only guarantee is calling Java from Scala, and even that
breaks from time to time because of mismatches between their type systems.

Thanks a lot,


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