# HG changeset patch
# User wenzelm
# Date 1650616298 -7200
# Node ID df9d869cd5fd5883440f19953667ffcaf76304eb
# Parent  a36a1cc0144c7ef49b9b0c43381c1872d474d21c# Parent  331f96a67924628cb93f7d844ac71f6ec288ac1b
merged

diff -r a36a1cc0144c -r df9d869cd5fd src/Pure/ML/ml_statistics.scala
--- a/src/Pure/ML/ml_statistics.scala	Wed Apr 13 16:53:46 2022 +0200
+++ b/src/Pure/ML/ml_statistics.scala	Fri Apr 22 10:31:38 2022 +0200
@@ -103,7 +103,8 @@
       }
     }
 
-    override val functions = List(Markup.ML_Statistics.name -> ml_statistics)
+    override val functions: Session.Protocol_Functions =
+      List(Markup.ML_Statistics.name -> ml_statistics)
   }
 
 
diff -r a36a1cc0144c -r df9d869cd5fd src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Wed Apr 13 16:53:46 2022 +0200
+++ b/src/Pure/PIDE/session.scala	Fri Apr 22 10:31:38 2022 +0200
@@ -106,11 +106,12 @@
   /* protocol handlers */
 
   type Protocol_Function = Prover.Protocol_Output => Boolean
+  type Protocol_Functions = List[(String, Protocol_Function)]
 
   abstract class Protocol_Handler extends Isabelle_System.Service {
     def init(session: Session): Unit = {}
     def exit(): Unit = {}
-    def functions: List[(String, Protocol_Function)] = Nil
+    def functions: Protocol_Functions = Nil
     def prover_options(options: Options): Options = options
   }
 }
