src/Tools/jEdit/src/jedit/scala_console.scala
author wenzelm
Fri Jan 08 12:26:44 2010 +0100 (2010-01-08)
changeset 34844 92ea2174ea78
parent 34841 2ada58650469
child 34845 6d64de27efa5
permissions -rw-r--r--
more precise prompt etc.;
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@34841
    12
import org.gjt.sp.jedit.jEdit
wenzelm@34841
    13
import org.gjt.sp.jedit.MiscUtilities
wenzelm@34841
    14
wenzelm@34841
    15
import java.io.{Writer, PrintWriter}
wenzelm@34841
    16
wenzelm@34841
    17
import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
wenzelm@34841
    18
wenzelm@34841
    19
wenzelm@34841
    20
class Scala_Console extends Shell("Scala")
wenzelm@34841
    21
{
wenzelm@34841
    22
  private var interpreters = Map[Console, Interpreter]()
wenzelm@34841
    23
wenzelm@34841
    24
  private var global_console: Console = null
wenzelm@34841
    25
  private var global_out: Output = null
wenzelm@34841
    26
  private var global_err: Output = null
wenzelm@34841
    27
wenzelm@34844
    28
  private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A =
wenzelm@34844
    29
  {
wenzelm@34844
    30
    global_console = console
wenzelm@34844
    31
    global_out = out
wenzelm@34844
    32
    global_err = if (err == null) out else err
wenzelm@34844
    33
    val res = Exn.capture { e }
wenzelm@34844
    34
    global_console = null
wenzelm@34844
    35
    global_out = null
wenzelm@34844
    36
    global_err = null
wenzelm@34844
    37
    Exn.release(res)
wenzelm@34844
    38
  }
wenzelm@34844
    39
wenzelm@34841
    40
  private def report_error(str: String)
wenzelm@34841
    41
  {
wenzelm@34841
    42
    if (global_console == null || global_err == null) System.err.println(str)
wenzelm@34841
    43
    else global_err.print(global_console.getErrorColor, str)
wenzelm@34841
    44
  }
wenzelm@34841
    45
wenzelm@34841
    46
  private class Console_Writer extends Writer
wenzelm@34841
    47
  {
wenzelm@34841
    48
    def close {}
wenzelm@34841
    49
    def flush {}
wenzelm@34841
    50
wenzelm@34841
    51
    def write(cbuf: Array[Char], off: Int, len: Int)
wenzelm@34841
    52
    {
wenzelm@34841
    53
      if (len > 0) write(new String(cbuf.subArray(off, off + len)))
wenzelm@34841
    54
    }
wenzelm@34841
    55
wenzelm@34841
    56
    override def write(str: String)
wenzelm@34841
    57
    {
wenzelm@34841
    58
      if (global_out == null) System.out.println(str)
wenzelm@34841
    59
      else global_out.print(null, str)
wenzelm@34841
    60
    }
wenzelm@34841
    61
  }
wenzelm@34841
    62
wenzelm@34841
    63
  override def openConsole(console: Console)
wenzelm@34841
    64
  {
wenzelm@34841
    65
    val settings = new GenericRunnerSettings(report_error)
wenzelm@34841
    66
    val printer = new PrintWriter(new Console_Writer, true)
wenzelm@34841
    67
    interpreters += (console -> new Interpreter(settings, printer))
wenzelm@34841
    68
  }
wenzelm@34841
    69
wenzelm@34841
    70
  override def closeConsole(console: Console)
wenzelm@34841
    71
  {
wenzelm@34841
    72
    interpreters -= console
wenzelm@34841
    73
  }
wenzelm@34841
    74
wenzelm@34841
    75
  override def printPrompt(console: Console, out: Output)
wenzelm@34841
    76
	{
wenzelm@34844
    77
    out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>")
wenzelm@34844
    78
		out.writeAttrs(null," ")
wenzelm@34841
    79
	}
wenzelm@34841
    80
wenzelm@34841
    81
  override def execute(console: Console, input: String, out: Output, err: Output, command: String)
wenzelm@34841
    82
  {
wenzelm@34844
    83
    with_console(console, out, err) {
wenzelm@34844
    84
      interpreters(console).interpret(command)
wenzelm@34844
    85
    }
wenzelm@34844
    86
    if (err != null) err.commandDone()
wenzelm@34844
    87
		out.commandDone()
wenzelm@34841
    88
  }
wenzelm@34841
    89
}