[isabelle-dev] new isabelle interface

[Makarius]

On Mon, 25 Aug 2008, Cameron Freer wrote:

> One can type a single command from the SAGE commandline to spawn a local 
> webserver running the notebook interface.  I've found the AJAX interface 
> to be surprisingly clean, responsive, and pleasant, even for those used 
> to the commandline.  Such a web interface for Isabelle would probably be 
> more complicated, but it does offer similar advantages -- not just the 
> ability to separate the kernel from the UI, but also portability (for 
> users running it locally).
> 
> Kaliszyk proposed something similar for Coq a couple years ago: 
> http://www.easychair.org/FLoC-06/UITP-preproceedings.pdf#page=57

Very good.  Cezary Kaliszyk is actually one of the prover UI people who 
greatly influenced the upcoming Isabelle architecture.  Cezary has quite 
responsive AJAX / JavaScript on the client side, but on the server his own 
OCaml wrapper around the prover, which exposes a couple of problems.  The 
latter can be easily replaced by a more robust version using the new Scala 
classes of Isabelle, using existing server tools available for the JVM.

If there are any AJAX experts out there who would like to produce an 
interface to our (slowly emerging) server infrastructure, I would be happy 
to assist them.


	Makarius