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