src/Tools/jEdit/src/jedit/scala_console.scala
author wenzelm
Sat Jan 09 22:03:47 2010 +0100 (2010-01-09)
changeset 34849 96bcb91b45ce
parent 34846 ca76b3978540
child 34850 fdd560e80264
permissions -rw-r--r--
bind "session";
added printInfoMessage;
added stop -- re-inits the interpreter;
wenzelm@34841
     1
/*
wenzelm@34841
     2
 * Scala instance of Console plugin
wenzelm@34841
     3
 *
wenzelm@34841
     4
 * @author Makarius
wenzelm@34841
     5
 */
wenzelm@34841
     6
wenzelm@34841
     7
package isabelle.jedit
wenzelm@34841
     8
wenzelm@34841
     9
wenzelm@34844
    10
import console.{Console, ConsolePane, Shell, Output}
wenzelm@34841
    11
wenzelm@34845
    12
import org.gjt.sp.jedit.{jEdit, JARClassLoader}
wenzelm@34841
    13
import org.gjt.sp.jedit.MiscUtilities
wenzelm@34841
    14
wenzelm@34846
    15
import java.io.{File, Writer, PrintWriter}
wenzelm@34841
    16
wenzelm@34841
    17
import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
wenzelm@34846
    18
import scala.collection.mutable
wenzelm@34841
    19
wenzelm@34841
    20
wenzelm@34841
    21
class Scala_Console extends Shell("Scala")
wenzelm@34841
    22
{
wenzelm@34849
    23
  /* global state -- owned by Swing thread */
wenzelm@34849
    24
wenzelm@34841
    25
  private var interpreters = Map[Console, Interpreter]()
wenzelm@34841
    26
wenzelm@34841
    27
  private var global_console: Console = null
wenzelm@34841
    28
  private var global_out: Output = null
wenzelm@34841
    29
  private var global_err: Output = null
wenzelm@34841
    30
wenzelm@34844
    31
  private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A =
wenzelm@34844
    32
  {
wenzelm@34844
    33
    global_console = console
wenzelm@34844
    34
    global_out = out
wenzelm@34844
    35
    global_err = if (err == null) out else err
wenzelm@34844
    36
    val res = Exn.capture { e }
wenzelm@34844
    37
    global_console = null
wenzelm@34844
    38
    global_out = null
wenzelm@34844
    39
    global_err = null
wenzelm@34844
    40
    Exn.release(res)
wenzelm@34844
    41
  }
wenzelm@34844
    42
wenzelm@34841
    43
  private def report_error(str: String)
wenzelm@34841
    44
  {
wenzelm@34841
    45
    if (global_console == null || global_err == null) System.err.println(str)
wenzelm@34841
    46
    else global_err.print(global_console.getErrorColor, str)
wenzelm@34841
    47
  }
wenzelm@34841
    48
wenzelm@34846
    49
  private def construct_classpath(): String =
wenzelm@34846
    50
  {
wenzelm@34846
    51
    def find_jars(start: String): List[String] =
wenzelm@34846
    52
      if (start != null)
wenzelm@34846
    53
        Standard_System.find_files(new File(start),
wenzelm@34846
    54
          entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
wenzelm@34846
    55
      else Nil
wenzelm@34846
    56
    val path =
wenzelm@34846
    57
      (jEdit.getJEditHome + File.separator + "jedit.jar") ::
wenzelm@34846
    58
        (find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome))
wenzelm@34846
    59
     path.mkString(File.pathSeparator)
wenzelm@34846
    60
  }
wenzelm@34846
    61
wenzelm@34841
    62
  private class Console_Writer extends Writer
wenzelm@34841
    63
  {
wenzelm@34841
    64
    def close {}
wenzelm@34841
    65
    def flush {}
wenzelm@34841
    66
wenzelm@34841
    67
    override def write(str: String)
wenzelm@34841
    68
    {
wenzelm@34841
    69
      if (global_out == null) System.out.println(str)
wenzelm@34841
    70
      else global_out.print(null, str)
wenzelm@34841
    71
    }
wenzelm@34849
    72
wenzelm@34849
    73
    def write(cbuf: Array[Char], off: Int, len: Int)
wenzelm@34849
    74
    {
wenzelm@34849
    75
      if (len > 0) write(new String(cbuf.subArray(off, off + len)))
wenzelm@34849
    76
    }
wenzelm@34841
    77
  }
wenzelm@34841
    78
wenzelm@34841
    79
  override def openConsole(console: Console)
wenzelm@34841
    80
  {
wenzelm@34841
    81
    val settings = new GenericRunnerSettings(report_error)
wenzelm@34846
    82
    settings.classpath.value = construct_classpath()
wenzelm@34841
    83
    val printer = new PrintWriter(new Console_Writer, true)
wenzelm@34849
    84
wenzelm@34845
    85
    val interp = new Interpreter(settings, printer)
wenzelm@34845
    86
    {
wenzelm@34845
    87
      override def parentClassLoader = new JARClassLoader
wenzelm@34845
    88
    }
wenzelm@34845
    89
    interp.setContextClassLoader
wenzelm@34846
    90
    interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
wenzelm@34849
    91
    interp.bind("session", "isabelle.proofdocument.Session", Isabelle.session)
wenzelm@34845
    92
    interpreters += (console -> interp)
wenzelm@34841
    93
  }
wenzelm@34841
    94
wenzelm@34841
    95
  override def closeConsole(console: Console)
wenzelm@34841
    96
  {
wenzelm@34841
    97
    interpreters -= console
wenzelm@34841
    98
  }
wenzelm@34841
    99
wenzelm@34849
   100
  override def printInfoMessage(out: Output)
wenzelm@34849
   101
  {
wenzelm@34849
   102
    out.print(null,
wenzelm@34849
   103
     "This shell evaluates Isabelle/Scala expressions.\n\n" +
wenzelm@34849
   104
     "The following special toplevel bindings are provided:\n" +
wenzelm@34849
   105
     "  view    -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
wenzelm@34849
   106
     "  session -- Isabelle session (e.g. session.isabelle_system)\n")
wenzelm@34849
   107
  }
wenzelm@34849
   108
wenzelm@34841
   109
  override def printPrompt(console: Console, out: Output)
wenzelm@34841
   110
	{
wenzelm@34844
   111
    out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>")
wenzelm@34845
   112
		out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ")
wenzelm@34841
   113
	}
wenzelm@34841
   114
wenzelm@34841
   115
  override def execute(console: Console, input: String, out: Output, err: Output, command: String)
wenzelm@34841
   116
  {
wenzelm@34846
   117
    val interp = interpreters(console)
wenzelm@34846
   118
    with_console(console, out, err) { interp.interpret(command) }
wenzelm@34844
   119
    if (err != null) err.commandDone()
wenzelm@34844
   120
		out.commandDone()
wenzelm@34841
   121
  }
wenzelm@34849
   122
wenzelm@34849
   123
  override def stop(console: Console)
wenzelm@34849
   124
  {
wenzelm@34849
   125
    closeConsole(console)
wenzelm@34849
   126
    console.clear
wenzelm@34849
   127
    openConsole(console)
wenzelm@34849
   128
    val out = console.getOutput
wenzelm@34849
   129
    out.commandDone
wenzelm@34849
   130
    printPrompt(console, out)
wenzelm@34849
   131
  }
wenzelm@34841
   132
}