# HG changeset patch # User wenzelm # Date 1610877236 -3600 # Node ID 11da341c2968ca27cec60e1bad76512d3fa49b35 # Parent 4c4d479b097dbab81b4d38fb84a976bb0d4ed0a5# Parent ca450d902198be5409671efbd650ce0acab45d61 merged diff -r 4c4d479b097d -r 11da341c2968 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Thu Jan 14 16:58:04 2021 +0000 +++ b/Admin/components/components.sha1 Sun Jan 17 10:53:56 2021 +0100 @@ -311,6 +311,7 @@ 54c1b06fa2c5f6c2ab3d391ef342c0532cd7f392 scala-2.12.6.tar.gz 02358f00acc138371324b6248fdb62eed791c6bd scala-2.12.7.tar.gz 201c05ae9cc382ee6c08af49430e426f6bbe0d5a scala-2.12.8.tar.gz +ec53cce3c5edda1145ec5d13924a5f9418995c15 scala-2.13.4.tar.gz b447017e81600cc5e30dd61b5d4962f6da01aa80 scala-2.8.1.final.tar.gz 5659440f6b86db29f0c9c0de7249b7e24a647126 scala-2.9.2.tar.gz abe7a3b50da529d557a478e9f631a22429418a67 smbc-0.4.1.tar.gz diff -r 4c4d479b097d -r 11da341c2968 Admin/components/main --- a/Admin/components/main Thu Jan 14 16:58:04 2021 +0000 +++ b/Admin/components/main Sun Jan 17 10:53:56 2021 +0100 @@ -15,7 +15,7 @@ opam-2.0.7 polyml-test-f86ae3dc1686 postgresql-42.2.18 -scala-2.12.12 +scala-2.13.4 smbc-0.4.1 spass-3.8ds-2 sqlite-jdbc-3.34.0 diff -r 4c4d479b097d -r 11da341c2968 etc/settings --- a/etc/settings Thu Jan 14 16:58:04 2021 +0000 +++ b/etc/settings Sun Jan 17 10:53:56 2021 +0100 @@ -16,7 +16,7 @@ ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m" -ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -nowarn -target:jvm-1.8 -Xmax-classfile-name 130 -J-Xms512m -J-Xmx4g -J-Xss16m" +ISABELLE_SCALAC_OPTIONS="-encoding UTF-8 -nowarn -target:jvm-1.8 -J-Xms512m -J-Xmx4g -J-Xss16m" classpath "$ISABELLE_HOME/lib/classes/Pure.jar" diff -r 4c4d479b097d -r 11da341c2968 src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Thu Jan 14 16:58:04 2021 +0000 +++ b/src/Doc/JEdit/JEdit.thy Sun Jan 17 10:53:56 2021 +0100 @@ -296,7 +296,7 @@ Options are: -c only check presence of server -n only report server name - -s NAME server name (default Isabelle) + -s NAME server name (default "Isabelle") Connect to already running Isabelle/jEdit instance and open FILES\} diff -r 4c4d479b097d -r 11da341c2968 src/HOL/Imperative_HOL/Array.thy --- a/src/HOL/Imperative_HOL/Array.thy Thu Jan 14 16:58:04 2021 +0000 +++ b/src/HOL/Imperative_HOL/Array.thy Sun Jan 17 10:53:56 2021 +0100 @@ -486,7 +486,7 @@ text \Scala\ -code_printing type_constructor array \ (Scala) "!collection.mutable.ArraySeq[_]" +code_printing type_constructor array \ (Scala) "!Array.T[_]" code_printing constant Array \ (Scala) "!sys.error(\"bare Array\")" code_printing constant Array.new' \ (Scala) "('_: Unit)/ => / Array.alloc((_))((_))" code_printing constant Array.make' \ (Scala) "('_: Unit)/ =>/ Array.make((_))((_))" diff -r 4c4d479b097d -r 11da341c2968 src/HOL/Imperative_HOL/Heap_Monad.thy --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Thu Jan 14 16:58:04 2021 +0000 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Sun Jan 17 10:53:56 2021 +0100 @@ -579,7 +579,7 @@ code_printing code_module "Heap" \ (Scala) \object Heap { - def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) () + def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g(f(()))(()) } class Ref[A](x: A) { @@ -596,20 +596,29 @@ } object Array { - import collection.mutable.ArraySeq - def alloc[A](n: BigInt)(x: A): ArraySeq[A] = - ArraySeq.fill(n.toInt)(x) - def make[A](n: BigInt)(f: BigInt => A): ArraySeq[A] = - ArraySeq.tabulate(n.toInt)((k: Int) => f(BigInt(k))) - def len[A](a: ArraySeq[A]): BigInt = - BigInt(a.length) - def nth[A](a: ArraySeq[A], n: BigInt): A = - a(n.toInt) - def upd[A](a: ArraySeq[A], n: BigInt, x: A): Unit = - a.update(n.toInt, x) - def freeze[A](a: ArraySeq[A]): List[A] = - a.toList + class T[A](n: Int) + { + val array: Array[AnyRef] = new Array[AnyRef](n) + def apply(i: Int): A = array(i).asInstanceOf[A] + def update(i: Int, x: A): Unit = array(i) = x.asInstanceOf[AnyRef] + def length: Int = array.length + def toList: List[A] = array.toList.asInstanceOf[List[A]] + override def toString: String = array.mkString("Array.T(", ",", ")") + } + def make[A](n: BigInt)(f: BigInt => A): T[A] = + { + val m = n.toInt + val a = new T[A](m) + for (i <- 0 until m) a(i) = f(i) + a + } + def alloc[A](n: BigInt)(x: A): T[A] = make(n)(_ => x) + def len[A](a: T[A]): BigInt = BigInt(a.length) + def nth[A](a: T[A], n: BigInt): A = a(n.toInt) + def upd[A](a: T[A], n: BigInt, x: A): Unit = a.update(n.toInt, x) + def freeze[A](a: T[A]): List[A] = a.toList } + \ code_reserved Scala Heap Ref Array diff -r 4c4d479b097d -r 11da341c2968 src/Pure/General/linear_set.scala --- a/src/Pure/General/linear_set.scala Thu Jan 14 16:58:04 2021 +0000 +++ b/src/Pure/General/linear_set.scala Sun Jan 17 10:53:56 2021 +0100 @@ -8,19 +8,26 @@ package isabelle -import scala.collection.SetLike -import scala.collection.generic.{SetFactory, CanBuildFrom, GenericSetTemplate, GenericCompanion} -import scala.collection.mutable.{Builder, SetBuilder} -import scala.language.higherKinds +import scala.collection.mutable +import scala.collection.immutable.SetOps +import scala.collection.{IterableFactory, IterableFactoryDefaults} -object Linear_Set extends SetFactory[Linear_Set] +object Linear_Set extends IterableFactory[Linear_Set] { private val empty_val: Linear_Set[Nothing] = new Linear_Set[Nothing](None, None, Map(), Map()) override def empty[A]: Linear_Set[A] = empty_val.asInstanceOf[Linear_Set[A]] - implicit def canBuildFrom[A]: CanBuildFrom[Coll, A, Linear_Set[A]] = setCanBuildFrom[A] - def newBuilder[A]: Builder[A, Linear_Set[A]] = new SetBuilder[A, Linear_Set[A]](empty[A]) + def from[A](entries: IterableOnce[A]): Linear_Set[A] = (empty[A] /: entries)(_.incl(_)) + + override def newBuilder[A]: mutable.Builder[A, Linear_Set[A]] = new Builder[A] + private class Builder[A] extends mutable.Builder[A, Linear_Set[A]] + { + private var res = empty[A] + override def clear() { res = empty[A] } + override def addOne(elem: A): this.type = { res = res.incl(elem); this } + override def result(): Linear_Set[A] = res + } class Duplicate[A](x: A) extends Exception class Undefined[A](x: A) extends Exception @@ -30,13 +37,10 @@ final class Linear_Set[A] private( start: Option[A], end: Option[A], val nexts: Map[A, A], prevs: Map[A, A]) - extends scala.collection.immutable.Set[A] - with GenericSetTemplate[A, Linear_Set] - with SetLike[A, Linear_Set[A]] + extends Iterable[A] + with SetOps[A, Linear_Set, Linear_Set[A]] + with IterableFactoryDefaults[A, Linear_Set] { - override def companion: GenericCompanion[Linear_Set] = Linear_Set - - /* relative addressing */ def next(elem: A): Option[A] = @@ -78,7 +82,7 @@ } } - def append_after(hook: Option[A], elems: Traversable[A]): Linear_Set[A] = // FIXME reverse fold + def append_after(hook: Option[A], elems: Iterable[A]): Linear_Set[A] = // FIXME reverse fold ((hook, this) /: elems) { case ((last, set), elem) => (Some(elem), set.insert_after(last, elem)) }._2 @@ -115,8 +119,6 @@ /* Set methods */ - override def stringPrefix = "Linear_Set" - override def isEmpty: Boolean = start.isEmpty override def size: Int = if (isEmpty) 0 else nexts.size + 1 @@ -153,7 +155,10 @@ override def last: A = reverse.head - def + (elem: A): Linear_Set[A] = insert_after(end, elem) + def incl(elem: A): Linear_Set[A] = insert_after(end, elem) + def excl(elem: A): Linear_Set[A] = delete_after(prev(elem)) - def - (elem: A): Linear_Set[A] = delete_after(prev(elem)) + override def iterableFactory: IterableFactory[Linear_Set] = Linear_Set + + override def toString: String = mkString("Linear_Set(", ", ", ")") } diff -r 4c4d479b097d -r 11da341c2968 src/Pure/General/multi_map.scala --- a/src/Pure/General/multi_map.scala Thu Jan 14 16:58:04 2021 +0000 +++ b/src/Pure/General/multi_map.scala Sun Jan 17 10:53:56 2021 +0100 @@ -6,24 +6,33 @@ package isabelle - -import scala.collection.GenTraversableOnce -import scala.collection.generic.{ImmutableMapFactory, CanBuildFrom} +import scala.collection.mutable +import scala.collection.{IterableFactory, MapFactory, MapFactoryDefaults} +import scala.collection.immutable.{Iterable, MapOps} -object Multi_Map extends ImmutableMapFactory[Multi_Map] +object Multi_Map extends MapFactory[Multi_Map] { private val empty_val: Multi_Map[Any, Nothing] = new Multi_Map[Any, Nothing](Map.empty) - override def empty[A, B]: Multi_Map[A, B] = empty_val.asInstanceOf[Multi_Map[A, B]] + def empty[A, B]: Multi_Map[A, B] = empty_val.asInstanceOf[Multi_Map[A, B]] + + def from[A, B](entries: IterableOnce[(A, B)]): Multi_Map[A, B] = + (empty[A, B] /: entries)({ case (m, (a, b)) => m.insert(a, b) }) - implicit def canBuildFrom[A, B]: CanBuildFrom[Coll, (A, B), Multi_Map[A, B]] = - new MapCanBuildFrom[A, B] + override def newBuilder[A, B]: mutable.Builder[(A, B), Multi_Map[A, B]] = new Builder[A, B] + private class Builder[A, B] extends mutable.Builder[(A, B), Multi_Map[A, B]] + { + private var res = empty[A, B] + override def clear() { res = empty[A, B] } + override def addOne(p: (A, B)): this.type = { res = res.insert(p._1, p._2); this } + override def result(): Multi_Map[A, B] = res + } } - final class Multi_Map[A, +B] private(protected val rep: Map[A, List[B]]) - extends scala.collection.immutable.Map[A, B] - with scala.collection.immutable.MapLike[A, B, Multi_Map[A, B]] + extends Iterable[(A, B)] + with MapOps[A, B, Multi_Map, Multi_Map[A, B]] + with MapFactoryDefaults[A, B, Multi_Map, Iterable] { /* Multi_Map operations */ @@ -61,8 +70,6 @@ /* Map operations */ - override def stringPrefix = "Multi_Map" - override def empty: Multi_Map[A, Nothing] = Multi_Map.empty override def isEmpty: Boolean = rep.isEmpty @@ -73,11 +80,12 @@ def get(a: A): Option[B] = get_list(a).headOption - def + [B1 >: B](p: (A, B1)): Multi_Map[A, B1] = insert(p._1, p._2) + override def updated[B1 >: B](a: A, b: B1): Multi_Map[A, B1] = insert(a, b) + + override def removed(a: A): Multi_Map[A, B] = + if (rep.isDefinedAt(a)) new Multi_Map(rep - a) else this - override def ++ [B1 >: B](entries: GenTraversableOnce[(A, B1)]): Multi_Map[A, B1] = - (this.asInstanceOf[Multi_Map[A, B1]] /: entries)(_ + _) + override def mapFactory: MapFactory[Multi_Map] = Multi_Map - def - (a: A): Multi_Map[A, B] = - if (rep.isDefinedAt(a)) new Multi_Map(rep - a) else this + override def toString: String = mkString("Multi_Map(", ", ", ")") } diff -r 4c4d479b097d -r 11da341c2968 src/Pure/General/scan.scala --- a/src/Pure/General/scan.scala Thu Jan 14 16:58:04 2021 +0000 +++ b/src/Pure/General/scan.scala Sun Jan 17 10:53:56 2021 +0100 @@ -9,10 +9,9 @@ import scala.annotation.tailrec import scala.collection.{IndexedSeq, Traversable, TraversableOnce} -import scala.collection.immutable.PagedSeq import scala.util.matching.Regex import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, - Reader, CharSequenceReader} + Reader, CharSequenceReader, PagedSeq} import scala.util.parsing.combinator.RegexParsers import java.io.{File => JFile, BufferedInputStream, FileInputStream, InputStream} import java.net.URL diff -r 4c4d479b097d -r 11da341c2968 src/Pure/General/uuid.scala --- a/src/Pure/General/uuid.scala Thu Jan 14 16:58:04 2021 +0000 +++ b/src/Pure/General/uuid.scala Sun Jan 17 10:53:56 2021 +0100 @@ -17,4 +17,6 @@ def unapply(s: String): Option[T] = try { Some(java.util.UUID.fromString(s)) } catch { case _: IllegalArgumentException => None } + + def unapply(body: XML.Body): Option[T] = unapply(XML.content(body)) } diff -r 4c4d479b097d -r 11da341c2968 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Thu Jan 14 16:58:04 2021 +0000 +++ b/src/Pure/ROOT.ML Sun Jan 17 10:53:56 2021 +0100 @@ -354,3 +354,4 @@ ML_file "Tools/jedit.ML"; ML_file "Tools/ghc.ML"; ML_file "Tools/generated_files.ML" + diff -r 4c4d479b097d -r 11da341c2968 src/Pure/ROOT.scala --- a/src/Pure/ROOT.scala Thu Jan 14 16:58:04 2021 +0000 +++ b/src/Pure/ROOT.scala Sun Jan 17 10:53:56 2021 +0100 @@ -21,3 +21,4 @@ val proper_string = Library.proper_string _ def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list) } + diff -r 4c4d479b097d -r 11da341c2968 src/Pure/System/bash.scala --- a/src/Pure/System/bash.scala Thu Jan 14 16:58:04 2021 +0000 +++ b/src/Pure/System/bash.scala Sun Jan 17 10:53:56 2021 +0100 @@ -199,7 +199,7 @@ if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt() - Process_Result(rc, out_lines.join, err_lines.join, false, get_timing) + Process_Result(rc, out_lines.join, err_lines.join, get_timing) } } } diff -r 4c4d479b097d -r 11da341c2968 src/Pure/System/process_result.scala --- a/src/Pure/System/process_result.scala Thu Jan 14 16:58:04 2021 +0000 +++ b/src/Pure/System/process_result.scala Sun Jan 17 10:53:56 2021 +0100 @@ -26,14 +26,16 @@ 137 -> "KILL SIGNAL", 138 -> "BUS ERROR", 139 -> "SEGMENTATION VIOLATION", + 142 -> "TIMEOUT", 143 -> "TERMINATION SIGNAL") + + val timeout_rc = 142 } final case class Process_Result( rc: Int, out_lines: List[String] = Nil, err_lines: List[String] = Nil, - timeout: Boolean = false, timing: Timing = Timing.zero) { def out: String = cat_lines(out_lines) @@ -46,11 +48,12 @@ def error(err: String): Process_Result = if (err.isEmpty) this else errors(List(err)) - def was_timeout: Process_Result = copy(rc = 1, timeout = true) - def ok: Boolean = rc == 0 def interrupted: Boolean = rc == Exn.Interrupt.return_code + def timeout_rc: Process_Result = copy(rc = Process_Result.timeout_rc) + def timeout: Boolean = rc == Process_Result.timeout_rc + def error_rc: Process_Result = if (interrupted) this else copy(rc = rc max 1) def errors_rc(errs: List[String]): Process_Result = diff -r 4c4d479b097d -r 11da341c2968 src/Pure/System/scala.scala --- a/src/Pure/System/scala.scala Thu Jan 14 16:58:04 2021 +0000 +++ b/src/Pure/System/scala.scala Sun Jan 17 10:53:56 2021 +0100 @@ -11,7 +11,7 @@ import scala.tools.nsc.{GenericRunnerSettings, ConsoleWriter, NewLinePrintWriter} import scala.tools.nsc.interpreter.{IMain, Results} - +import scala.tools.nsc.interpreter.shell.ReplReporterImpl object Scala { @@ -96,7 +96,7 @@ print_writer: PrintWriter = default_print_writer, class_loader: ClassLoader = null): IMain = { - new IMain(settings, print_writer) + new IMain(settings, new ReplReporterImpl(settings, print_writer)) { override def parentClassLoader: ClassLoader = if (class_loader == null) super.parentClassLoader diff -r 4c4d479b097d -r 11da341c2968 src/Pure/Thy/file_format.scala --- a/src/Pure/Thy/file_format.scala Thu Jan 14 16:58:04 2021 +0000 +++ b/src/Pure/Thy/file_format.scala Sun Jan 17 10:53:56 2021 +0100 @@ -1,7 +1,7 @@ /* Title: Pure/Thy/file_format.scala Author: Makarius -Support for user-defined file formats. +Support for user-defined file formats, associated with active session. */ package isabelle diff -r 4c4d479b097d -r 11da341c2968 src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala Thu Jan 14 16:58:04 2021 +0000 +++ b/src/Pure/Thy/html.scala Sun Jan 17 10:53:56 2021 +0100 @@ -330,6 +330,8 @@ """ """ + val footer: String = """""" + val head_meta: XML.Elem = XML.Elem(Markup("meta", List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil) @@ -340,12 +342,14 @@ structural: Boolean = true): String = { cat_lines( - List(header, + List( + header, output( XML.elem("head", head_meta :: (if (css == "") Nil else List(style_file(css))) ::: head), hidden = hidden, structural = structural), output(XML.elem("body", body), - hidden = hidden, structural = structural))) + hidden = hidden, structural = structural), + footer)) } diff -r 4c4d479b097d -r 11da341c2968 src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Thu Jan 14 16:58:04 2021 +0000 +++ b/src/Pure/Tools/build_job.scala Sun Jan 17 10:53:56 2021 +0100 @@ -523,10 +523,9 @@ } val result2 = - if (result1.interrupted) { - if (was_timeout) result1.error(Output.error_message_text("Timeout")).was_timeout - else result1.error(Output.error_message_text("Interrupt")) - } + if (result1.ok) result1 + else if (was_timeout) result1.error(Output.error_message_text("Timeout")).timeout_rc + else if (result1.interrupted) result1.error(Output.error_message_text("Interrupt")) else result1 val heap_digest = diff -r 4c4d479b097d -r 11da341c2968 src/Pure/Tools/server.scala --- a/src/Pure/Tools/server.scala Thu Jan 14 16:58:04 2021 +0000 +++ b/src/Pure/Tools/server.scala Sun Jan 17 10:53:56 2021 +0100 @@ -121,6 +121,39 @@ } + /* handler: port, password, thread */ + + abstract class Handler(port0: Int) + { + val socket: ServerSocket = new ServerSocket(port0, 50, Server.localhost) + def port: Int = socket.getLocalPort + val password: String = UUID.random_string() + + override def toString: String = print(port, password) + + def handle(connection: Server.Connection): Unit + + private lazy val thread: Thread = + Isabelle_Thread.fork(name = "server_handler") { + var finished = false + while (!finished) { + Exn.capture(socket.accept) match { + case Exn.Res(client) => + Isabelle_Thread.fork(name = "server_connection") { + using(Connection(client))(connection => + if (connection.read_password(password)) handle(connection)) + } + case Exn.Exn(_) => finished = true + } + } + } + + def start { thread } + def join { thread.join } + def stop { socket.close; join } + } + + /* socket connection */ object Connection @@ -155,6 +188,10 @@ try { Byte_Message.read_line_message(in).map(_.text) } catch { case _: IOException => None } + def await_close(): Unit = + try { Byte_Message.read(in, 1); socket.close() } + catch { case _: IOException => } + def write_message(msg: String): Unit = out_lock.synchronized { Byte_Message.write_line_message(out, Bytes(UTF8.bytes(msg))) } @@ -240,7 +277,7 @@ { val json = for ((name, node_status) <- nodes_status.present) - yield name.json + ("status" -> nodes_status(name).json) + yield name.json + ("status" -> node_status.json) context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json)) } @@ -477,12 +514,10 @@ }) } -class Server private(_port: Int, val log: Logger) +class Server private(port0: Int, val log: Logger) extends Server.Handler(port0) { server => - private val server_socket = new ServerSocket(_port, 50, Server.localhost) - private val _sessions = Synchronized(Map.empty[UUID.T, Headless.Session]) def err_session(id: UUID.T): Nothing = error("No session " + Library.single_quote(id.toString)) def the_session(id: UUID.T): Headless.Session = _sessions.value.getOrElse(id, err_session(id)) @@ -498,7 +533,7 @@ def shutdown() { - server_socket.close + server.socket.close val sessions = _sessions.change_result(sessions => (sessions, Map.empty)) for ((_, session) <- sessions) { @@ -510,75 +545,53 @@ } } - def port: Int = server_socket.getLocalPort - val password: String = UUID.random_string() + override def join { super.join; shutdown() } - override def toString: String = Server.print(port, password) - - private def handle(connection: Server.Connection) + override def handle(connection: Server.Connection) { using(new Server.Context(server, connection))(context => { - if (connection.read_password(password)) { - connection.reply_ok( - JSON.Object( - "isabelle_id" -> Isabelle_System.isabelle_id(), - "isabelle_version" -> Distribution.version)) + connection.reply_ok( + JSON.Object( + "isabelle_id" -> Isabelle_System.isabelle_id(), + "isabelle_version" -> Distribution.version)) - var finished = false - while (!finished) { - connection.read_message() match { - case None => finished = true - case Some("") => context.notify("Command 'help' provides list of commands") - case Some(msg) => - val (name, argument) = Server.Argument.split(msg) - Server.command_table.get(name) match { - case Some(cmd) => - argument match { - case Server.Argument(arg) => - if (cmd.command_body.isDefinedAt((context, arg))) { - Exn.capture { cmd.command_body((context, arg)) } match { - case Exn.Res(task: Server.Task) => - connection.reply_ok(JSON.Object(task.ident)) - task.start - case Exn.Res(res) => connection.reply_ok(res) - case Exn.Exn(exn) => - val err = Server.json_error(exn) - if (err.isEmpty) throw exn else connection.reply_error(err) - } + var finished = false + while (!finished) { + connection.read_message() match { + case None => finished = true + case Some("") => context.notify("Command 'help' provides list of commands") + case Some(msg) => + val (name, argument) = Server.Argument.split(msg) + Server.command_table.get(name) match { + case Some(cmd) => + argument match { + case Server.Argument(arg) => + if (cmd.command_body.isDefinedAt((context, arg))) { + Exn.capture { cmd.command_body((context, arg)) } match { + case Exn.Res(task: Server.Task) => + connection.reply_ok(JSON.Object(task.ident)) + task.start + case Exn.Res(res) => connection.reply_ok(res) + case Exn.Exn(exn) => + val err = Server.json_error(exn) + if (err.isEmpty) throw exn else connection.reply_error(err) } - else { - connection.reply_error_message( - "Bad argument for command " + Library.single_quote(name), - "argument" -> argument) - } - case _ => + } + else { connection.reply_error_message( - "Malformed argument for command " + Library.single_quote(name), + "Bad argument for command " + Library.single_quote(name), "argument" -> argument) - } - case None => connection.reply_error("Bad command " + Library.single_quote(name)) - } - } + } + case _ => + connection.reply_error_message( + "Malformed argument for command " + Library.single_quote(name), + "argument" -> argument) + } + case None => connection.reply_error("Bad command " + Library.single_quote(name)) + } } } }) } - - private lazy val server_thread: Thread = - Isabelle_Thread.fork(name = "server") { - var finished = false - while (!finished) { - Exn.capture(server_socket.accept) match { - case Exn.Res(socket) => - Isabelle_Thread.fork(name = "server_connection") - { using(Server.Connection(socket))(handle) } - case Exn.Exn(_) => finished = true - } - } - } - - def start { server_thread } - - def join { server_thread.join; shutdown() } } diff -r 4c4d479b097d -r 11da341c2968 src/Tools/jEdit/lib/Tools/jedit_client --- a/src/Tools/jEdit/lib/Tools/jedit_client Thu Jan 14 16:58:04 2021 +0000 +++ b/src/Tools/jEdit/lib/Tools/jedit_client Sun Jan 17 10:53:56 2021 +0100 @@ -23,7 +23,7 @@ echo " Options are:" echo " -c only check presence of server" echo " -n only report server name" - echo " -s NAME server name (default $SERVER_NAME)" + echo " -s NAME server name (default \"$SERVER_NAME\")" echo echo " Connect to already running Isabelle/jEdit instance and open FILES" echo