diff --git a/src/Pure/System/scala.scala b/src/Pure/System/scala.scala --- a/src/Pure/System/scala.scala +++ b/src/Pure/System/scala.scala @@ -1,183 +1,196 @@ /* Title: Pure/System/scala.scala Author: Makarius Support for Scala at runtime. */ package isabelle import java.lang.reflect.{Modifier, InvocationTargetException} import java.io.{File => JFile, StringWriter, PrintWriter} import scala.util.matching.Regex -import scala.tools.nsc.GenericRunnerSettings +import scala.tools.nsc.{GenericRunnerSettings, ConsoleWriter, NewLinePrintWriter} import scala.tools.nsc.interpreter.IMain object Scala { /* compiler */ object Compiler { - def classpath(jar_dirs: List[JFile]): String = + def context( + error: String => Unit = Exn.error, + jar_dirs: List[JFile] = Nil): Context = { def find_jars(dir: JFile): List[String] = File.find_files(dir, file => file.getName.endsWith(".jar")). map(File.absolute_name) val class_path = for { prop <- List("scala.boot.class.path", "java.class.path") path = System.getProperty(prop, "") if path != "\"\"" elem <- space_explode(JFile.pathSeparatorChar, path) } yield elem - (class_path ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator) - } - - type Settings = scala.tools.nsc.Settings + val settings = new GenericRunnerSettings(error) + settings.classpath.value = + (class_path ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator) - def settings( - error: String => Unit = Exn.error, - jar_dirs: List[JFile] = Nil): Settings = - { - val settings = new GenericRunnerSettings(error) - settings.classpath.value = classpath(jar_dirs) - settings + new Context(settings) } - def toplevel(settings: Settings, source: String): List[String] = + def default_print_writer: PrintWriter = + new NewLinePrintWriter(new ConsoleWriter, true) + + class Context private [Compiler](val settings: GenericRunnerSettings) { - val out = new StringWriter - val interp = new IMain(settings, new PrintWriter(out)) - val rep = new interp.ReadEvalPrint - val ok = interp.withLabel("\u0001") { rep.compile(source) } - out.close + def interpreter( + print_writer: PrintWriter = default_print_writer, + class_loader: ClassLoader = null): IMain = + { + new IMain(settings, print_writer) + { + override def parentClassLoader: ClassLoader = + if (class_loader == null) super.parentClassLoader + else class_loader + } + } - val Error = """(?s)^\S* error: (.*)$""".r - val errors = - space_explode('\u0001', Library.strip_ansi_color(out.toString)). - collect({ case Error(msg) => "Scala error: " + Library.trim_line(msg) }) + def toplevel(source: String): List[String] = + { + val out = new StringWriter + val interp = interpreter(new PrintWriter(out)) + val rep = new interp.ReadEvalPrint + val ok = interp.withLabel("\u0001") { rep.compile(source) } + out.close - if (!ok && errors.isEmpty) List("Error") else errors + val Error = """(?s)^\S* error: (.*)$""".r + val errors = + space_explode('\u0001', Library.strip_ansi_color(out.toString)). + collect({ case Error(msg) => "Scala error: " + Library.trim_line(msg) }) + + if (!ok && errors.isEmpty) List("Error") else errors + } } } /** invoke JVM method via Isabelle/Scala **/ /* method reflection */ private val Ext = new Regex("(.*)\\.([^.]*)") private val STRING = Class.forName("java.lang.String") private def get_method(name: String): String => String = name match { case Ext(class_name, method_name) => val m = try { Class.forName(class_name).getMethod(method_name, STRING) } catch { case _: ClassNotFoundException | _: NoSuchMethodException => error("No such method: " + quote(name)) } if (!Modifier.isStatic(m.getModifiers)) error("Not at static method: " + m.toString) if (m.getReturnType != STRING) error("Bad method return type: " + m.toString) (arg: String) => { try { m.invoke(null, arg).asInstanceOf[String] } catch { case e: InvocationTargetException if e.getCause != null => throw e.getCause } } case _ => error("Malformed method name: " + quote(name)) } /* method invocation */ object Tag extends Enumeration { val NULL, OK, ERROR, FAIL, INTERRUPT = Value } def method(name: String, arg: String): (Tag.Value, String) = Exn.capture { get_method(name) } match { case Exn.Res(f) => Exn.capture { f(arg) } match { case Exn.Res(null) => (Tag.NULL, "") case Exn.Res(res) => (Tag.OK, res) case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, "") case Exn.Exn(e) => (Tag.ERROR, Exn.message(e)) } case Exn.Exn(e) => (Tag.FAIL, Exn.message(e)) } } /* protocol handler */ class Scala extends Session.Protocol_Handler { private var session: Session = null private var futures = Map.empty[String, Future[Unit]] override def init(init_session: Session): Unit = synchronized { session = init_session } override def exit(): Unit = synchronized { for ((id, future) <- futures) cancel(id, future) futures = Map.empty } private def fulfill(id: String, tag: Scala.Tag.Value, res: String): Unit = synchronized { if (futures.isDefinedAt(id)) { session.protocol_command("Scala.fulfill", id, tag.id.toString, res) futures -= id } } private def cancel(id: String, future: Future[Unit]) { future.cancel fulfill(id, Scala.Tag.INTERRUPT, "") } private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized { msg.properties match { case Markup.Invoke_Scala(name, id) => futures += (id -> Future.fork { val (tag, result) = Scala.method(name, msg.text) fulfill(id, tag, result) }) true case _ => false } } private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized { msg.properties match { case Markup.Cancel_Scala(id) => futures.get(id) match { case Some(future) => cancel(id, future) case None => } true case _ => false } } val functions = List( Markup.Invoke_Scala.name -> invoke_scala, Markup.Cancel_Scala.name -> cancel_scala) } diff --git a/src/Tools/jEdit/src/scala_console.scala b/src/Tools/jEdit/src/scala_console.scala --- a/src/Tools/jEdit/src/scala_console.scala +++ b/src/Tools/jEdit/src/scala_console.scala @@ -1,185 +1,182 @@ /* Title: Tools/jEdit/src/scala_console.scala Author: Makarius Scala instance of Console plugin. */ package isabelle.jedit import isabelle._ import console.{Console, ConsolePane, Shell, Output} import org.gjt.sp.jedit.JARClassLoader import java.io.{OutputStream, Writer, PrintWriter} -import scala.tools.nsc.interpreter.IMain class Scala_Console extends Shell("Scala") { /* global state -- owned by GUI thread */ @volatile private var interpreters = Map.empty[Console, Interpreter] @volatile private var global_console: Console = null @volatile private var global_out: Output = null @volatile private var global_err: Output = null private val console_stream = new OutputStream { val buf = new StringBuilder(100) override def flush() { val s = buf.synchronized { val s = buf.toString; buf.clear; s } val str = UTF8.decode_permissive(s) GUI_Thread.later { if (global_out == null) System.out.print(str) else global_out.writeAttrs(null, str) } Time.seconds(0.01).sleep // FIXME adhoc delay to avoid loosing output } override def close() { flush () } def write(byte: Int) { val c = byte.toChar buf.synchronized { buf.append(c) } if (c == '\n') flush() } } private val console_writer = new Writer { def flush() { console_stream.flush() } def close() { console_stream.flush() } def write(cbuf: Array[Char], off: Int, len: Int) { if (len > 0) { UTF8.bytes(new String(cbuf.slice(off, off + len))).foreach(console_stream.write(_)) } } } private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A = { global_console = console global_out = out global_err = if (err == null) out else err try { scala.Console.withErr(console_stream) { scala.Console.withOut(console_stream) { e } } } finally { console_stream.flush global_console = null global_out = null global_err = null } } private def report_error(str: String) { if (global_console == null || global_err == null) isabelle.Output.writeln(str) else GUI_Thread.later { global_err.print(global_console.getErrorColor, str) } } /* interpreter thread */ private abstract class Request private case class Start(console: Console) extends Request private case class Execute(console: Console, out: Output, err: Output, command: String) extends Request private class Interpreter { private val running = Synchronized[Option[Thread]](None) def interrupt { running.change(opt => { opt.foreach(_.interrupt); opt }) } - private val settings = - Scala.Compiler.settings(error = report_error, jar_dirs = JEdit_Lib.directories) - - private val interp = new IMain(settings, new PrintWriter(console_writer, true)) - { - override def parentClassLoader = new JARClassLoader - } + private val interp = + Scala.Compiler.context(error = report_error, jar_dirs = JEdit_Lib.directories). + interpreter( + print_writer = new PrintWriter(console_writer, true), + class_loader = new JARClassLoader) val thread: Consumer_Thread[Request] = Consumer_Thread.fork("Scala_Console") { case Start(console) => interp.bind("view", "org.gjt.sp.jedit.View", console.getView) interp.bind("console", "console.Console", console) interp.interpret("import isabelle._; import isabelle.jedit._") true case Execute(console, out, err, command) => with_console(console, out, err) { try { running.change(_ => Some(Thread.currentThread())) interp.interpret(command) } finally { running.change(_ => None) Exn.Interrupt.dispose() } GUI_Thread.later { if (err != null) err.commandDone() out.commandDone() } true } } } /* jEdit console methods */ override def openConsole(console: Console) { val interp = new Interpreter interp.thread.send(Start(console)) interpreters += (console -> interp) } override def closeConsole(console: Console) { interpreters.get(console) match { case Some(interp) => interp.interrupt interp.thread.shutdown interpreters -= console case None => } } override def printInfoMessage(out: Output) { out.print(null, "This shell evaluates Isabelle/Scala expressions.\n\n" + "The contents of package isabelle and isabelle.jedit are imported.\n" + "The following special toplevel bindings are provided:\n" + " view -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" + " console -- jEdit Console plugin\n" + " PIDE -- Isabelle/PIDE plugin (e.g. PIDE.session, PIDE.snapshot, PIDE.rendering)\n") } override def printPrompt(console: Console, out: Output) { out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>") out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ") } override def execute(console: Console, input: String, out: Output, err: Output, command: String) { interpreters(console).thread.send(Execute(console, out, err, command)) } override def stop(console: Console) { interpreters.get(console).foreach(_.interrupt) } }