src/Tools/jEdit/src/scala_console.scala
author wenzelm
Thu Jun 23 14:52:32 2011 +0200 (2011-06-23)
changeset 43520 cec9b95fa35d
parent 43282 5d294220ca43
child 43661 39fdbd814c7f
permissions -rw-r--r--
explicit import java.lang.System to prevent odd scope problems;
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@43520
    17
import java.lang.System
wenzelm@34850
    18
import java.io.{File, OutputStream, Writer, PrintWriter}
wenzelm@34841
    19
wenzelm@34841
    20
import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
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@34850
    32
        Standard_System.find_files(new File(start),
wenzelm@34850
    33
          entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
wenzelm@34850
    34
      else Nil
wenzelm@34850
    35
    val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome)
wenzelm@34850
    36
    path.mkString(File.pathSeparator)
wenzelm@34850
    37
  }
wenzelm@34850
    38
wenzelm@34850
    39
wenzelm@34849
    40
  /* global state -- owned by Swing thread */
wenzelm@34849
    41
wenzelm@34841
    42
  private var interpreters = Map[Console, Interpreter]()
wenzelm@34841
    43
wenzelm@34841
    44
  private var global_console: Console = null
wenzelm@34841
    45
  private var global_out: Output = null
wenzelm@34841
    46
  private var global_err: Output = null
wenzelm@34841
    47
wenzelm@34850
    48
  private val console_stream = new OutputStream
wenzelm@34850
    49
  {
wenzelm@34850
    50
    val buf = new StringBuilder
wenzelm@34850
    51
    override def flush()
wenzelm@34850
    52
    {
wenzelm@34850
    53
      val str = Standard_System.decode_permissive_utf8(buf.toString)
wenzelm@34850
    54
      buf.clear
wenzelm@34850
    55
      if (global_out == null) System.out.print(str)
wenzelm@34850
    56
      else Swing_Thread.now { global_out.writeAttrs(null, str) }
wenzelm@34850
    57
    }
wenzelm@34850
    58
    override def close() { flush () }
wenzelm@34850
    59
    def write(byte: Int) { buf.append(byte.toChar) }
wenzelm@34850
    60
  }
wenzelm@34850
    61
wenzelm@34850
    62
  private val console_writer = new Writer
wenzelm@34850
    63
  {
wenzelm@34850
    64
    def flush() {}
wenzelm@34850
    65
    def close() {}
wenzelm@34850
    66
wenzelm@34850
    67
    def write(cbuf: Array[Char], off: Int, len: Int)
wenzelm@34850
    68
    {
wenzelm@36015
    69
      if (len > 0) write(new String(cbuf.slice(off, off + len)))
wenzelm@34850
    70
    }
wenzelm@34850
    71
wenzelm@34850
    72
    override def write(str: String)
wenzelm@34850
    73
    {
wenzelm@34850
    74
      if (global_out == null) System.out.println(str)
wenzelm@34850
    75
      else global_out.print(null, str)
wenzelm@34850
    76
    }
wenzelm@34850
    77
  }
wenzelm@34850
    78
wenzelm@34844
    79
  private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A =
wenzelm@34844
    80
  {
wenzelm@34844
    81
    global_console = console
wenzelm@34844
    82
    global_out = out
wenzelm@34844
    83
    global_err = if (err == null) out else err
wenzelm@34850
    84
    val res = Exn.capture { scala.Console.withOut(console_stream)(e) }
wenzelm@34850
    85
    console_stream.flush
wenzelm@34844
    86
    global_console = null
wenzelm@34844
    87
    global_out = null
wenzelm@34844
    88
    global_err = null
wenzelm@34844
    89
    Exn.release(res)
wenzelm@34844
    90
  }
wenzelm@34844
    91
wenzelm@34841
    92
  private def report_error(str: String)
wenzelm@34841
    93
  {
wenzelm@34841
    94
    if (global_console == null || global_err == null) System.err.println(str)
wenzelm@34850
    95
    else Swing_Thread.now { global_err.print(global_console.getErrorColor, str) }
wenzelm@34846
    96
  }
wenzelm@34846
    97
wenzelm@34841
    98
wenzelm@34850
    99
  /* jEdit console methods */
wenzelm@34841
   100
wenzelm@34841
   101
  override def openConsole(console: Console)
wenzelm@34841
   102
  {
wenzelm@34841
   103
    val settings = new GenericRunnerSettings(report_error)
wenzelm@34850
   104
    settings.classpath.value = reconstruct_classpath()
wenzelm@34849
   105
wenzelm@34850
   106
    val interp = new Interpreter(settings, new PrintWriter(console_writer, true))
wenzelm@34845
   107
    {
wenzelm@34845
   108
      override def parentClassLoader = new JARClassLoader
wenzelm@34845
   109
    }
wenzelm@34845
   110
    interp.setContextClassLoader
wenzelm@34846
   111
    interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
wenzelm@34852
   112
    interp.bind("console", "console.Console", console)
wenzelm@34851
   113
    interp.interpret("import isabelle.jedit.Isabelle")
wenzelm@34850
   114
wenzelm@34845
   115
    interpreters += (console -> interp)
wenzelm@34841
   116
  }
wenzelm@34841
   117
wenzelm@34841
   118
  override def closeConsole(console: Console)
wenzelm@34841
   119
  {
wenzelm@34841
   120
    interpreters -= console
wenzelm@34841
   121
  }
wenzelm@34841
   122
wenzelm@34849
   123
  override def printInfoMessage(out: Output)
wenzelm@34849
   124
  {
wenzelm@34849
   125
    out.print(null,
wenzelm@34849
   126
     "This shell evaluates Isabelle/Scala expressions.\n\n" +
wenzelm@34849
   127
     "The following special toplevel bindings are provided:\n" +
wenzelm@34851
   128
     "  view      -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
wenzelm@34852
   129
     "  console   -- jEdit Console plugin instance\n" +
wenzelm@34852
   130
     "  Isabelle  -- Isabelle plugin instance (e.g. Isabelle.system, Isabelle.session)\n")
wenzelm@34849
   131
  }
wenzelm@34849
   132
wenzelm@34841
   133
  override def printPrompt(console: Console, out: Output)
wenzelm@37175
   134
  {
wenzelm@34844
   135
    out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>")
wenzelm@37175
   136
    out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ")
wenzelm@37175
   137
  }
wenzelm@34841
   138
wenzelm@34841
   139
  override def execute(console: Console, input: String, out: Output, err: Output, command: String)
wenzelm@34841
   140
  {
wenzelm@34846
   141
    val interp = interpreters(console)
wenzelm@34846
   142
    with_console(console, out, err) { interp.interpret(command) }
wenzelm@34844
   143
    if (err != null) err.commandDone()
wenzelm@37175
   144
    out.commandDone()
wenzelm@34841
   145
  }
wenzelm@34849
   146
wenzelm@34849
   147
  override def stop(console: Console)
wenzelm@34849
   148
  {
wenzelm@34849
   149
    closeConsole(console)
wenzelm@34849
   150
    console.clear
wenzelm@34849
   151
    openConsole(console)
wenzelm@34849
   152
    val out = console.getOutput
wenzelm@34849
   153
    out.commandDone
wenzelm@34849
   154
    printPrompt(console, out)
wenzelm@34849
   155
  }
wenzelm@34841
   156
}