src/Tools/jEdit/src/jedit/scala_console.scala
author wenzelm
Sat, 09 Jan 2010 00:49:51 +0100
changeset 34845 6d64de27efa5
parent 34844 92ea2174ea78
child 34846 ca76b3978540
permissions -rw-r--r--
provide some bindings of jEdit values; plain color for input;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34841
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
     1
/*
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
     2
 * Scala instance of Console plugin
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
     3
 *
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
     4
 * @author Makarius
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
     5
 */
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
     6
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
     8
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
     9
34844
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
    10
import console.{Console, ConsolePane, Shell, Output}
34841
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    11
34845
6d64de27efa5 provide some bindings of jEdit values;
wenzelm
parents: 34844
diff changeset
    12
import org.gjt.sp.jedit.{jEdit, JARClassLoader}
34841
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    13
import org.gjt.sp.jedit.MiscUtilities
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    14
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    15
import java.io.{Writer, PrintWriter}
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    16
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    17
import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    18
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    19
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    20
class Scala_Console extends Shell("Scala")
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    21
{
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    22
  private var interpreters = Map[Console, Interpreter]()
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    23
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    24
  private var global_console: Console = null
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    25
  private var global_out: Output = null
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    26
  private var global_err: Output = null
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    27
34844
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
    28
  private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A =
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
    29
  {
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
    30
    global_console = console
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
    31
    global_out = out
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
    32
    global_err = if (err == null) out else err
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
    33
    val res = Exn.capture { e }
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
    34
    global_console = null
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
    35
    global_out = null
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
    36
    global_err = null
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
    37
    Exn.release(res)
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
    38
  }
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
    39
34841
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    40
  private def report_error(str: String)
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    41
  {
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    42
    if (global_console == null || global_err == null) System.err.println(str)
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    43
    else global_err.print(global_console.getErrorColor, str)
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    44
  }
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    45
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    46
  private class Console_Writer extends Writer
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    47
  {
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    48
    def close {}
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    49
    def flush {}
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    50
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    51
    def write(cbuf: Array[Char], off: Int, len: Int)
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    52
    {
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    53
      if (len > 0) write(new String(cbuf.subArray(off, off + len)))
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    54
    }
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    55
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    56
    override def write(str: String)
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    57
    {
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    58
      if (global_out == null) System.out.println(str)
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    59
      else global_out.print(null, str)
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    60
    }
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    61
  }
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    62
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    63
  override def openConsole(console: Console)
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    64
  {
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    65
    val settings = new GenericRunnerSettings(report_error)
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    66
    val printer = new PrintWriter(new Console_Writer, true)
34845
6d64de27efa5 provide some bindings of jEdit values;
wenzelm
parents: 34844
diff changeset
    67
    val interp = new Interpreter(settings, printer)
6d64de27efa5 provide some bindings of jEdit values;
wenzelm
parents: 34844
diff changeset
    68
    {
6d64de27efa5 provide some bindings of jEdit values;
wenzelm
parents: 34844
diff changeset
    69
      override def parentClassLoader = new JARClassLoader
6d64de27efa5 provide some bindings of jEdit values;
wenzelm
parents: 34844
diff changeset
    70
    }
6d64de27efa5 provide some bindings of jEdit values;
wenzelm
parents: 34844
diff changeset
    71
    interp.setContextClassLoader
6d64de27efa5 provide some bindings of jEdit values;
wenzelm
parents: 34844
diff changeset
    72
6d64de27efa5 provide some bindings of jEdit values;
wenzelm
parents: 34844
diff changeset
    73
    val view = console.getView
6d64de27efa5 provide some bindings of jEdit values;
wenzelm
parents: 34844
diff changeset
    74
    val edit_pane = view.getEditPane
6d64de27efa5 provide some bindings of jEdit values;
wenzelm
parents: 34844
diff changeset
    75
    interp.bind("view", "org.gjt.sp.jedit.View", view)
6d64de27efa5 provide some bindings of jEdit values;
wenzelm
parents: 34844
diff changeset
    76
    interp.bind("editPane", "org.gjt.sp.jedit.EditPane", edit_pane)
6d64de27efa5 provide some bindings of jEdit values;
wenzelm
parents: 34844
diff changeset
    77
    interp.bind("buffer", "org.gjt.sp.jedit.Buffer", edit_pane.getBuffer)
6d64de27efa5 provide some bindings of jEdit values;
wenzelm
parents: 34844
diff changeset
    78
    interp.bind("textArea", "org.gjt.sp.jedit.textarea.JEditTextArea", edit_pane.getTextArea)
6d64de27efa5 provide some bindings of jEdit values;
wenzelm
parents: 34844
diff changeset
    79
    interp.bind("wm", "org.gjt.sp.jedit.gui.DockableWindowManager", view.getDockableWindowManager)
6d64de27efa5 provide some bindings of jEdit values;
wenzelm
parents: 34844
diff changeset
    80
6d64de27efa5 provide some bindings of jEdit values;
wenzelm
parents: 34844
diff changeset
    81
    interpreters += (console -> interp)
34841
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    82
  }
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    83
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    84
  override def closeConsole(console: Console)
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    85
  {
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    86
    interpreters -= console
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    87
  }
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    88
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    89
  override def printPrompt(console: Console, out: Output)
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    90
	{
34844
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
    91
    out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>")
34845
6d64de27efa5 provide some bindings of jEdit values;
wenzelm
parents: 34844
diff changeset
    92
		out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ")
34841
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    93
	}
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    94
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    95
  override def execute(console: Console, input: String, out: Output, err: Output, command: String)
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    96
  {
34845
6d64de27efa5 provide some bindings of jEdit values;
wenzelm
parents: 34844
diff changeset
    97
    with_console(console, out, err) { interpreters(console).interpret(command) }
34844
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
    98
    if (err != null) err.commandDone()
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
    99
		out.commandDone()
34841
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
   100
  }
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
   101
}