author | wenzelm |
Sun, 13 Dec 2020 16:35:37 +0100 | |
changeset 72900 | c9813630cca4 |
parent 71868 | 06ec50d9fc0a |
child 73340 | 0ffcad1f6130 |
permissions | -rw-r--r-- |
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 | 2 |
Author: Makarius |
3 |
||
4 |
Scala instance of Console plugin. |
|
5 |
*/ |
|
34841 | 6 |
|
7 |
package isabelle.jedit |
|
8 |
||
9 |
||
36015 | 10 |
import isabelle._ |
11 |
||
34844 | 12 |
import console.{Console, ConsolePane, Shell, Output} |
71863 | 13 |
import org.gjt.sp.jedit.JARClassLoader |
14 |
import java.io.{OutputStream, Writer, PrintWriter} |
|
34841 | 15 |
|
16 |
||
17 |
class Scala_Console extends Shell("Scala") |
|
18 |
{ |
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57609
diff
changeset
|
19 |
/* global state -- owned by GUI thread */ |
34849 | 20 |
|
57609 | 21 |
@volatile private var interpreters = Map.empty[Console, Interpreter] |
34841 | 22 |
|
57609 | 23 |
@volatile private var global_console: Console = null |
24 |
@volatile private var global_out: Output = null |
|
25 |
@volatile private var global_err: Output = null |
|
34841 | 26 |
|
34850
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
27 |
private val console_stream = new OutputStream |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
28 |
{ |
65876 | 29 |
val buf = new StringBuilder(100) |
30 |
||
34850
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
31 |
override def flush() |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
32 |
{ |
57609 | 33 |
val s = buf.synchronized { val s = buf.toString; buf.clear; s } |
56833
d0a57abc71f8
clarified synchronization and exception handling;
wenzelm
parents:
56832
diff
changeset
|
34 |
val str = UTF8.decode_permissive(s) |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57609
diff
changeset
|
35 |
GUI_Thread.later { |
56834
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
36 |
if (global_out == null) System.out.print(str) |
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
37 |
else global_out.writeAttrs(null, str) |
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
38 |
} |
71684 | 39 |
Time.seconds(0.01).sleep // FIXME adhoc delay to avoid loosing output |
34850
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
40 |
} |
65876 | 41 |
|
34850
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
42 |
override def close() { flush () } |
65876 | 43 |
|
44 |
def write(byte: Int) |
|
45 |
{ |
|
56833
d0a57abc71f8
clarified synchronization and exception handling;
wenzelm
parents:
56832
diff
changeset
|
46 |
val c = byte.toChar |
57609 | 47 |
buf.synchronized { buf.append(c) } |
56833
d0a57abc71f8
clarified synchronization and exception handling;
wenzelm
parents:
56832
diff
changeset
|
48 |
if (c == '\n') flush() |
d0a57abc71f8
clarified synchronization and exception handling;
wenzelm
parents:
56832
diff
changeset
|
49 |
} |
34850
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
50 |
} |
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 |
private val console_writer = new Writer |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
53 |
{ |
65877
6eb1a3f7012f
more uniform line-oriented output, notably for scala-2.12.2 REPL which emits "\n" separately;
wenzelm
parents:
65876
diff
changeset
|
54 |
def flush() { console_stream.flush() } |
6eb1a3f7012f
more uniform line-oriented output, notably for scala-2.12.2 REPL which emits "\n" separately;
wenzelm
parents:
65876
diff
changeset
|
55 |
def close() { console_stream.flush() } |
34850
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
56 |
|
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
57 |
def write(cbuf: Array[Char], off: Int, len: Int) |
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
58 |
{ |
65877
6eb1a3f7012f
more uniform line-oriented output, notably for scala-2.12.2 REPL which emits "\n" separately;
wenzelm
parents:
65876
diff
changeset
|
59 |
if (len > 0) { |
6eb1a3f7012f
more uniform line-oriented output, notably for scala-2.12.2 REPL which emits "\n" separately;
wenzelm
parents:
65876
diff
changeset
|
60 |
UTF8.bytes(new String(cbuf.slice(off, off + len))).foreach(console_stream.write(_)) |
6eb1a3f7012f
more uniform line-oriented output, notably for scala-2.12.2 REPL which emits "\n" separately;
wenzelm
parents:
65876
diff
changeset
|
61 |
} |
34850
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
62 |
} |
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 |
|
34844 | 65 |
private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A = |
66 |
{ |
|
67 |
global_console = console |
|
68 |
global_out = out |
|
69 |
global_err = if (err == null) out else err |
|
56833
d0a57abc71f8
clarified synchronization and exception handling;
wenzelm
parents:
56832
diff
changeset
|
70 |
try { |
56832 | 71 |
scala.Console.withErr(console_stream) { |
72 |
scala.Console.withOut(console_stream) { e } |
|
73 |
} |
|
74 |
} |
|
56833
d0a57abc71f8
clarified synchronization and exception handling;
wenzelm
parents:
56832
diff
changeset
|
75 |
finally { |
d0a57abc71f8
clarified synchronization and exception handling;
wenzelm
parents:
56832
diff
changeset
|
76 |
console_stream.flush |
d0a57abc71f8
clarified synchronization and exception handling;
wenzelm
parents:
56832
diff
changeset
|
77 |
global_console = null |
d0a57abc71f8
clarified synchronization and exception handling;
wenzelm
parents:
56832
diff
changeset
|
78 |
global_out = null |
d0a57abc71f8
clarified synchronization and exception handling;
wenzelm
parents:
56832
diff
changeset
|
79 |
global_err = null |
d0a57abc71f8
clarified synchronization and exception handling;
wenzelm
parents:
56832
diff
changeset
|
80 |
} |
34844 | 81 |
} |
82 |
||
34841 | 83 |
private def report_error(str: String) |
84 |
{ |
|
67178 | 85 |
if (global_console == null || global_err == null) isabelle.Output.writeln(str) |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57609
diff
changeset
|
86 |
else GUI_Thread.later { 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
|
87 |
} |
ca76b3978540
pass all jEdit jars to compiler as classpath -- to enable proper referencing of application name space;
wenzelm
parents:
34845
diff
changeset
|
88 |
|
34841 | 89 |
|
56834
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
90 |
/* interpreter thread */ |
34841 | 91 |
|
56836
69531d86d77e
more sensible interrupt of interpreter, when the user pushes Cancel button;
wenzelm
parents:
56834
diff
changeset
|
92 |
private abstract class Request |
56834
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
93 |
private case class Start(console: Console) extends Request |
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
94 |
private case class Execute(console: Console, out: Output, err: Output, command: String) |
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
95 |
extends Request |
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
96 |
|
56836
69531d86d77e
more sensible interrupt of interpreter, when the user pushes Cancel button;
wenzelm
parents:
56834
diff
changeset
|
97 |
private class Interpreter |
34841 | 98 |
{ |
61590 | 99 |
private val running = Synchronized[Option[Thread]](None) |
56836
69531d86d77e
more sensible interrupt of interpreter, when the user pushes Cancel button;
wenzelm
parents:
56834
diff
changeset
|
100 |
def interrupt { running.change(opt => { opt.foreach(_.interrupt); opt }) } |
69531d86d77e
more sensible interrupt of interpreter, when the user pushes Cancel button;
wenzelm
parents:
56834
diff
changeset
|
101 |
|
71868 | 102 |
private val interp = |
103 |
Scala.Compiler.context(error = report_error, jar_dirs = JEdit_Lib.directories). |
|
104 |
interpreter( |
|
105 |
print_writer = new PrintWriter(console_writer, true), |
|
106 |
class_loader = new JARClassLoader) |
|
56834
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
107 |
|
56836
69531d86d77e
more sensible interrupt of interpreter, when the user pushes Cancel button;
wenzelm
parents:
56834
diff
changeset
|
108 |
val thread: Consumer_Thread[Request] = Consumer_Thread.fork("Scala_Console") |
69531d86d77e
more sensible interrupt of interpreter, when the user pushes Cancel button;
wenzelm
parents:
56834
diff
changeset
|
109 |
{ |
56834
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
110 |
case Start(console) => |
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
111 |
interp.bind("view", "org.gjt.sp.jedit.View", console.getView) |
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
112 |
interp.bind("console", "console.Console", console) |
57603 | 113 |
interp.interpret("import isabelle._; import isabelle.jedit._") |
56834
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
114 |
true |
34850
fdd560e80264
redirect scala.Console output during interpretation;
wenzelm
parents:
34849
diff
changeset
|
115 |
|
56834
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
116 |
case Execute(console, out, err, command) => |
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
117 |
with_console(console, out, err) { |
56836
69531d86d77e
more sensible interrupt of interpreter, when the user pushes Cancel button;
wenzelm
parents:
56834
diff
changeset
|
118 |
try { |
69531d86d77e
more sensible interrupt of interpreter, when the user pushes Cancel button;
wenzelm
parents:
56834
diff
changeset
|
119 |
running.change(_ => Some(Thread.currentThread())) |
69531d86d77e
more sensible interrupt of interpreter, when the user pushes Cancel button;
wenzelm
parents:
56834
diff
changeset
|
120 |
interp.interpret(command) |
69531d86d77e
more sensible interrupt of interpreter, when the user pushes Cancel button;
wenzelm
parents:
56834
diff
changeset
|
121 |
} |
69531d86d77e
more sensible interrupt of interpreter, when the user pushes Cancel button;
wenzelm
parents:
56834
diff
changeset
|
122 |
finally { |
69531d86d77e
more sensible interrupt of interpreter, when the user pushes Cancel button;
wenzelm
parents:
56834
diff
changeset
|
123 |
running.change(_ => None) |
71700 | 124 |
Exn.Interrupt.dispose() |
56836
69531d86d77e
more sensible interrupt of interpreter, when the user pushes Cancel button;
wenzelm
parents:
56834
diff
changeset
|
125 |
} |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57609
diff
changeset
|
126 |
GUI_Thread.later { |
56834
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
127 |
if (err != null) err.commandDone() |
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
128 |
out.commandDone() |
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
129 |
} |
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
130 |
true |
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
131 |
} |
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
132 |
} |
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
133 |
} |
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
134 |
|
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
135 |
|
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
136 |
/* jEdit console methods */ |
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
137 |
|
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
138 |
override def openConsole(console: Console) |
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
139 |
{ |
56836
69531d86d77e
more sensible interrupt of interpreter, when the user pushes Cancel button;
wenzelm
parents:
56834
diff
changeset
|
140 |
val interp = new Interpreter |
69531d86d77e
more sensible interrupt of interpreter, when the user pushes Cancel button;
wenzelm
parents:
56834
diff
changeset
|
141 |
interp.thread.send(Start(console)) |
34845 | 142 |
interpreters += (console -> interp) |
34841 | 143 |
} |
144 |
||
145 |
override def closeConsole(console: Console) |
|
146 |
{ |
|
56834
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
147 |
interpreters.get(console) match { |
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
148 |
case Some(interp) => |
56836
69531d86d77e
more sensible interrupt of interpreter, when the user pushes Cancel button;
wenzelm
parents:
56834
diff
changeset
|
149 |
interp.interrupt |
69531d86d77e
more sensible interrupt of interpreter, when the user pushes Cancel button;
wenzelm
parents:
56834
diff
changeset
|
150 |
interp.thread.shutdown |
56834
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
151 |
interpreters -= console |
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
152 |
case None => |
a752f065f3d3
fork Scala interpreter thread, independently of Swing_Thread;
wenzelm
parents:
56833
diff
changeset
|
153 |
} |
34841 | 154 |
} |
155 |
||
34849 | 156 |
override def printInfoMessage(out: Output) |
157 |
{ |
|
158 |
out.print(null, |
|
159 |
"This shell evaluates Isabelle/Scala expressions.\n\n" + |
|
57848 | 160 |
"The contents of package isabelle and isabelle.jedit are imported.\n" + |
34849 | 161 |
"The following special toplevel bindings are provided:\n" + |
50205 | 162 |
" view -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" + |
163 |
" console -- jEdit Console plugin\n" + |
|
55621
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
164 |
" PIDE -- Isabelle/PIDE plugin (e.g. PIDE.session, PIDE.snapshot, PIDE.rendering)\n") |
34849 | 165 |
} |
166 |
||
34841 | 167 |
override def printPrompt(console: Console, out: Output) |
37175 | 168 |
{ |
34844 | 169 |
out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>") |
37175 | 170 |
out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ") |
171 |
} |
|
34841 | 172 |
|
173 |
override def execute(console: Console, input: String, out: Output, err: Output, command: String) |
|
174 |
{ |
|
56836
69531d86d77e
more sensible interrupt of interpreter, when the user pushes Cancel button;
wenzelm
parents:
56834
diff
changeset
|
175 |
interpreters(console).thread.send(Execute(console, out, err, command)) |
34841 | 176 |
} |
34849 | 177 |
|
178 |
override def stop(console: Console) |
|
179 |
{ |
|
56836
69531d86d77e
more sensible interrupt of interpreter, when the user pushes Cancel button;
wenzelm
parents:
56834
diff
changeset
|
180 |
interpreters.get(console).foreach(_.interrupt) |
34849 | 181 |
} |
34841 | 182 |
} |