diff -r a36a1cc0144c -r df9d869cd5fd src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Wed Apr 13 16:53:46 2022 +0200
+++ b/src/Pure/PIDE/xml.scala	Fri Apr 22 10:31:38 2022 +0200
@@ -333,7 +333,7 @@
 
   object Decode {
     type T[A] = XML.Body => A
-    type V[A] = (List[String], XML.Body) => A
+    type V[A] = PartialFunction[(List[String], XML.Body), A]
     type P[A] = PartialFunction[List[String], A]
 
 
diff -r a36a1cc0144c -r df9d869cd5fd src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Wed Apr 13 16:53:46 2022 +0200
+++ b/src/Pure/System/isabelle_system.scala	Fri Apr 22 10:31:38 2022 +0200
@@ -143,19 +143,22 @@
 
   /* scala functions */
 
-  private def apply_paths(args: List[String], fun: List[Path] => Unit): List[String] = {
+  private def apply_paths(
+    args: List[String],
+    fun: PartialFunction[List[Path], Unit]
+  ): List[String] = {
     fun(args.map(Path.explode))
     Nil
   }
 
   private def apply_paths1(args: List[String], fun: Path => Unit): List[String] =
-    apply_paths(args, { case List(path) => fun(path) case _ => ??? })
+    apply_paths(args, { case List(path) => fun(path) })
 
   private def apply_paths2(args: List[String], fun: (Path, Path) => Unit): List[String] =
-    apply_paths(args, { case List(path1, path2) => fun(path1, path2) case _ => ??? })
+    apply_paths(args, { case List(path1, path2) => fun(path1, path2) })
 
   private def apply_paths3(args: List[String], fun: (Path, Path, Path) => Unit): List[String] =
-    apply_paths(args, { case List(path1, path2, path3) => fun(path1, path2, path3) case _ => ??? })
+    apply_paths(args, { case List(path1, path2, path3) => fun(path1, path2, path3) })
 
 
   /* permissions */
@@ -481,7 +484,7 @@
   object Download extends Scala.Fun("download", thread = true) {
     val here = Scala_Project.here
     override def invoke(args: List[Bytes]): List[Bytes] =
-      args match { case List(url) => List(download(url.text).bytes) case _ => ??? }
+      args.map(url => download(url.text).bytes)
   }
 
 
diff -r a36a1cc0144c -r df9d869cd5fd src/Pure/System/scala.scala
--- a/src/Pure/System/scala.scala	Wed Apr 13 16:53:46 2022 +0200
+++ b/src/Pure/System/scala.scala	Fri Apr 22 10:31:38 2022 +0200
@@ -80,9 +80,14 @@
     } yield elem
 
   object Compiler {
+    def default_print_writer: PrintWriter =
+      new NewLinePrintWriter(new ConsoleWriter, true)
+
     def context(
+      print_writer: PrintWriter = default_print_writer,
       error: String => Unit = Exn.error,
-      jar_dirs: List[JFile] = Nil
+      jar_dirs: List[JFile] = Nil,
+      class_loader: Option[ClassLoader] = None
     ): Context = {
       def find_jars(dir: JFile): List[String] =
         File.find_files(dir, file => file.getName.endsWith(".jar")).
@@ -92,44 +97,40 @@
       settings.classpath.value =
         (class_path() ::: jar_dirs.flatMap(find_jars)).mkString(JFile.pathSeparator)
 
-      new Context(settings)
+      new Context(settings, print_writer, class_loader)
     }
 
-    def default_print_writer: PrintWriter =
-      new NewLinePrintWriter(new ConsoleWriter, true)
-
-    class Context private [Compiler](val settings: GenericRunnerSettings) {
+    class Context private [Compiler](
+      val settings: GenericRunnerSettings,
+      val print_writer: PrintWriter,
+      val class_loader: Option[ClassLoader]
+    ) {
       override def toString: String = settings.toString
 
-      def interpreter(
-        print_writer: PrintWriter = default_print_writer,
-        class_loader: ClassLoader = null
-      ): IMain = {
+      val interp: IMain =
         new IMain(settings, new ReplReporterImpl(settings, print_writer)) {
           override def parentClassLoader: ClassLoader =
-            if (class_loader == null) super.parentClassLoader
-            else class_loader
+            class_loader getOrElse super.parentClassLoader
         }
-      }
+    }
 
-      def toplevel(interpret: Boolean, source: String): List[String] = {
-        val out = new StringWriter
-        val interp = interpreter(new PrintWriter(out))
-        val marker = '\u000b'
-        val ok =
-          interp.withLabel(marker.toString) {
-            if (interpret) interp.interpret(source) == Results.Success
-            else (new interp.ReadEvalPrint).compile(source)
-          }
-        out.close()
+    def toplevel(interpret: Boolean, source: String): List[String] = {
+      val out = new StringWriter
+      val interp = Compiler.context(print_writer = new PrintWriter(out)).interp
+      val marker = '\u000b'
+      val ok =
+        interp.withLabel(marker.toString) {
+          if (interpret) interp.interpret(source) == Results.Success
+          else (new interp.ReadEvalPrint).compile(source)
+        }
+      out.close()
 
-        val Error = """(?s)^\S* error: (.*)$""".r
-        val errors =
-          space_explode(marker, Library.strip_ansi_color(out.toString)).
-            collect({ case Error(msg) => "Scala error: " + Library.trim_line(msg) })
+      val Error = """(?s)^\S* error: (.*)$""".r
+      val errors =
+        space_explode(marker, Library.strip_ansi_color(out.toString)).
+          collect({ case Error(msg) => "Scala error: " + Library.trim_line(msg) })
 
-        if (!ok && errors.isEmpty) List("Error") else errors
-      }
+      if (!ok && errors.isEmpty) List("Error") else errors
     }
   }
 
@@ -143,7 +144,7 @@
           case body => import XML.Decode._; pair(bool, string)(body)
         }
       val errors =
-        try { Compiler.context().toplevel(interpret, source) }
+        try { Compiler.toplevel(interpret, source) }
         catch { case ERROR(msg) => List(msg) }
       locally { import XML.Encode._; YXML.string_of_body(list(string)(errors)) }
     }
