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