--- a/src/Tools/jEdit/src/jedit/scala_console.scala Wed Jun 08 17:01:07 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,155 +0,0 @@
-/* Title: Tools/jEdit/src/jedit/scala_console.scala
- Author: Makarius
-
-Scala instance of Console plugin.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import console.{Console, ConsolePane, Shell, Output}
-
-import org.gjt.sp.jedit.{jEdit, JARClassLoader}
-import org.gjt.sp.jedit.MiscUtilities
-
-import java.io.{File, OutputStream, Writer, PrintWriter}
-
-import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
-import scala.collection.mutable
-
-
-class Scala_Console extends Shell("Scala")
-{
- /* reconstructed jEdit/plugin classpath */
-
- private def reconstruct_classpath(): String =
- {
- def find_jars(start: String): List[String] =
- if (start != null)
- Standard_System.find_files(new File(start),
- entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
- else Nil
- val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome)
- path.mkString(File.pathSeparator)
- }
-
-
- /* global state -- owned by Swing thread */
-
- private var interpreters = Map[Console, Interpreter]()
-
- private var global_console: Console = null
- private var global_out: Output = null
- private var global_err: Output = null
-
- private val console_stream = new OutputStream
- {
- val buf = new StringBuilder
- override def flush()
- {
- val str = Standard_System.decode_permissive_utf8(buf.toString)
- buf.clear
- if (global_out == null) System.out.print(str)
- else Swing_Thread.now { global_out.writeAttrs(null, str) }
- }
- override def close() { flush () }
- def write(byte: Int) { buf.append(byte.toChar) }
- }
-
- private val console_writer = new Writer
- {
- def flush() {}
- def close() {}
-
- def write(cbuf: Array[Char], off: Int, len: Int)
- {
- if (len > 0) write(new String(cbuf.slice(off, off + len)))
- }
-
- override def write(str: String)
- {
- if (global_out == null) System.out.println(str)
- else global_out.print(null, str)
- }
- }
-
- private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A =
- {
- global_console = console
- global_out = out
- global_err = if (err == null) out else err
- val res = Exn.capture { scala.Console.withOut(console_stream)(e) }
- console_stream.flush
- global_console = null
- global_out = null
- global_err = null
- Exn.release(res)
- }
-
- private def report_error(str: String)
- {
- if (global_console == null || global_err == null) System.err.println(str)
- else Swing_Thread.now { global_err.print(global_console.getErrorColor, str) }
- }
-
-
- /* jEdit console methods */
-
- override def openConsole(console: Console)
- {
- val settings = new GenericRunnerSettings(report_error)
- settings.classpath.value = reconstruct_classpath()
-
- val interp = new Interpreter(settings, new PrintWriter(console_writer, true))
- {
- override def parentClassLoader = new JARClassLoader
- }
- interp.setContextClassLoader
- interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
- interp.bind("console", "console.Console", console)
- interp.interpret("import isabelle.jedit.Isabelle")
-
- interpreters += (console -> interp)
- }
-
- override def closeConsole(console: Console)
- {
- 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" +
- " console -- jEdit Console plugin instance\n" +
- " Isabelle -- Isabelle plugin instance (e.g. Isabelle.system, Isabelle.session)\n")
- }
-
- override def printPrompt(console: Console, out: Output)
- {
- out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>")
- out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ")
- }
-
- override def execute(console: Console, input: String, out: Output, err: Output, command: String)
- {
- val interp = interpreters(console)
- with_console(console, out, err) { interp.interpret(command) }
- 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)
- }
-}