src/Tools/jEdit/src/scala_console.scala
author wenzelm
Sun, 25 Nov 2012 20:17:04 +0100
changeset 50203 00d8ad713e32
parent 48613 232652ac346e
child 50205 788c8263e634
permissions -rw-r--r--
explicit module UTF8;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43282
5d294220ca43 moved sources -- eliminated Netbeans artifact of jedit package directory;
wenzelm
parents: 37175
diff changeset
     1
/*  Title:      Tools/jEdit/src/scala_console.scala
36760
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     2
    Author:     Makarius
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     3
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     4
Scala instance of Console plugin.
b82a698ef6c9 tuned headers;
wenzelm
parents: 36015
diff changeset
     5
*/
34841
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
36015
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34857
diff changeset
    10
import isabelle._
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34857
diff changeset
    11
34844
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
    12
import console.{Console, ConsolePane, Shell, Output}
34841
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    13
34845
6d64de27efa5 provide some bindings of jEdit values;
wenzelm
parents: 34844
diff changeset
    14
import org.gjt.sp.jedit.{jEdit, JARClassLoader}
34841
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    15
import org.gjt.sp.jedit.MiscUtilities
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    16
43520
cec9b95fa35d explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents: 43282
diff changeset
    17
import java.lang.System
48613
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48412
diff changeset
    18
import java.io.{File => JFile, FileFilter, OutputStream, Writer, PrintWriter}
34841
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    19
47992
7700f0e9618c avoid scala.tools.nsc.Interpreter -- deprecated in scala-2.9.0;
wenzelm
parents: 45580
diff changeset
    20
import scala.tools.nsc.{GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter}
7700f0e9618c avoid scala.tools.nsc.Interpreter -- deprecated in scala-2.9.0;
wenzelm
parents: 45580
diff changeset
    21
import scala.tools.nsc.interpreter.IMain
34846
ca76b3978540 pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents: 34845
diff changeset
    22
import scala.collection.mutable
34841
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    23
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    24
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    25
class Scala_Console extends Shell("Scala")
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    26
{
34850
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    27
  /* reconstructed jEdit/plugin classpath */
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    28
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    29
  private def reconstruct_classpath(): String =
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    30
  {
48613
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48412
diff changeset
    31
    def find_files(start: JFile, ok: JFile => Boolean = _ => true): List[JFile] =
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48412
diff changeset
    32
    {
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48412
diff changeset
    33
      val files = new mutable.ListBuffer[JFile]
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48412
diff changeset
    34
      val filter = new FileFilter { def accept(entry: JFile) = entry.isDirectory || ok(entry) }
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48412
diff changeset
    35
      def find_entry(entry: JFile)
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48412
diff changeset
    36
      {
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48412
diff changeset
    37
        if (ok(entry)) files += entry
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48412
diff changeset
    38
        if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry)
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48412
diff changeset
    39
      }
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48412
diff changeset
    40
      find_entry(start)
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48412
diff changeset
    41
      files.toList
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48412
diff changeset
    42
    }
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48412
diff changeset
    43
34850
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    44
    def find_jars(start: String): List[String] =
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    45
      if (start != null)
48613
232652ac346e clarified directory content operations (similar to ML version);
wenzelm
parents: 48412
diff changeset
    46
        find_files(new JFile(start),
34850
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    47
          entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath)
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    48
      else Nil
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    49
    val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome)
48409
0d2114eb412a more explicit java.io.{File => JFile};
wenzelm
parents: 47992
diff changeset
    50
    path.mkString(JFile.pathSeparator)
34850
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    51
  }
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    52
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    53
34849
96bcb91b45ce bind "session";
wenzelm
parents: 34846
diff changeset
    54
  /* global state -- owned by Swing thread */
96bcb91b45ce bind "session";
wenzelm
parents: 34846
diff changeset
    55
47992
7700f0e9618c avoid scala.tools.nsc.Interpreter -- deprecated in scala-2.9.0;
wenzelm
parents: 45580
diff changeset
    56
  private var interpreters = Map[Console, IMain]()
