src/Tools/jEdit/src/scala_console.scala
author wenzelm
Wed Mar 14 15:37:51 2012 +0100 (2012-03-14)
changeset 46920 5f44c8bea84e
parent 45580 136e3faf74da
child 47992 7700f0e9618c
permissions -rw-r--r--
more explicit indication of swing thread context;
     1 /*  Title:      Tools/jEdit/src/scala_console.scala
     2     Author:     Makarius
     3 
     4 Scala instance of Console plugin.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import console.{Console, ConsolePane, Shell, Output}
    13 
    14 import org.gjt.sp.jedit.{jEdit, JARClassLoader}
    15 import org.gjt.sp.jedit.MiscUtilities
    16 
    17 import java.lang.System
    18 import java.io.{File, OutputStream, Writer, PrintWriter}
    19 
    20 import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
    21 import scala.collection.mutable
    22 
    23 
    24 class Scala_Console extends Shell("Scala")
    25 {
    26   /* reconstructed jEdit/plugin classpath */
    27 
    28   private def reconstruct_classpath(): String =
    29   {
    30     def find_jars(start: String): List[String] =
    31       if (start != null)
    32         Standard_System.find_files(new File(start),
    33           entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
    34       else Nil
    35     val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome)
    36     path.mkString(File.pathSeparator)
    37   }
    38 
    39 
    40   /* global state -- owned by Swing thread */
    41 
    42   private var interpreters = Map[Console, Interpreter]()
    43 
    44   private var global_console: Console = null
    45   private var global_out: Output = null
    46   private var global_err: Output = null
    47 
    48   private val console_stream = new OutputStream
    49   {
    50     val buf = new StringBuilder
    51     override def flush()
    52     {
    53       val str = Standard_System.decode_permissive_utf8(buf.toString)
    54       buf.clear
    55       if (global_out == null) System.out.print(str)
    56       else Swing_Thread.now { global_out.writeAttrs(null, str) }
    57     }
    58     override def close() { flush () }
    59     def write(byte: Int) { buf.append(byte.toChar) }
    60   }
    61 
    62   private val console_writer = new Writer
    63   {
    64     def flush() {}
    65     def close() {}
    66 
    67     def write(cbuf: Array[Char], off: Int, len: Int)
    68     {
    69       if (len > 0) write(new String(cbuf.slice(off, off + len)))
    70     }
    71 
    72     override def write(str: String)
    73     {
    74       if (global_out == null) System.out.println(str)
    75       else global_out.print(null, str)
    76     }
    77   }
    78 
    79   private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A =
    80   {
    81     global_console = console
    82     global_out = out
    83     global_err = if (err == null) out else err
    84     val res = Exn.capture { scala.Console.withOut(console_stream)(e) }
    85     console_stream.flush
    86     global_console = null
    87     global_out = null
    88     global_err = null
    89     Exn.release(res)
    90   }
    91 
    92   private def report_error(str: String)
    93   {
    94     if (global_console == null || global_err == null) System.err.println(str)
    95     else Swing_Thread.now { global_err.print(global_console.getErrorColor, str) }
    96   }
    97 
    98 
    99   /* jEdit console methods */
   100 
   101   override def openConsole(console: Console)
   102   {
   103     val settings = new GenericRunnerSettings(report_error)
   104     settings.classpath.value = reconstruct_classpath()
   105 
   106     val interp = new Interpreter(settings, new PrintWriter(console_writer, true))
   107     {
   108       override def parentClassLoader = new JARClassLoader
   109     }
   110     interp.setContextClassLoader
   111     interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
   112     interp.bind("console", "console.Console", console)
   113     interp.interpret("import isabelle.jedit.Isabelle")
   114 
   115     interpreters += (console -> interp)
   116   }
   117 
   118   override def closeConsole(console: Console)
   119   {
   120     interpreters -= console
   121   }
   122 
   123   override def printInfoMessage(out: Output)
   124   {
   125     out.print(null,
   126      "This shell evaluates Isabelle/Scala expressions.\n\n" +
   127      "The following special toplevel bindings are provided:\n" +
   128      "  view      -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
   129      "  console   -- jEdit Console plugin\n" +
   130      "  Isabelle  -- Isabelle plugin (e.g. Isabelle.session, Isabelle.document_model)\n")
   131   }
   132 
   133   override def printPrompt(console: Console, out: Output)
   134   {
   135     out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>")
   136     out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ")
   137   }
   138 
   139   override def execute(console: Console, input: String, out: Output, err: Output, command: String)
   140   {
   141     val interp = interpreters(console)
   142     with_console(console, out, err) { interp.interpret(command) }
   143     if (err != null) err.commandDone()
   144     out.commandDone()
   145   }
   146 
   147   override def stop(console: Console)
   148   {
   149     closeConsole(console)
   150     console.clear
   151     openConsole(console)
   152     val out = console.getOutput
   153     out.commandDone
   154     printPrompt(console, out)
   155   }
   156 }