1/* Title: Tools/jEdit/src/scala_console.scala 2 Author: Makarius 3 4Scala instance of Console plugin. 5*/ 6 7package isabelle.jedit 8 9 10import isabelle._ 11 12import console.{Console, ConsolePane, Shell, Output} 13 14import org.gjt.sp.jedit.{jEdit, JARClassLoader} 15import org.gjt.sp.jedit.MiscUtilities 16 17import java.io.{File => JFile, FileFilter, OutputStream, Writer, PrintWriter} 18 19import scala.tools.nsc.{GenericRunnerSettings, NewLinePrintWriter, ConsoleWriter} 20import scala.tools.nsc.interpreter.IMain 21import scala.collection.mutable 22 23 24class Scala_Console extends Shell("Scala") 25{ 26 /* reconstructed jEdit/plugin classpath */ 27 28 private def reconstruct_classpath(): String = 29 { 30 def find_jars(start: String): List[String] = 31 if (start != null) 32 File.find_files(new JFile(start), file => file.getName.endsWith(".jar")). 33 map(File.absolute_name(_)) 34 else Nil 35 36 val initial_class_path = 37 space_explode(JFile.pathSeparatorChar, System.getProperty("java.class.path", "")) 38 39 val path = 40 initial_class_path ::: 41 find_jars(jEdit.getSettingsDirectory) ::: 42 find_jars(jEdit.getJEditHome) 43 path.mkString(JFile.pathSeparator) 44 } 45 46 47 /* global state -- owned by GUI thread */ 48 49 @volatile private var interpreters = Map.empty[Console, Interpreter] 50 51 @volatile private var global_console: Console = null 52 @volatile private var global_out: Output = null 53 @volatile private var global_err: Output = null 54 55 private val console_stream = new OutputStream 56 { 57 val buf = new StringBuilder(100) 58 59 override def flush() 60 { 61 val s = buf.synchronized { val s = buf.toString; buf.clear; s } 62 val str = UTF8.decode_permissive(s) 63 GUI_Thread.later { 64 if (global_out == null) System.out.print(str) 65 else global_out.writeAttrs(null, str) 66 } 67 Thread.sleep(10) // FIXME adhoc delay to avoid loosing output 68 } 69 70 override def close() { flush () } 71 72 def write(byte: Int) 73 { 74 val c = byte.toChar 75 buf.synchronized { buf.append(c) } 76 if (c == '\n') flush() 77 } 78 } 79 80 private val console_writer = new Writer 81 { 82 def flush() { console_stream.flush() } 83 def close() { console_stream.flush() } 84 85 def write(cbuf: Array[Char], off: Int, len: Int) 86 { 87 if (len > 0) { 88 UTF8.bytes(new String(cbuf.slice(off, off + len))).foreach(console_stream.write(_)) 89 } 90 } 91 } 92 93 private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A = 94 { 95 global_console = console 96 global_out = out 97 global_err = if (err == null) out else err 98 try { 99 scala.Console.withErr(console_stream) { 100 scala.Console.withOut(console_stream) { e } 101 } 102 } 103 finally { 104 console_stream.flush 105 global_console = null 106 global_out = null 107 global_err = null 108 } 109 } 110 111 private def report_error(str: String) 112 { 113 if (global_console == null || global_err == null) isabelle.Output.writeln(str) 114 else GUI_Thread.later { global_err.print(global_console.getErrorColor, str) } 115 } 116 117 118 /* interpreter thread */ 119 120 private abstract class Request 121 private case class Start(console: Console) extends Request 122 private case class Execute(console: Console, out: Output, err: Output, command: String) 123 extends Request 124 125 private class Interpreter 126 { 127 private val running = Synchronized[Option[Thread]](None) 128 def interrupt { running.change(opt => { opt.foreach(_.interrupt); opt }) } 129 130 private val settings = new GenericRunnerSettings(report_error) 131 settings.classpath.value = reconstruct_classpath() 132 133 private val interp = new IMain(settings, new PrintWriter(console_writer, true)) 134 { 135 override def parentClassLoader = new JARClassLoader 136 } 137 interp.setContextClassLoader 138 139 val thread: Consumer_Thread[Request] = Consumer_Thread.fork("Scala_Console") 140 { 141 case Start(console) => 142 interp.bind("view", "org.gjt.sp.jedit.View", console.getView) 143 interp.bind("console", "console.Console", console) 144 interp.interpret("import isabelle._; import isabelle.jedit._") 145 true 146 147 case Execute(console, out, err, command) => 148 with_console(console, out, err) { 149 try { 150 running.change(_ => Some(Thread.currentThread())) 151 interp.interpret(command) 152 } 153 finally { 154 running.change(_ => None) 155 Thread.interrupted 156 } 157 GUI_Thread.later { 158 if (err != null) err.commandDone() 159 out.commandDone() 160 } 161 true 162 } 163 } 164 } 165 166 167 /* jEdit console methods */ 168 169 override def openConsole(console: Console) 170 { 171 val interp = new Interpreter 172 interp.thread.send(Start(console)) 173 interpreters += (console -> interp) 174 } 175 176 override def closeConsole(console: Console) 177 { 178 interpreters.get(console) match { 179 case Some(interp) => 180 interp.interrupt 181 interp.thread.shutdown 182 interpreters -= console 183 case None => 184 } 185 } 186 187 override def printInfoMessage(out: Output) 188 { 189 out.print(null, 190 "This shell evaluates Isabelle/Scala expressions.\n\n" + 191 "The contents of package isabelle and isabelle.jedit are imported.\n" + 192 "The following special toplevel bindings are provided:\n" + 193 " view -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" + 194 " console -- jEdit Console plugin\n" + 195 " PIDE -- Isabelle/PIDE plugin (e.g. PIDE.session, PIDE.snapshot, PIDE.rendering)\n") 196 } 197 198 override def printPrompt(console: Console, out: Output) 199 { 200 out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>") 201 out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ") 202 } 203 204 override def execute(console: Console, input: String, out: Output, err: Output, command: String) 205 { 206 interpreters(console).thread.send(Execute(console, out, err, command)) 207 } 208 209 override def stop(console: Console) 210 { 211 interpreters.get(console).foreach(_.interrupt) 212 } 213} 214