34841
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    57
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    58
  private var global_console: Console = null
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    59
  private var global_out: Output = null
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    60
  private var global_err: Output = null
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
    61
34850
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    62
  private val console_stream = new OutputStream
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    63
  {
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    64
    val buf = new StringBuilder
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    65
    override def flush()
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    66
    {
50203
00d8ad713e32 explicit module UTF8;
wenzelm
parents: 48613
diff changeset
    67
      val str = UTF8.decode_permissive(buf.toString)
34850
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    68
      buf.clear
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    69
      if (global_out == null) System.out.print(str)
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    70
      else Swing_Thread.now { global_out.writeAttrs(null, str) }
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    71
    }
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    72
    override def close() { flush () }
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    73
    def write(byte: Int) { buf.append(byte.toChar) }
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    74
  }
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    75
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    76
  private val console_writer = new Writer
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    77
  {
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    78
    def flush() {}
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    79
    def close() {}
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    80
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    81
    def write(cbuf: Array[Char], off: Int, len: Int)
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    82
    {
36015
6111de7c916a adapted to Scala 2.8.0 Beta 1;
wenzelm
parents: 34857
diff changeset
    83
      if (len > 0) write(new String(cbuf.slice(off, off + len)))
34850
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    84
    }
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    85
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    86
    override def write(str: String)
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    87
    {
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    88
      if (global_out == null) System.out.println(str)
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    89
      else global_out.print(null, str)
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    90
    }
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    91
  }
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    92
34844
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
    93
  private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A =
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
    94
  {
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
    95
    global_console = console
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
    96
    global_out = out
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
    97
    global_err = if (err == null) out else err
34850
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    98
    val res = Exn.capture { scala.Console.withOut(console_stream)(e) }
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
    99
    console_stream.flush
34844
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
   100
    global_console = null
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
   101
    global_out = null
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
   102
    global_err = null
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
   103
    Exn.release(res)
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
   104
  }
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
   105
34841
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
   106
  private def report_error(str: String)
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
   107
  {
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
   108
    if (global_console == null || global_err == null) System.err.println(str)
34850
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
   109
    else Swing_Thread.now { global_err.print(global_console.getErrorColor, str) }
34846
ca76b3978540 pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents: 34845
diff changeset
   110
  }
ca76b3978540 pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents: 34845
diff changeset
   111
34841
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
   112
34850
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
   113
  /* jEdit console methods */
34841
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
   114
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
   115
  override def openConsole(console: Console)
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
   116
  {
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
   117
    val settings = new GenericRunnerSettings(report_error)
34850
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
   118
    settings.classpath.value = reconstruct_classpath()
34849
96bcb91b45ce bind "session";
wenzelm
parents: 34846
diff changeset
   119
47992
7700f0e9618c avoid scala.tools.nsc.Interpreter -- deprecated in scala-2.9.0;
wenzelm
parents: 45580
diff changeset
   120
    val interp = new IMain(settings, new PrintWriter(console_writer, true))
34845
6d64de27efa5 provide some bindings of jEdit values;
wenzelm
parents: 34844
diff changeset
   121
    {
6d64de27efa5 provide some bindings of jEdit values;
wenzelm
parents: 34844
diff changeset
   122
      override def parentClassLoader = new JARClassLoader
6d64de27efa5 provide some bindings of jEdit values;
wenzelm
parents: 34844
diff changeset
   123
    }
6d64de27efa5 provide some bindings of jEdit values;
wenzelm
parents: 34844
diff changeset
   124
    interp.setContextClassLoader
34846
ca76b3978540 pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents: 34845
diff changeset
   125
    interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
34852
d21c997104c4 adhoc reset of blink rate;
wenzelm
parents: 34851
diff changeset
   126
    interp.bind("console", "console.Console", console)
34851
304a86164dd2 provide global "Isabelle" within interpreter loop -- using import instead of val avoids pontential conflicts with later import isabelle.jedit._;
wenzelm
parents: 34850
diff changeset
   127
    interp.interpret("import isabelle.jedit.Isabelle")
34850
fdd560e80264 redirect scala.Console output during interpretation;
wenzelm
parents: 34849
diff changeset
   128
34845
6d64de27efa5 provide some bindings of jEdit values;
wenzelm
parents: 34844
diff changeset
   129
    interpreters += (console -> interp)
34841
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
   130
  }
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
   131
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
   132
  override def closeConsole(console: Console)
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
   133
  {
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
   134
    interpreters -= console
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
   135
  }
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
   136
