[isabelle] replace "isabelle tty"



We did not engage for "Remaining uses of Proof General" because we hope for easy ways to replace "isabelle tty" in our prototype, and because we look forward to replace our self-made front-end by Isabelle/jEdit as soon as Isabelle goes collaboration and includes session management.

Until Isabelle2013-2, our prototype had the communication between its front-end (client) in Java and its mathematics-engine (server) in Isabelle/ML via stdin/stdout of the server process:

(a) Java started the server by
     "isabelle tty -l Isac"
(b) the first text line written to stdin was
     "theory TTY_Communication imports Build_Isac begin"
(c) the client requests were ML functions   f : a1 -> .. -> an -> unit
     written to stdin as text "ML {* f a1 .. an *}"
(d) the functions f wrote data in XML-format, which was read from stdout
     by a Java XML parser.

We want to invest into replacement of this outdated communication the more, the closer Isabelle comes to a session management. So presently our questions are

(1) Is the code around the removed "isabelle tty" already stable enough to start replacement of "isabelle tty" in our project now ? (2) If "yes", what are the options to replace the above (a..d) "isabelle tty" communication in our prototype ? Where should we start to look to in the Isabelle code ?

We are aware, that the above questions are at the borderline of this mailing list's scope --- so we are really grateful for any help!

Walther

[1] http://www.ist.tugraz.at/isac




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