[isabelle-dev] new isabelle interface

[Chris Capel]

Hi all,

I'm thinking about making a new interface to Isabelle, along the lines
of Proof General, but not requiring Emacs (ugh). It would be done in
C# and be for Windows initially, though depending on how I do it it
could probably be made to work in Linux and other Unixen as well.

First of all, is there anything done already along these lines?

I plan to use SML.NET to compile Isabelle. Does anyone forsee any
problems with this? Is Isabelle's code fairly portable across Standard
ML compilers?

Besides what's in the source distribution, is there any internals
documentation I should know about?

Is there much in Isabelle that's Unix-specific that I'd need to port?
If so, it would be nice to have a clean way to do that.

Chris Capel
-- 
"What is it like to be a bat? What is it like to bat a bee? What is it
like to be a bee being batted? What is it like to be a batted bee?"
-- The Mind's I (Hofstadter, Dennet)