@@ -151,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 */
@@ -208,15 +269,15 @@
     private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized {
       msg.properties match {
         case Markup.Invoke_Scala(name, id) =>
-          def body: Unit = {
+          def body(): Unit = {
             val (tag, res) = Scala.function_body(name, msg.chunks)
             result(id, tag, res)
           }
           val future =
             if (Scala.function_thread(name)) {
-              Future.thread(name = Isabelle_Thread.make_name(base = "invoke_scala"))(body)
+              Future.thread(name = Isabelle_Thread.make_name(base = "invoke_scala"))(body())
             }
-            else Future.fork(body)
+            else Future.fork(body())
           futures += (id -> future)
           true
         case _ => false
@@ -235,7 +296,7 @@
       }
     }
 
-    override val functions =
+    override val functions: Session.Protocol_Functions =
       List(
         Markup.Invoke_Scala.name -> invoke_scala,
         Markup.Cancel_Scala.name -> cancel_scala)
diff -r a36a1cc0144c -r df9d869cd5fd src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Wed Apr 13 16:53:46 2022 +0200
+++ b/src/Pure/Thy/export_theory.scala	Fri Apr 22 10:31:38 2022 +0200
@@ -264,13 +264,12 @@
 
   def decode_syntax: XML.Decode.T[Syntax] =
     XML.Decode.variant(List(
-      { case (Nil, Nil) => No_Syntax case _ => ??? },
-      { case (List(delim), Nil) => Prefix(delim) case _ => ??? },
+      { case (Nil, Nil) => No_Syntax },
+      { case (List(delim), Nil) => Prefix(delim) },
       { case (Nil, body) =>
           import XML.Decode._
           val (ass, delim, pri) = triple(int, string, int)(body)
-          Infix(Assoc(ass), delim, pri)
-        case _ => ??? }))
+          Infix(Assoc(ass), delim, pri) }))
 
 
   /* types */
@@ -685,11 +684,11 @@
   val decode_recursion: XML.Decode.T[Recursion] = {
     import XML.Decode._
     variant(List(
-      { case (Nil, a) => Primrec(list(string)(a)) case _ => ??? },
-      { case (Nil, Nil) => Recdef case _ => ??? },
-      { case (Nil, a) => Primcorec(list(string)(a)) case _ => ??? },
-      { case (Nil, Nil) => Corec case _ => ??? },
-      { case (Nil, Nil) => Unknown_Recursion case _ => ??? }))
+      { case (Nil, a) => Primrec(list(string)(a)) },
+      { case (Nil, Nil) => Recdef },
+      { case (Nil, a) => Primcorec(list(string)(a)) },
+      { case (Nil, Nil) => Corec },
+      { case (Nil, Nil) => Unknown_Recursion }))
   }
 
 
@@ -714,10 +713,10 @@
   val decode_rough_classification: XML.Decode.T[Rough_Classification] = {
     import XML.Decode._
     variant(List(
-      { case (Nil, a) => Equational(decode_recursion(a)) case _ => ??? },
-      { case (Nil, Nil) => Inductive case _ => ??? },
-      { case (Nil, Nil) => Co_Inductive case _ => ??? },
-      { case (Nil, Nil) => Unknown case _ => ??? }))
+      { case (Nil, a) => Equational(decode_recursion(a)) },
+      { case (Nil, Nil) => Inductive },
+      { case (Nil, Nil) => Co_Inductive },
+      { case (Nil, Nil) => Unknown }))
   }
 
 
diff -r a36a1cc0144c -r df9d869cd5fd src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Wed Apr 13 16:53:46 2022 +0200
+++ b/src/Pure/Tools/build_job.scala	Fri Apr 22 10:31:38 2022 +0200
@@ -321,7 +321,7 @@
               case _ => false
             }
 
