--- 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
--- 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
--- 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"
--- 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\<close>}
--- 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 \<open>Scala\<close>
-code_printing type_constructor array \<rightharpoonup> (Scala) "!collection.mutable.ArraySeq[_]"
+code_printing type_constructor array \<rightharpoonup> (Scala) "!Array.T[_]"
code_printing constant Array \<rightharpoonup> (Scala) "!sys.error(\"bare Array\")"
code_printing constant Array.new' \<rightharpoonup> (Scala) "('_: Unit)/ => / Array.alloc((_))((_))"
code_printing constant Array.make' \<rightharpoonup> (Scala) "('_: Unit)/ =>/ Array.make((_))((_))"
--- 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" \<rightharpoonup> (Scala)
\<open>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
}
+
\<close>
code_reserved Scala Heap Ref Array
--- 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(", ", ", ")")
}
--- 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(", ", ", ")")
}
--- 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
--- 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))
}
--- 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"
+
--- 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)
}
+
--- 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)
}
}
}
--- 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 =
--- 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
--- 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
--- 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 @@
"""<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">"""
+ val footer: String = """</html>"""
+
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))
}
--- 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 =
--- 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() }
}
--- 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