Some recent messages on the Isabelle mailing list bring the information that the Isabelle team is working on a new interface for Isabelle and possibly other provers that will replace Emacs based ProofGeneral. The new interface will be written in Scala. Scala is an multiparadigm language (OO and functional) that runs on JVM. This is an interesting choice of technology that suggests something about the design goals (I am speculating again). Applications writen in Scala can run on any platform that has JVM. In particular, one can write applets in Scala that can be run in a browser. Scala is a general purpose language, but seems to be particularly good for web programming. There are a couple of web programming frameworks written in Scala, Lift being the most popular, competing with Rails. So the new interface will be multiplatform and easy to integrate with web applications (wiki?). Hopefully this will make Isabelle proving environment closer to being network transparent – a user interface, possibly running in a browser and sending formalized text for verification to an Isabelle server located (possibly) on a different host with dependencies scattered all over the internet.
There are two ways of looking at authoring Isabelle theories. For some people this is similar to writing software. For those people the Eclipse interface may be better.
I use Isabelle for formalized mathematics so for me Isabelle is a back-end of a document preparation system. The front end to such system should have features typical for a word processor rather than programmer’s editor. The features that are most important for me are the ease of setup and WISIWYG support for mathematical notation. Easy search for theorems (not necessarily semantic, just one based on strings in the comments would be good enough) would be nice too.