# HG changeset patch # User wenzelm # Date 1263076132 -3600 # Node ID fdd560e80264839bf353bdf0636b1135c9d20506 # Parent 96bcb91b45ce24313aeb625b78d10792eb3a4f39 redirect scala.Console output during interpretation; misc tuning; diff -r 96bcb91b45ce -r fdd560e80264 src/Tools/jEdit/src/jedit/scala_console.scala --- a/src/Tools/jEdit/src/jedit/scala_console.scala Sat Jan 09 22:03:47 2010 +0100 +++ b/src/Tools/jEdit/src/jedit/scala_console.scala Sat Jan 09 23:28:52 2010 +0100 @@ -12,7 +12,7 @@ import org.gjt.sp.jedit.{jEdit, JARClassLoader} import org.gjt.sp.jedit.MiscUtilities -import java.io.{File, Writer, PrintWriter} +import java.io.{File, OutputStream, Writer, PrintWriter} import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter} import scala.collection.mutable @@ -20,6 +20,20 @@ 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]() @@ -28,12 +42,44 @@ 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.subArray(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 { e } + val res = Exn.capture { scala.Console.withOut(console_stream)(e) } + console_stream.flush global_console = null global_out = null global_err = null @@ -43,52 +89,25 @@ private def report_error(str: String) { if (global_console == null || global_err == null) System.err.println(str) - else global_err.print(global_console.getErrorColor, str) - } - - private def construct_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 = - (jEdit.getJEditHome + File.separator + "jedit.jar") :: - (find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome)) - path.mkString(File.pathSeparator) + else Swing_Thread.now { global_err.print(global_console.getErrorColor, str) } } - private class Console_Writer extends Writer - { - def close {} - def flush {} - 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))) - } - } + /* jEdit console methods */ override def openConsole(console: Console) { val settings = new GenericRunnerSettings(report_error) - settings.classpath.value = construct_classpath() - val printer = new PrintWriter(new Console_Writer, true) + settings.classpath.value = reconstruct_classpath() - val interp = new Interpreter(settings, printer) + 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("session", "isabelle.proofdocument.Session", Isabelle.session) + interpreters += (console -> interp) }