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