34849
96bcb91b45ce bind "session";
wenzelm
parents: 34846
diff changeset
   137
  override def printInfoMessage(out: Output)
96bcb91b45ce bind "session";
wenzelm
parents: 34846
diff changeset
   138
  {
96bcb91b45ce bind "session";
wenzelm
parents: 34846
diff changeset
   139
    out.print(null,
96bcb91b45ce bind "session";
wenzelm
parents: 34846
diff changeset
   140
     "This shell evaluates Isabelle/Scala expressions.\n\n" +
96bcb91b45ce bind "session";
wenzelm
parents: 34846
diff changeset
   141
     "The following special toplevel bindings are provided:\n" +
34851
304a86164dd2 provide global "Isabelle" within interpreter loop -- using import instead of val avoids pontential conflicts with later import isabelle.jedit._;
wenzelm
parents: 34850
diff changeset
   142
     "  view      -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
45580
136e3faf74da tuned message;
wenzelm
parents: 43661
diff changeset
   143
     "  console   -- jEdit Console plugin\n" +
136e3faf74da tuned message;
wenzelm
parents: 43661
diff changeset
   144
     "  Isabelle  -- Isabelle plugin (e.g. Isabelle.session, Isabelle.document_model)\n")
34849
96bcb91b45ce bind "session";
wenzelm
parents: 34846
diff changeset
   145
  }
96bcb91b45ce bind "session";
wenzelm
parents: 34846
diff changeset
   146
34841
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
   147
  override def printPrompt(console: Console, out: Output)
37175
be764a7adb10 eliminated hard tabs;
wenzelm
parents: 36760
diff changeset
   148
  {
34844
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
   149
    out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>")
37175
be764a7adb10 eliminated hard tabs;
wenzelm
parents: 36760
diff changeset
   150
    out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ")
be764a7adb10 eliminated hard tabs;
wenzelm
parents: 36760
diff changeset
   151
  }
34841
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
   152
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
   153
  override def execute(console: Console, input: String, out: Output, err: Output, command: String)
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
   154
  {
34846
ca76b3978540 pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents: 34845
diff changeset
   155
    val interp = interpreters(console)
ca76b3978540 pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents: 34845
diff changeset
   156
    with_console(console, out, err) { interp.interpret(command) }
34844
92ea2174ea78 more precise prompt etc.;
wenzelm
parents: 34841
diff changeset
   157
    if (err != null) err.commandDone()
37175
be764a7adb10 eliminated hard tabs;
wenzelm
parents: 36760
diff changeset
   158
    out.commandDone()
34841
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
   159
  }
34849
96bcb91b45ce bind "session";
wenzelm
parents: 34846
diff changeset
   160
96bcb91b45ce bind "session";
wenzelm
parents: 34846
diff changeset
   161
  override def stop(console: Console)
96bcb91b45ce bind "session";
wenzelm
parents: 34846
diff changeset
   162
  {
96bcb91b45ce bind "session";
wenzelm
parents: 34846
diff changeset
   163
    closeConsole(console)
96bcb91b45ce bind "session";
wenzelm
parents: 34846
diff changeset
   164
    console.clear
96bcb91b45ce bind "session";
wenzelm
parents: 34846
diff changeset
   165
    openConsole(console)
96bcb91b45ce bind "session";
wenzelm
parents: 34846
diff changeset
   166
    val out = console.getOutput
96bcb91b45ce bind "session";
wenzelm
parents: 34846
diff changeset
   167
    out.commandDone
96bcb91b45ce bind "session";
wenzelm
parents: 34846
diff changeset
   168
    printPrompt(console, out)
96bcb91b45ce bind "session";
wenzelm
parents: 34846
diff changeset
   169
  }
34841
2ada58650469 some attempts at Scala console plugin;
wenzelm
parents:
diff changeset
   170
}