-          override val functions =
+          override val functions: Session.Protocol_Functions =
             List(
               Markup.Build_Session_Finished.name -> build_session_finished,
               Markup.Loading_Theory.name -> loading_theory,
@@ -463,10 +463,10 @@
 
       val result = {
         val theory_timing =
-          theory_timings.iterator.map(
+          theory_timings.iterator.flatMap(
             {
-              case props @ Markup.Name(name) => name -> props
-              case _ => ???
+              case props @ Markup.Name(name) => Some(name -> props)
+              case _ => None
             }).toMap
         val used_theory_timings =
           for { (name, _) <- deps(session_name).used_theories }
diff -r a36a1cc0144c -r df9d869cd5fd src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Wed Apr 13 16:53:46 2022 +0200
+++ b/src/Pure/Tools/debugger.scala	Fri Apr 22 10:31:38 2022 +0200
@@ -133,7 +133,7 @@
       }
     }
 
-    override val functions =
+    override val functions: Session.Protocol_Functions =
       List(
         Markup.DEBUGGER_STATE -> debugger_state,
         Markup.DEBUGGER_OUTPUT -> debugger_output)
diff -r a36a1cc0144c -r df9d869cd5fd src/Pure/Tools/print_operation.scala
--- a/src/Pure/Tools/print_operation.scala	Wed Apr 13 16:53:46 2022 +0200
+++ b/src/Pure/Tools/print_operation.scala	Fri Apr 22 10:31:38 2022 +0200
@@ -34,6 +34,7 @@
       true
     }
 
-    override val functions = List(Markup.PRINT_OPERATIONS -> put)
+    override val functions: Session.Protocol_Functions =
+      List(Markup.PRINT_OPERATIONS -> put)
   }
 }
diff -r a36a1cc0144c -r df9d869cd5fd src/Pure/Tools/simplifier_trace.scala
--- a/src/Pure/Tools/simplifier_trace.scala	Wed Apr 13 16:53:46 2022 +0200
+++ b/src/Pure/Tools/simplifier_trace.scala	Fri Apr 22 10:31:38 2022 +0200
@@ -313,6 +313,7 @@
           false
       }
 
-    override val functions = List(Markup.SIMP_TRACE_CANCEL -> cancel)
+    override val functions: Session.Protocol_Functions =
+      List(Markup.SIMP_TRACE_CANCEL -> cancel)
   }
 }
diff -r a36a1cc0144c -r df9d869cd5fd src/Pure/term_xml.scala
--- a/src/Pure/term_xml.scala	Wed Apr 13 16:53:46 2022 +0200
+++ b/src/Pure/term_xml.scala	Fri Apr 22 10:31:38 2022 +0200
@@ -48,20 +48,20 @@
 
     def typ: T[Typ] =
       variant[Typ](List(
-        { case (List(a), b) => Type(a, list(typ)(b)) case _ => ??? },
-        { case (List(a), b) => TFree(a, sort(b)) case _ => ??? },
+        { case (List(a), b) => Type(a, list(typ)(b)) },
+        { case (List(a), b) => TFree(a, sort(b)) },
         { case (a, b) => TVar(indexname(a), sort(b)) }))
 
     val typ_body: T[Typ] = { case Nil => dummyT case body => typ(body) }
 
     def term: T[Term] =
       variant[Term](List(
-        { case (List(a), b) => Const(a, list(typ)(b)) case _ => ??? },
-        { case (List(a), b) => Free(a, typ_body(b)) case _ => ??? },
+        { case (List(a), b) => Const(a, list(typ)(b)) },
+        { case (List(a), b) => Free(a, typ_body(b)) },
         { case (a, b) => Var(indexname(a), typ_body(b)) },
-        { case (Nil, a) => Bound(int(a)) case _ => ??? },
-        { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) case _ => ??? },
-        { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) case _ => ??? }))
+        { case (Nil, a) => Bound(int(a)) },
+        { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
+        { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
 
     def term_env(env: Map[String, Typ]): T[Term] = {
       def env_type(x: String, t: Typ): Typ =
@@ -69,12 +69,12 @@
 
       def term: T[Term] =
         variant[Term](List(
-          { case (List(a), b) => Const(a, list(typ)(b)) case _ => ??? },
-          { case (List(a), b) => Free(a, env_type(a, typ_body(b))) case _ => ??? },
+          { case (List(a), b) => Const(a, list(typ)(b)) },
+          { case (List(a), b) => Free(a, env_type(a, typ_body(b))) },
           { case (a, b) => Var(indexname(a), typ_body(b)) },
-          { case (Nil, a) => Bound(int(a)) case _ => ??? },
-          { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) case _ => ??? },
-          { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) case _ => ??? }))
+          { case (Nil, a) => Bound(int(a)) },
+          { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
+          { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))
       term
     }
 
