--- a/src/Pure/General/json.scala Thu Dec 13 13:11:35 2018 +0100
+++ b/src/Pure/General/json.scala Thu Dec 13 15:21:34 2018 +0100
@@ -244,11 +244,9 @@
{
object UUID
{
- def unapply(json: T): Option[java.util.UUID] =
+ def unapply(json: T): Option[isabelle.UUID.T] =
json match {
- case x: java.lang.String =>
- try { Some(java.util.UUID.fromString(x)) }
- catch { case _: IllegalArgumentException => None }
+ case x: java.lang.String => isabelle.UUID.unapply(x)
case _ => None
}
}
@@ -349,7 +347,7 @@
case Some(json) => unapply(json)
}
- def uuid(obj: T, name: String): Option[UUID] =
+ def uuid(obj: T, name: String): Option[UUID.T] =
value(obj, name, Value.UUID.unapply)
def string(obj: T, name: String): Option[String] =
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/uuid.scala Thu Dec 13 15:21:34 2018 +0100
@@ -0,0 +1,20 @@
+/* Title: Pure/General/uuid.scala
+ Author: Makarius
+
+Universally unique identifiers.
+*/
+
+package isabelle
+
+
+object UUID
+{
+ type T = java.util.UUID
+
+ def random(): T = java.util.UUID.randomUUID()
+ def random_string(): String = random().toString
+
+ def unapply(s: String): Option[T] =
+ try { Some(java.util.UUID.fromString(s)) }
+ catch { case _: IllegalArgumentException => None }
+}
--- a/src/Pure/PIDE/headless.scala Thu Dec 13 13:11:35 2018 +0100
+++ b/src/Pure/PIDE/headless.scala Thu Dec 13 15:21:34 2018 +0100
@@ -193,7 +193,7 @@
check_limit: Int = 0,
watchdog_timeout: Time = default_watchdog_timeout,
nodes_status_delay: Time = default_nodes_status_delay,
- id: UUID = UUID(),
+ id: UUID.T = UUID.random(),
// commit: must not block, must not fail
commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None,
commit_cleanup_delay: Time = default_commit_cleanup_delay,
@@ -362,7 +362,7 @@
}
sealed case class State(
- required: Multi_Map[Document.Node.Name, UUID] = Multi_Map.empty,
+ required: Multi_Map[Document.Node.Name, UUID.T] = Multi_Map.empty,
theories: Map[Document.Node.Name, Theory] = Map.empty)
{
lazy val theory_graph: Graph[Document.Node.Name, Unit] =
@@ -375,10 +375,10 @@
def is_required(name: Document.Node.Name): Boolean = required.isDefinedAt(name)
- def insert_required(id: UUID, names: List[Document.Node.Name]): State =
+ def insert_required(id: UUID.T, names: List[Document.Node.Name]): State =
copy(required = (required /: names)(_.insert(_, id)))
- def remove_required(id: UUID, names: List[Document.Node.Name]): State =
+ def remove_required(id: UUID.T, names: List[Document.Node.Name]): State =
copy(required = (required /: names)(_.remove(_, id)))
def update_theories(update: List[(Document.Node.Name, Theory)]): State =
@@ -396,7 +396,8 @@
copy(theories = theories -- remove)
}
- def unload_theories(session: Session, id: UUID, dep_theories: List[Document.Node.Name]): State =
+ def unload_theories(session: Session, id: UUID.T, dep_theories: List[Document.Node.Name])
+ : State =
{
val st1 = remove_required(id, dep_theories)
val theory_edits =
@@ -455,7 +456,7 @@
def load_theories(
session: Session,
- id: UUID,
+ id: UUID.T,
dep_theories: List[Document.Node.Name],
progress: Progress)
{
@@ -490,12 +491,12 @@
})
}
- def unload_theories(session: Session, id: UUID, dep_theories: List[Document.Node.Name])
+ def unload_theories(session: Session, id: UUID.T, dep_theories: List[Document.Node.Name])
{
state.change(_.unload_theories(session, id, dep_theories))
}
- def clean_theories(session: Session, id: UUID, clean: Set[Document.Node.Name])
+ def clean_theories(session: Session, id: UUID.T, clean: Set[Document.Node.Name])
{
state.change(st =>
{
--- a/src/Pure/ROOT.scala Thu Dec 13 13:11:35 2018 +0100
+++ b/src/Pure/ROOT.scala Thu Dec 13 15:21:34 2018 +0100
@@ -21,7 +21,4 @@
def proper[A](x: A): Option[A] = Library.proper(x)
val proper_string = Library.proper_string _
def proper_list[A](list: List[A]): Option[List[A]] = Library.proper_list(list)
-
- type UUID = java.util.UUID
- def UUID(): UUID = java.util.UUID.randomUUID()
}
--- a/src/Pure/Tools/server.scala Thu Dec 13 13:11:35 2018 +0100
+++ b/src/Pure/Tools/server.scala Thu Dec 13 15:21:34 2018 +0100
@@ -238,7 +238,7 @@
def remove_task(task: Task): Unit =
_tasks.change(_ - task)
- def cancel_task(id: UUID): Unit =
+ def cancel_task(id: UUID.T): Unit =
_tasks.change(tasks => { tasks.find(task => task.id == id).foreach(_.cancel); tasks })
def close()
@@ -282,7 +282,7 @@
{
task =>
- val id: UUID = UUID()
+ val id: UUID.T = UUID.random()
val ident: JSON.Object.Entry = ("task" -> id.toString)
val progress: Connection_Progress = context.progress(ident)
@@ -492,11 +492,11 @@
private val server_socket = new ServerSocket(_port, 50, InetAddress.getByName("127.0.0.1"))
- private val _sessions = Synchronized(Map.empty[UUID, Headless.Session])
- def err_session(id: UUID): Nothing = error("No session " + Library.single_quote(id.toString))
- def the_session(id: UUID): Headless.Session = _sessions.value.get(id) getOrElse err_session(id)
- def add_session(entry: (UUID, Headless.Session)) { _sessions.change(_ + entry) }
- def remove_session(id: UUID): Headless.Session =
+ 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.get(id) getOrElse err_session(id)
+ def add_session(entry: (UUID.T, Headless.Session)) { _sessions.change(_ + entry) }
+ def remove_session(id: UUID.T): Headless.Session =
{
_sessions.change_result(sessions =>
sessions.get(id) match {
@@ -520,7 +520,7 @@
}
def port: Int = server_socket.getLocalPort
- val password: String = UUID().toString
+ val password: String = UUID.random_string()
override def toString: String = Server.print(port, password)
--- a/src/Pure/Tools/server_commands.scala Thu Dec 13 13:11:35 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala Thu Dec 13 15:21:34 2018 +0100
@@ -13,7 +13,7 @@
object Cancel
{
- sealed case class Args(task: UUID)
+ sealed case class Args(task: UUID.T)
def unapply(json: JSON.T): Option[Args] =
for { task <- JSON.uuid(json, "task") }
@@ -107,7 +107,7 @@
yield Args(build = build, print_mode = print_mode)
def command(args: Args, progress: Progress = No_Progress, log: Logger = No_Logger)
- : (JSON.Object.T, (UUID, Headless.Session)) =
+ : (JSON.Object.T, (UUID.T, Headless.Session)) =
{
val base_info =
try { Session_Build.command(args.build, progress = progress)._3 }
@@ -123,7 +123,7 @@
progress = progress,
log = log)
- val id = UUID()
+ val id = UUID.random()
val res =
JSON.Object(
@@ -136,7 +136,7 @@
object Session_Stop
{
- def unapply(json: JSON.T): Option[UUID] =
+ def unapply(json: JSON.T): Option[UUID.T] =
JSON.uuid(json, "session_id")
def command(session: Headless.Session): (JSON.Object.T, Process_Result) =
@@ -152,7 +152,7 @@
object Use_Theories
{
sealed case class Args(
- session_id: UUID,
+ session_id: UUID.T,
theories: List[String],
master_dir: String = "",
pretty_margin: Double = Pretty.default_margin,
@@ -187,7 +187,7 @@
def command(args: Args,
session: Headless.Session,
- id: UUID = UUID(),
+ id: UUID.T = UUID.random(),
progress: Progress = No_Progress): (JSON.Object.T, Headless.Use_Theories_Result) =
{
val result =
@@ -249,7 +249,7 @@
object Purge_Theories
{
sealed case class Args(
- session_id: UUID,
+ session_id: UUID.T,
theories: List[String] = Nil,
master_dir: String = "",
all: Boolean = false)
--- a/src/Pure/build-jars Thu Dec 13 13:11:35 2018 +0100
+++ b/src/Pure/build-jars Thu Dec 13 15:21:34 2018 +0100
@@ -75,6 +75,7 @@
General/untyped.scala
General/url.scala
General/utf8.scala
+ General/uuid.scala
General/value.scala
General/word.scala
General/xz.scala
--- a/src/Tools/VSCode/src/grammar.scala Thu Dec 13 13:11:35 2018 +0100
+++ b/src/Tools/VSCode/src/grammar.scala Thu Dec 13 15:21:34 2018 +0100
@@ -45,7 +45,7 @@
"name": "Isabelle",
"scopeName": "source.isabelle",
"fileTypes": ["thy"],
- "uuid": """ + JSON.Format(UUID().toString) + """,
+ "uuid": """ + JSON.Format(UUID.random_string()) + """,
"repository": {
"comment": {
"patterns": [
--- a/src/Tools/jEdit/src/plugin.scala Thu Dec 13 13:11:35 2018 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Thu Dec 13 15:21:34 2018 +0100
@@ -433,7 +433,7 @@
/* HTTP server */
- val http_root: String = "/" + UUID()
+ val http_root: String = "/" + UUID.random()
val http_server: HTTP.Server = HTTP.server(Document_Model.http_handlers(http_root))