src/Tools/jEdit/src/scala_console.scala
author wenzelm
Sun Dec 10 20:29:00 2017 +0100 (18 months ago)
changeset 67178 70576478bda9
parent 66923 914935f8a462
permissions -rw-r--r--
avoid println with its extra CR on Windows;
     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(File.absolute_name(_))
    34       else Nil
    35 
    36     val initial_class_path =
    37       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(100)
    58 
    59     override def flush()
    60     {
    61       val s = buf.synchronized { val s = buf.toString; buf.clear; s }
    62       val str = UTF8.decode_permissive(s)
    63       GUI_Thread.later {
    64         if (global_out == null) System.out.print(str)
    65         else global_out.writeAttrs(null, str)
    66       }
    67       Thread.sleep(10)  // FIXME adhoc delay to avoid loosing output
    68     }
    69 
    70     override def close() { flush () }
    71 
    72     def write(byte: Int)
    73     {
    74       val c = byte.toChar
    75       buf.synchronized { buf.append(c) }
    76       if (c == '\n') flush()
    77     }
    78   }
    79 
    80   private val console_writer = new Writer
    81   {
    82     def flush() { console_stream.flush() }
    83     def close() { console_stream.flush() }
    84 
    85     def write(cbuf: Array[Char], off: Int, len: Int)
    86     {
    87       if (len > 0) {
    88         UTF8.bytes(new String(cbuf.slice(off, off + len))).foreach(console_stream.write(_))
    89       }
    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) isabelle.Output.writeln(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 }