@@ -82,17 +82,17 @@
       val term = term_env(env)
       def proof: T[Proof] =
         variant[Proof](List(
-          { case (Nil, Nil) => MinProof case _ => ??? },
-          { case (Nil, a) => PBound(int(a)) case _ => ??? },
-          { case (List(a), b) => val (c, d) = pair(typ, proof)(b); Abst(a, c, d) case _ => ??? },
-          { case (List(a), b) => val (c, d) = pair(term, proof)(b); AbsP(a, c, d) case _ => ??? },
-          { case (Nil, a) => val (b, c) = pair(proof, term)(a); Appt(b, c) case _ => ??? },
-          { case (Nil, a) => val (b, c) = pair(proof, proof)(a); AppP(b, c) case _ => ??? },
-          { case (Nil, a) => Hyp(term(a)) case _ => ??? },
-          { case (List(a), b) => PAxm(a, list(typ)(b)) case _ => ??? },
-          { case (List(a), b) => PClass(typ(b), a) case _ => ??? },
-          { case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) case _ => ??? },
-          { case (List(a, b, c), d) => PThm(long_atom(a), b, c, list(typ)(d)) case _ => ??? }))
+          { case (Nil, Nil) => MinProof },
+          { case (Nil, a) => PBound(int(a)) },
+          { case (List(a), b) => val (c, d) = pair(typ, proof)(b); Abst(a, c, d) },
+          { case (List(a), b) => val (c, d) = pair(term, proof)(b); AbsP(a, c, d) },
+          { case (Nil, a) => val (b, c) = pair(proof, term)(a); Appt(b, c) },
+          { case (Nil, a) => val (b, c) = pair(proof, proof)(a); AppP(b, c) },
+          { case (Nil, a) => Hyp(term(a)) },
+          { case (List(a), b) => PAxm(a, list(typ)(b)) },
+          { case (List(a), b) => PClass(typ(b), a) },
+          { case (List(a), b) => val (c, d) = pair(term, list(typ))(b); Oracle(a, c, d) },
+          { case (List(a, b, c), d) => PThm(long_atom(a), b, c, list(typ)(d)) }))
       proof
     }
 
diff -r a36a1cc0144c -r df9d869cd5fd src/Tools/Graphview/layout.scala
--- a/src/Tools/Graphview/layout.scala	Wed Apr 13 16:53:46 2022 +0200
+++ b/src/Tools/Graphview/layout.scala	Fri Apr 22 10:31:38 2022 +0200
@@ -137,10 +137,10 @@
 
               val levels1 = dummies_levels.foldLeft(levels)(_ + _)
               val graph1 =
-                (v1 :: dummies ::: List(v2)).sliding(2).map(_.toList).
-                  foldLeft(dummies.foldLeft(graph)(_.new_node(_, dummy_info)).del_edge(v1, v2)) {
-                    case (g, List(a, b)) => g.add_edge(a, b)
-                    case _ => ???
+                (v1 :: dummies ::: List(v2)).sliding(2)
+                  .foldLeft(dummies.foldLeft(graph)(_.new_node(_, dummy_info)).del_edge(v1, v2)) {
+                    case (g, Seq(a, b)) => g.add_edge(a, b)
+                    case (g, _) => g
                   }
               (graph1, levels1)
             }
