10 import console.{Console, ConsolePane, Shell, Output} |
10 import console.{Console, ConsolePane, Shell, Output} |
11 |
11 |
12 import org.gjt.sp.jedit.{jEdit, JARClassLoader} |
12 import org.gjt.sp.jedit.{jEdit, JARClassLoader} |
13 import org.gjt.sp.jedit.MiscUtilities |
13 import org.gjt.sp.jedit.MiscUtilities |
14 |
14 |
15 import java.io.{File, Writer, PrintWriter} |
15 import java.io.{File, OutputStream, Writer, PrintWriter} |
16 |
16 |
17 import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter} |
17 import scala.tools.nsc.{Interpreter, GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter} |
18 import scala.collection.mutable |
18 import scala.collection.mutable |
19 |
19 |
20 |
20 |
21 class Scala_Console extends Shell("Scala") |
21 class Scala_Console extends Shell("Scala") |
22 { |
22 { |
|
23 /* reconstructed jEdit/plugin classpath */ |
|
24 |
|
25 private def reconstruct_classpath(): String = |
|
26 { |
|
27 def find_jars(start: String): List[String] = |
|
28 if (start != null) |
|
29 Standard_System.find_files(new File(start), |
|
30 entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath) |
|
31 else Nil |
|
32 val path = find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome) |
|
33 path.mkString(File.pathSeparator) |
|
34 } |
|
35 |
|
36 |
23 /* global state -- owned by Swing thread */ |
37 /* global state -- owned by Swing thread */ |
24 |
38 |
25 private var interpreters = Map[Console, Interpreter]() |
39 private var interpreters = Map[Console, Interpreter]() |
26 |
40 |
27 private var global_console: Console = null |
41 private var global_console: Console = null |
28 private var global_out: Output = null |
42 private var global_out: Output = null |
29 private var global_err: Output = null |
43 private var global_err: Output = null |
30 |
44 |
|
45 private val console_stream = new OutputStream |
|
46 { |
|
47 val buf = new StringBuilder |
|
48 override def flush() |
|
49 { |
|
50 val str = Standard_System.decode_permissive_utf8(buf.toString) |
|
51 buf.clear |
|
52 if (global_out == null) System.out.print(str) |
|
53 else Swing_Thread.now { global_out.writeAttrs(null, str) } |
|
54 } |
|
55 override def close() { flush () } |
|
56 def write(byte: Int) { buf.append(byte.toChar) } |
|
57 } |
|
58 |
|
59 private val console_writer = new Writer |
|
60 { |
|
61 def flush() {} |
|
62 def close() {} |
|
63 |
|
64 def write(cbuf: Array[Char], off: Int, len: Int) |
|
65 { |
|
66 if (len > 0) write(new String(cbuf.subArray(off, off + len))) |
|
67 } |
|
68 |
|
69 override def write(str: String) |
|
70 { |
|
71 if (global_out == null) System.out.println(str) |
|
72 else global_out.print(null, str) |
|
73 } |
|
74 } |
|
75 |
31 private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A = |
76 private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A = |
32 { |
77 { |
33 global_console = console |
78 global_console = console |
34 global_out = out |
79 global_out = out |
35 global_err = if (err == null) out else err |
80 global_err = if (err == null) out else err |
36 val res = Exn.capture { e } |
81 val res = Exn.capture { scala.Console.withOut(console_stream)(e) } |
|
82 console_stream.flush |
37 global_console = null |
83 global_console = null |
38 global_out = null |
84 global_out = null |
39 global_err = null |
85 global_err = null |
40 Exn.release(res) |
86 Exn.release(res) |
41 } |
87 } |
42 |
88 |
43 private def report_error(str: String) |
89 private def report_error(str: String) |
44 { |
90 { |
45 if (global_console == null || global_err == null) System.err.println(str) |
91 if (global_console == null || global_err == null) System.err.println(str) |
46 else global_err.print(global_console.getErrorColor, str) |
92 else Swing_Thread.now { global_err.print(global_console.getErrorColor, str) } |
47 } |
93 } |
48 |
94 |
49 private def construct_classpath(): String = |
|
50 { |
|
51 def find_jars(start: String): List[String] = |
|
52 if (start != null) |
|
53 Standard_System.find_files(new File(start), |
|
54 entry => entry.isFile && entry.getName.endsWith(".jar")).map(_.getAbsolutePath) |
|
55 else Nil |
|
56 val path = |
|
57 (jEdit.getJEditHome + File.separator + "jedit.jar") :: |
|
58 (find_jars(jEdit.getSettingsDirectory) ::: find_jars(jEdit.getJEditHome)) |
|
59 path.mkString(File.pathSeparator) |
|
60 } |
|
61 |
95 |
62 private class Console_Writer extends Writer |
96 /* jEdit console methods */ |
63 { |
|
64 def close {} |
|
65 def flush {} |
|
66 |
|
67 override def write(str: String) |
|
68 { |
|
69 if (global_out == null) System.out.println(str) |
|
70 else global_out.print(null, str) |
|
71 } |
|
72 |
|
73 def write(cbuf: Array[Char], off: Int, len: Int) |
|
74 { |
|
75 if (len > 0) write(new String(cbuf.subArray(off, off + len))) |
|
76 } |
|
77 } |
|
78 |
97 |
79 override def openConsole(console: Console) |
98 override def openConsole(console: Console) |
80 { |
99 { |
81 val settings = new GenericRunnerSettings(report_error) |
100 val settings = new GenericRunnerSettings(report_error) |
82 settings.classpath.value = construct_classpath() |
101 settings.classpath.value = reconstruct_classpath() |
83 val printer = new PrintWriter(new Console_Writer, true) |
|
84 |
102 |
85 val interp = new Interpreter(settings, printer) |
103 val interp = new Interpreter(settings, new PrintWriter(console_writer, true)) |
86 { |
104 { |
87 override def parentClassLoader = new JARClassLoader |
105 override def parentClassLoader = new JARClassLoader |
88 } |
106 } |
89 interp.setContextClassLoader |
107 interp.setContextClassLoader |
90 interp.bind("view", "org.gjt.sp.jedit.View", console.getView) |
108 interp.bind("view", "org.gjt.sp.jedit.View", console.getView) |
91 interp.bind("session", "isabelle.proofdocument.Session", Isabelle.session) |
109 interp.bind("session", "isabelle.proofdocument.Session", Isabelle.session) |
|
110 |
92 interpreters += (console -> interp) |
111 interpreters += (console -> interp) |
93 } |
112 } |
94 |
113 |
95 override def closeConsole(console: Console) |
114 override def closeConsole(console: Console) |
96 { |
115 { |