--- 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)
}
--- 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
}
}
--- 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]
--- 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)
}
--- 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)
--- 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 }))
}
--- 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 }
--- 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)
--- 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)
}
}
--- 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)
}
}
--- 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
}
--- 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 =>
--- 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
--- 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())
}
--- 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
}
}