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