src/Tools/jEdit/src/scala_console.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 62443 133f65ac17e5
child 65876 326c9f828c3d
permissions -rw-r--r--
tuned signature;
     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.io.{File => JFile, FileFilter, OutputStream, Writer, PrintWriter}
    18 
    19 import scala.tools.nsc.{GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
    20 import scala.tools.nsc.interpreter.IMain
    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         File.find_files(new JFile(start), file => file.getName.endsWith(".jar")).
    33           map(_.getAbsolutePath)
    34       else Nil
    35 
    36     val initial_class_path =
    37       Library.space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", ""))
    38 
    39     val path =
    40       initial_class_path :::
    41       find_jars(jEdit.getSettingsDirectory) :::
    42       find_jars(jEdit.getJEditHome)
    43     path.mkString(JFile.pathSeparator)
    44   }
    45 
    46 
    47   /* global state -- owned by GUI thread */
    48 
    49   @volatile private var interpreters = Map.empty[Console, Interpreter]
    50 
    51   @volatile private var global_console: Console = null
    52   @volatile private var global_out: Output = null
    53   @volatile private var global_err: Output = null
    54 
    55   private val console_stream = new OutputStream
    56   {
    57     val buf = new StringBuilder
    58     override def flush()
    59     {
    60       val s = buf.synchronized { val s = buf.toString; buf.clear; s }
    61       val str = UTF8.decode_permissive(s)
    62       GUI_Thread.later {
    63         if (global_out == null) System.out.print(str)
    64         else global_out.writeAttrs(null, str)
    65       }
    66       Thread.sleep(10)  // FIXME adhoc delay to avoid loosing output
    67     }
    68     override def close() { flush () }
    69     def write(byte: Int) {
    70       val c = byte.toChar
    71       buf.synchronized { buf.append(c) }
    72       if (c == '\n') flush()
    73     }
    74   }
    75 
    76   private val console_writer = new Writer
    77   {
    78     def flush() {}
    79     def close() {}
    80 
    81     def write(cbuf: Array[Char], off: Int, len: Int)
    82     {
    83       if (len > 0) write(new String(cbuf.slice(off, off + len)))
    84     }
    85 
    86     override def write(str: String)
    87     {
    88       if (global_out == null) System.out.println(str)
    89       else global_out.print(null, str)
    90     }
    91   }
    92 
    93   private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A =
    94   {
    95     global_console = console
    96     global_out = out
    97     global_err = if (err == null) out else err
    98     try {
    99       scala.Console.withErr(console_stream) {
   100         scala.Console.withOut(console_stream) { e }
   101       }
   102     }
   103     finally {
   104       console_stream.flush
   105       global_console = null
   106       global_out = null
   107       global_err = null
   108     }
   109   }
   110 
   111   private def report_error(str: String)
   112   {
   113     if (global_console == null || global_err == null) System.err.println(str)
   114     else GUI_Thread.later { global_err.print(global_console.getErrorColor, str) }
   115   }
   116 
   117 
   118   /* interpreter thread */
   119 
   120   private abstract class Request
   121   private case class Start(console: Console) extends Request
   122   private case class Execute(console: Console, out: Output, err: Output, command: String)
   123     extends Request
   124 
   125   private class Interpreter
   126   {
   127     private val running = Synchronized[Option[Thread]](None)
   128     def interrupt { running.change(opt => { opt.foreach(_.interrupt); opt }) }
   129 
   130     private val settings = new GenericRunnerSettings(report_error)
   131     settings.classpath.value = reconstruct_classpath()
   132 
   133     private val interp = new IMain(settings, new PrintWriter(console_writer, true))
   134     {
   135       override def parentClassLoader = new JARClassLoader
   136     }
   137     interp.setContextClassLoader
   138 
   139     val thread: Consumer_Thread[Request] = Consumer_Thread.fork("Scala_Console")
   140     {
   141       case Start(console) =>
   142         interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
   143         interp.bind("console", "console.Console", console)
   144         interp.interpret("import isabelle._; import isabelle.jedit._")
   145         true
   146 
   147       case Execute(console, out, err, command) =>
   148         with_console(console, out, err) {
   149           try {
   150             running.change(_ => Some(Thread.currentThread()))
   151             interp.interpret(command)
   152           }
   153           finally {
   154             running.change(_ => None)
   155             Thread.interrupted
   156           }
   157           GUI_Thread.later {
   158             if (err != null) err.commandDone()
   159             out.commandDone()
   160           }
   161           true
   162         }
   163     }
   164   }
   165 
   166 
   167   /* jEdit console methods */
   168 
   169   override def openConsole(console: Console)
   170   {
   171     val interp = new Interpreter
   172     interp.thread.send(Start(console))
   173     interpreters += (console -> interp)
   174   }
   175 
   176   override def closeConsole(console: Console)
   177   {
   178     interpreters.get(console) match {
   179       case Some(interp) =>
   180         interp.interrupt
   181         interp.thread.shutdown
   182         interpreters -= console
   183       case None =>
   184     }
   185   }
   186 
   187   override def printInfoMessage(out: Output)
   188   {
   189     out.print(null,
   190      "This shell evaluates Isabelle/Scala expressions.\n\n" +
   191      "The contents of package isabelle and isabelle.jedit are imported.\n" +
   192      "The following special toplevel bindings are provided:\n" +
   193      "  view    -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
   194      "  console -- jEdit Console plugin\n" +
   195      "  PIDE    -- Isabelle/PIDE plugin (e.g. PIDE.session, PIDE.snapshot, PIDE.rendering)\n")
   196   }
   197 
   198   override def printPrompt(console: Console, out: Output)
   199   {
   200     out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>")
   201     out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ")
   202   }
   203 
   204   override def execute(console: Console, input: String, out: Output, err: Output, command: String)
   205   {
   206     interpreters(console).thread.send(Execute(console, out, err, command))
   207   }
   208 
   209   override def stop(console: Console)
   210   {
   211     interpreters.get(console).foreach(_.interrupt)
   212   }
   213 }