# HG changeset patch # User wenzelm # Date 1263071027 -3600 # Node ID 96bcb91b45ce24313aeb625b78d10792eb3a4f39 # Parent 77ac1383397265861f2bd7567180636464804ebd bind "session"; added printInfoMessage; added stop -- re-inits the interpreter; diff -r 77ac13833972 -r 96bcb91b45ce src/Tools/jEdit/src/jedit/scala_console.scala --- 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) + } }