clarified management of interpreter threads: more generic;
avoid interp.bind, which is unavailable in scala3;
--- a/src/Pure/System/scala.scala Thu Apr 21 11:49:53 2022 +0200
+++ b/src/Pure/System/scala.scala Fri Apr 22 10:11:06 2022 +0200
@@ -152,6 +152,66 @@
+ /** interpreter thread **/
+
+ object Interpreter {
+ /* requests */
+
+ sealed abstract class Request
+ case class Execute(command: Compiler.Context => Unit) extends Request
+ case object Shutdown extends Request
+
+
+ /* known interpreters */
+
+ private val known = Synchronized(Set.empty[Interpreter])
+
+ def add(interpreter: Interpreter): Unit = known.change(_ + interpreter)
+ def del(interpreter: Interpreter): Unit = known.change(_ - interpreter)
+
+ def get[A](which: PartialFunction[Interpreter, A]): Option[A] =
+ known.value.collectFirst(which)
+ }
+
+ class Interpreter(context: Compiler.Context) {
+ interpreter =>
+
+ private val running = Synchronized[Option[Thread]](None)
+ def running_thread(thread: Thread): Boolean = running.value.contains(thread)
+ def interrupt_thread(): Unit = running.change({ opt => opt.foreach(_.interrupt()); opt })
+
+ private lazy val thread: Consumer_Thread[Interpreter.Request] =
+ Consumer_Thread.fork("Scala.Interpreter") {
+ case Interpreter.Execute(command) =>
+ try {
+ running.change(_ => Some(Thread.currentThread()))
+ command(context)
+ }
+ finally {
+ running.change(_ => None)
+ Exn.Interrupt.dispose()
+ }
+ true
+ case Interpreter.Shutdown =>
+ Interpreter.del(interpreter)
+ false
+ }
+
+ def shutdown(): Unit = {
+ thread.send(Interpreter.Shutdown)
+ interrupt_thread()
+ thread.shutdown()
+ }
+
+ def execute(command: Compiler.Context => Unit): Unit =
+ thread.send(Interpreter.Execute(command))
+
+ Interpreter.add(interpreter)
+ thread
+ }
+
+
+
/** invoke Scala functions from ML **/
/* invoke function */
--- a/src/Tools/jEdit/jedit_main/scala_console.scala Thu Apr 21 11:49:53 2022 +0200
+++ b/src/Tools/jEdit/jedit_main/scala_console.scala Fri Apr 22 10:11:06 2022 +0200
@@ -15,11 +15,32 @@
import java.io.{OutputStream, Writer, PrintWriter}
+object Scala_Console {
+ class Interpreter(context: Scala.Compiler.Context, val console: Console)
+ extends Scala.Interpreter(context)
+
+ def console_interpreter(console: Console): Option[Interpreter] =
+ Scala.Interpreter.get { case int: Interpreter if int.console == console => int }
+
+ def running_interpreter(): Interpreter = {
+ val self = Thread.currentThread()
+ Scala.Interpreter.get { case int: Interpreter if int.running_thread(self) => int }
+ .getOrElse(error("Bad Scala interpreter thread"))
+ }
+
+ def running_console(): Console = running_interpreter().console
+
+ val init = """
+import isabelle._
+import isabelle.jedit._
+val console = isabelle.jedit_main.Scala_Console.running_console()
+val view = console.getView()
+"""
+}
+
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
@@ -80,68 +101,22 @@
}
- /* 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(): Unit = running.change({ opt => opt.foreach(_.interrupt()); opt })
-
- private val interp =
- Scala.Compiler.context(
- print_writer = new PrintWriter(console_writer, true),
- error = report_error,
- jar_dirs = JEdit_Lib.directories,
- class_loader = Some(new JARClassLoader)).interp
-
- 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): Unit = {
- val interp = new Interpreter
- interp.thread.send(Start(console))
- interpreters += (console -> interp)
+ val context =
+ Scala.Compiler.context(
+ print_writer = new PrintWriter(console_writer, true),
+ error = report_error,
+ jar_dirs = JEdit_Lib.directories,
+ class_loader = Some(new JARClassLoader))
+
+ val interpreter = new Scala_Console.Interpreter(context, console)
+ interpreter.execute(_.interp.interpret(Scala_Console.init))
}
- override def closeConsole(console: Console): Unit = {
- interpreters.get(console) match {
- case Some(interp) =>
- interp.interrupt()
- interp.thread.shutdown()
- interpreters -= console
- case None =>
- }
- }
+ override def closeConsole(console: Console): Unit =
+ Scala_Console.console_interpreter(console).foreach(_.shutdown())
override def printInfoMessage(out: Output): Unit = {
out.print(null,
@@ -162,11 +137,19 @@
console: Console,
input: String,
out: Output,
- err: Output, command: String
+ err: Output,
+ command: String
): Unit = {
- interpreters(console).thread.send(Execute(console, out, err, command))
+ Scala_Console.console_interpreter(console).foreach(interpreter =>
+ interpreter.execute { context =>
+ with_console(console, out, err) { context.interp.interpret(command) }
+ GUI_Thread.later {
+ Option(err).foreach(_.commandDone())
+ out.commandDone()
+ }
+ })
}
override def stop(console: Console): Unit =
- interpreters.get(console).foreach(_.interrupt())
+ Scala_Console.console_interpreter(console).foreach(_.shutdown())
}