@@ -236,8 +236,8 @@
   }
 
   private def count_crossings(graph: Graph, levels: List[Level]): Int =
-    levels.iterator.sliding(2).map(_.toList).map {
-      case List(top, bot) =>
+    levels.iterator.sliding(2).map {
+      case Seq(top, bot) =>
         top.iterator.zipWithIndex.map {
           case (outer_parent, outer_parent_index) =>
             graph.imm_succs(outer_parent).iterator.map(bot.indexOf(_)).map(outer_child =>
diff -r a36a1cc0144c -r df9d869cd5fd src/Tools/Graphview/shapes.scala
--- a/src/Tools/Graphview/shapes.scala	Wed Apr 13 16:53:46 2022 +0200
+++ b/src/Tools/Graphview/shapes.scala	Fri Apr 22 10:31:38 2022 +0200
@@ -116,8 +116,8 @@
         val dy = coords(2).y - coords(0).y
 
         val (dx2, dy2) =
-          coords.sliding(3).map(_.toList).foldLeft((dx, dy)) {
-            case ((dx, dy), List(l, m, r)) =>
+          coords.sliding(3).foldLeft((dx, dy)) {
+            case ((dx, dy), Seq(l, m, r)) =>
               val dx2 = r.x - l.x
               val dy2 = r.y - l.y
               path.curveTo(
@@ -125,7 +125,7 @@
                 m.x - slack * dx2, m.y - slack * dy2,
                 m.x, m.y)
               (dx2, dy2)
-            case _ => ???
+            case (p, _) => p
           }
 
         val l = ds.last
diff -r a36a1cc0144c -r df9d869cd5fd src/Tools/jEdit/jedit_main/scala_console.scala
--- a/src/Tools/jEdit/jedit_main/scala_console.scala	Wed Apr 13 16:53:46 2022 +0200
+++ b/src/Tools/jEdit/jedit_main/scala_console.scala	Fri Apr 22 10:31:38 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,67 +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(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): 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,
@@ -161,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())
 }
diff -r a36a1cc0144c -r df9d869cd5fd src/Tools/jEdit/src/jedit_bibtex.scala
--- a/src/Tools/jEdit/src/jedit_bibtex.scala	Wed Apr 13 16:53:46 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_bibtex.scala	Fri Apr 22 10:31:38 2022 +0200
@@ -26,24 +26,20 @@
 object JEdit_Bibtex {
   /** context menu **/
 
-  def context_menu(text_area0: JEditTextArea): List[JMenuItem] = {
-    text_area0 match {
-      case text_area: TextArea =>
-        text_area.getBuffer match {
-          case buffer: Buffer
-          if (Bibtex.is_bibtex(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable) =>
-            val menu = new JMenu("BibTeX entries")
-            for (entry <- Bibtex.known_entries) {
-              val item = new JMenuItem(entry.kind)
-              item.addActionListener(new ActionListener {
-                def actionPerformed(evt: ActionEvent): Unit =
-                  Isabelle.insert_line_padding(text_area, entry.template)
-              })
-              menu.add(item)
-            }
-            List(menu)
-          case _ => Nil
+  def context_menu(text_area: JEditTextArea): List[JMenuItem] = {
+    text_area.getBuffer match {
+      case buffer: Buffer
+      if Bibtex.is_bibtex(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable =>
+        val menu = new JMenu("BibTeX entries")
+        for (entry <- Bibtex.known_entries) {
+          val item = new JMenuItem(entry.kind)
+          item.addActionListener(new ActionListener {
+            def actionPerformed(evt: ActionEvent): Unit =
+              Isabelle.insert_line_padding(text_area, entry.template)
+          })
+          menu.add(item)
         }
+        List(menu)
       case _ => Nil
     }
   }