src/Tools/jEdit/src/jedit/scala_console.scala
changeset 34849 96bcb91b45ce
parent 34846 ca76b3978540
child 34850 fdd560e80264
--- a/src/Tools/jEdit/src/jedit/scala_console.scala	Sat Jan 09 22:02:35 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/scala_console.scala	Sat Jan 09 22:03:47 2010 +0100
@@ -20,6 +20,8 @@
 
 class Scala_Console extends Shell("Scala")
 {
+  /* global state -- owned by Swing thread */
+
   private var interpreters = Map[Console, Interpreter]()
 
   private var global_console: Console = null
@@ -62,16 +64,16 @@
     def close {}
     def flush {}
 
-    def write(cbuf: Array[Char], off: Int, len: Int)
-    {
-      if (len > 0) write(new String(cbuf.subArray(off, off + len)))
-    }
-
     override def write(str: String)
     {
       if (global_out == null) System.out.println(str)
       else global_out.print(null, str)
     }
+
+    def write(cbuf: Array[Char], off: Int, len: Int)
+    {
+      if (len > 0) write(new String(cbuf.subArray(off, off + len)))
+    }
   }
 
   override def openConsole(console: Console)
@@ -79,12 +81,14 @@
     val settings = new GenericRunnerSettings(report_error)
     settings.classpath.value = construct_classpath()
     val printer = new PrintWriter(new Console_Writer, true)
+
     val interp = new Interpreter(settings, printer)
     {
       override def parentClassLoader = new JARClassLoader
     }
     interp.setContextClassLoader
     interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
+    interp.bind("session", "isabelle.proofdocument.Session", Isabelle.session)
     interpreters += (console -> interp)
   }
 
@@ -93,6 +97,15 @@
     interpreters -= console
   }
 
+  override def printInfoMessage(out: Output)
+  {
+    out.print(null,
+     "This shell evaluates Isabelle/Scala expressions.\n\n" +
+     "The following special toplevel bindings are provided:\n" +
+     "  view    -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
+     "  session -- Isabelle session (e.g. session.isabelle_system)\n")
+  }
+
   override def printPrompt(console: Console, out: Output)
 	{
     out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>")
@@ -106,4 +119,14 @@
     if (err != null) err.commandDone()
 		out.commandDone()
   }
+
+  override def stop(console: Console)
+  {
+    closeConsole(console)
+    console.clear
+    openConsole(console)
+    val out = console.getOutput
+    out.commandDone
+    printPrompt(console, out)
+  }
 }