1.1 --- a/src/Tools/jEdit/src/jedit/scala_console.scala	Sat Jan 09 22:03:47 2010 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/scala_console.scala	Sat Jan 09 23:28:52 2010 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  import org.gjt.sp.jedit.{jEdit, JARClassLoader}
     1.5  import org.gjt.sp.jedit.MiscUtilities
     1.6  
     1.7 -import java.io.{File, Writer, PrintWriter}
     1.8 +import java.io.{File, OutputStream, Writer, PrintWriter}
     1.9  
    1.10  import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
    1.11  import scala.collection.mutable
    1.12 @@ -20,6 +20,20 @@
    1.13  
    1.14  class Scala_Console extends Shell("Scala")
    1.15  {
    1.16 +  /* reconstructed jEdit/plugin classpath */
    1.17 +
    1.18 +  private def reconstruct_classpath(): String =
    1.19 +  {
    1.20 +    def find_jars(start: String): List[String] =
    1.21 +      if (start != null)
    1.22 +        Standard_System.find_files(new File(start),
    1.23 +          entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
    1.24 +      else Nil
    1.25 +    val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome)
    1.26 +    path.mkString(File.pathSeparator)
    1.27 +  }
    1.28 +
    1.29 +
    1.30    /* global state -- owned by Swing thread */
    1.31  
    1.32    private var interpreters = Map[Console, Interpreter]()
    1.33 @@ -28,12 +42,44 @@
    1.34    private var global_out: Output = null
    1.35    private var global_err: Output = null
    1.36  
    1.37 +  private val console_stream = new OutputStream
    1.38 +  {
    1.39 +    val buf = new StringBuilder
    1.40 +    override def flush()
    1.41 +    {
    1.42 +      val str = Standard_System.decode_permissive_utf8(buf.toString)
    1.43 +      buf.clear
    1.44 +      if (global_out == null) System.out.print(str)
    1.45 +      else Swing_Thread.now { global_out.writeAttrs(null, str) }
    1.46 +    }
    1.47 +    override def close() { flush () }
    1.48 +    def write(byte: Int) { buf.append(byte.toChar) }
    1.49 +  }
    1.50 +
    1.51 +  private val console_writer = new Writer
    1.52 +  {
    1.53 +    def flush() {}
    1.54 +    def close() {}
    1.55 +
    1.56 +    def write(cbuf: Array[Char], off: Int, len: Int)
    1.57 +    {
    1.58 +      if (len > 0) write(new String(cbuf.subArray(off, off + len)))
    1.59 +    }
    1.60 +
    1.61 +    override def write(str: String)
    1.62 +    {
    1.63 +      if (global_out == null) System.out.println(str)
    1.64 +      else global_out.print(null, str)
    1.65 +    }
    1.66 +  }
    1.67 +
    1.68    private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A =
    1.69    {
    1.70      global_console = console
    1.71      global_out = out
    1.72      global_err = if (err == null) out else err
    1.73 -    val res = Exn.capture { e }
    1.74 +    val res = Exn.capture { scala.Console.withOut(console_stream)(e) }
    1.75 +    console_stream.flush
    1.76      global_console = null
    1.77      global_out = null
    1.78      global_err = null
    1.79 @@ -43,52 +89,25 @@
    1.80    private def report_error(str: String)
    1.81    {
    1.82      if (global_console == null || global_err == null) System.err.println(str)
    1.83 -    else global_err.print(global_console.getErrorColor, str)
    1.84 +    else Swing_Thread.now { global_err.print(global_console.getErrorColor, str) }
    1.85    }
    1.86  
    1.87 -  private def construct_classpath(): String =
    1.88 -  {
    1.89 -    def find_jars(start: String): List[String] =
    1.90 -      if (start != null)
    1.91 -        Standard_System.find_files(new File(start),
    1.92 -          entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
    1.93 -      else Nil
    1.94 -    val path =
    1.95 -      (jEdit.getJEditHome + File.separator + "jedit.jar") ::
    1.96 -        (find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome))
    1.97 -     path.mkString(File.pathSeparator)
    1.98 -  }
    1.99  
   1.100 -  private class Console_Writer extends Writer
   1.101 -  {
   1.102 -    def close {}
   1.103 -    def flush {}
   1.104 -
   1.105 -    override def write(str: String)
   1.106 -    {
   1.107 -      if (global_out == null) System.out.println(str)
   1.108 -      else global_out.print(null, str)
   1.109 -    }
   1.110 -
   1.111 -    def write(cbuf: Array[Char], off: Int, len: Int)
   1.112 -    {
   1.113 -      if (len > 0) write(new String(cbuf.subArray(off, off + len)))
   1.114 -    }
   1.115 -  }
   1.116 +  /* jEdit console methods */
   1.117  
   1.118    override def openConsole(console: Console)
   1.119    {
   1.120      val settings = new GenericRunnerSettings(report_error)
   1.121 -    settings.classpath.value = construct_classpath()
   1.122 -    val printer = new PrintWriter(new Console_Writer, true)
   1.123 +    settings.classpath.value = reconstruct_classpath()
   1.124  
   1.125 -    val interp = new Interpreter(settings, printer)
   1.126 +    val interp = new Interpreter(settings, new PrintWriter(console_writer, true))
   1.127      {
   1.128        override def parentClassLoader = new JARClassLoader
   1.129      }
   1.130      interp.setContextClassLoader
   1.131      interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
   1.132      interp.bind("session", "isabelle.proofdocument.Session", Isabelle.session)
   1.133 +
   1.134      interpreters += (console -> interp)
   1.135    }
   1.136