src/Tools/jEdit/src/jedit/scala_console.scala
changeset 34850 fdd560e80264
parent 34849 96bcb91b45ce
child 34851 304a86164dd2
equal deleted inserted replaced
34849:96bcb91b45ce 34850:fdd560e80264
    10 import console.{Console, ConsolePane, Shell, Output}
    10 import console.{Console, ConsolePane, Shell, Output}
    11 
    11 
    12 import org.gjt.sp.jedit.{jEdit, JARClassLoader}
    12 import org.gjt.sp.jedit.{jEdit, JARClassLoader}
    13 import org.gjt.sp.jedit.MiscUtilities
    13 import org.gjt.sp.jedit.MiscUtilities
    14 
    14 
    15 import java.io.{File, Writer, PrintWriter}
    15 import java.io.{File, OutputStream, Writer, PrintWriter}
    16 
    16 
    17 import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
    17 import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
    18 import scala.collection.mutable
    18 import scala.collection.mutable
    19 
    19 
    20 
    20 
    21 class Scala_Console extends Shell("Scala")
    21 class Scala_Console extends Shell("Scala")
    22 {
    22 {
       
    23   /* reconstructed jEdit/plugin classpath */
       
    24 
       
    25   private def reconstruct_classpath(): String =
       
    26   {
       
    27     def find_jars(start: String): List[String] =
       
    28       if (start != null)
       
    29         Standard_System.find_files(new File(start),
       
    30           entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
       
    31       else Nil
       
    32     val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome)
       
    33     path.mkString(File.pathSeparator)
       
    34   }
       
    35 
       
    36 
    23   /* global state -- owned by Swing thread */
    37   /* global state -- owned by Swing thread */
    24 
    38 
    25   private var interpreters = Map[Console, Interpreter]()
    39   private var interpreters = Map[Console, Interpreter]()
    26 
    40 
    27   private var global_console: Console = null
    41   private var global_console: Console = null
    28   private var global_out: Output = null
    42   private var global_out: Output = null
    29   private var global_err: Output = null
    43   private var global_err: Output = null
    30 
    44 
       
    45   private val console_stream = new OutputStream
       
    46   {
       
    47     val buf = new StringBuilder
       
    48     override def flush()
       
    49     {
       
    50       val str = Standard_System.decode_permissive_utf8(buf.toString)
       
    51       buf.clear
       
    52       if (global_out == null) System.out.print(str)
       
    53       else Swing_Thread.now { global_out.writeAttrs(null, str) }
       
    54     }
       
    55     override def close() { flush () }
       
    56     def write(byte: Int) { buf.append(byte.toChar) }
       
    57   }
       
    58 
       
    59   private val console_writer = new Writer
       
    60   {
       
    61     def flush() {}
       
    62     def close() {}
       
    63 
       
    64     def write(cbuf: Array[Char], off: Int, len: Int)
       
    65     {
       
    66       if (len > 0) write(new String(cbuf.subArray(off, off + len)))
       
    67     }
       
    68 
       
    69     override def write(str: String)
       
    70     {
       
    71       if (global_out == null) System.out.println(str)
       
    72       else global_out.print(null, str)
       
    73     }
       
    74   }
       
    75 
    31   private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A =
    76   private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A =
    32   {
    77   {
    33     global_console = console
    78     global_console = console
    34     global_out = out
    79     global_out = out
    35     global_err = if (err == null) out else err
    80     global_err = if (err == null) out else err
    36     val res = Exn.capture { e }
    81     val res = Exn.capture { scala.Console.withOut(console_stream)(e) }
       
    82     console_stream.flush
    37     global_console = null
    83     global_console = null
    38     global_out = null
    84     global_out = null
    39     global_err = null
    85     global_err = null
    40     Exn.release(res)
    86     Exn.release(res)
    41   }
    87   }
    42 
    88 
    43   private def report_error(str: String)
    89   private def report_error(str: String)
    44   {
    90   {
    45     if (global_console == null || global_err == null) System.err.println(str)
    91     if (global_console == null || global_err == null) System.err.println(str)
    46     else global_err.print(global_console.getErrorColor, str)
    92     else Swing_Thread.now { global_err.print(global_console.getErrorColor, str) }
    47   }
    93   }
    48 
    94 
    49   private def construct_classpath(): String =
       
    50   {
       
    51     def find_jars(start: String): List[String] =
       
    52       if (start != null)
       
    53         Standard_System.find_files(new File(start),
       
    54           entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
       
    55       else Nil
       
    56     val path =
       
    57       (jEdit.getJEditHome + File.separator + "jedit.jar") ::
       
    58         (find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome))
       
    59      path.mkString(File.pathSeparator)
       
    60   }
       
    61 
    95 
    62   private class Console_Writer extends Writer
    96   /* jEdit console methods */
    63   {
       
    64     def close {}
       
    65     def flush {}
       
    66 
       
    67     override def write(str: String)
       
    68     {
       
    69       if (global_out == null) System.out.println(str)
       
    70       else global_out.print(null, str)
       
    71     }
       
    72 
       
    73     def write(cbuf: Array[Char], off: Int, len: Int)
       
    74     {
       
    75       if (len > 0) write(new String(cbuf.subArray(off, off + len)))
       
    76     }
       
    77   }
       
    78 
    97 
    79   override def openConsole(console: Console)
    98   override def openConsole(console: Console)
    80   {
    99   {
    81     val settings = new GenericRunnerSettings(report_error)
   100     val settings = new GenericRunnerSettings(report_error)
    82     settings.classpath.value = construct_classpath()
   101     settings.classpath.value = reconstruct_classpath()
    83     val printer = new PrintWriter(new Console_Writer, true)
       
    84 
   102 
    85     val interp = new Interpreter(settings, printer)
   103     val interp = new Interpreter(settings, new PrintWriter(console_writer, true))
    86     {
   104     {
    87       override def parentClassLoader = new JARClassLoader
   105       override def parentClassLoader = new JARClassLoader
    88     }
   106     }
    89     interp.setContextClassLoader
   107     interp.setContextClassLoader
    90     interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
   108     interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
    91     interp.bind("session", "isabelle.proofdocument.Session", Isabelle.session)
   109     interp.bind("session", "isabelle.proofdocument.Session", Isabelle.session)
       
   110 
    92     interpreters += (console -> interp)
   111     interpreters += (console -> interp)
    93   }
   112   }
    94 
   113 
    95   override def closeConsole(console: Console)
   114   override def closeConsole(console: Console)
    96   {
   115   {