# HG changeset patch
# User wenzelm
# Date 1650615066 -7200
# Node ID 331f96a67924628cb93f7d844ac71f6ec288ac1b
# Parent  d6f2fbdc6322841f9fa9701da570abfab9d0a0b3
clarified management of interpreter threads: more generic;
avoid interp.bind, which is unavailable in scala3;

diff -r d6f2fbdc6322 -r 331f96a67924 src/Pure/System/scala.scala
--- 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 */
diff -r d6f2fbdc6322 -r 331f96a67924 src/Tools/jEdit/jedit_main/scala_console.scala
--- 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())
 }