# HG changeset patch
# User wenzelm
# Date 1544710894 -3600
# Node ID 5655af3ea5bdc48eb81700e3de1e7efc5c066c38
# Parent  bea49e443909db49d5f8d945911d5ee2fce4797e
clarified modules and signature;

diff -r bea49e443909 -r 5655af3ea5bd src/Pure/General/json.scala
--- 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] =
diff -r bea49e443909 -r 5655af3ea5bd src/Pure/General/uuid.scala
--- /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 }
+}
diff -r bea49e443909 -r 5655af3ea5bd src/Pure/PIDE/headless.scala
--- 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 =>
         {
diff -r bea49e443909 -r 5655af3ea5bd src/Pure/ROOT.scala
--- 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()
 }
diff -r bea49e443909 -r 5655af3ea5bd src/Pure/Tools/server.scala
--- 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)
 
diff -r bea49e443909 -r 5655af3ea5bd src/Pure/Tools/server_commands.scala
--- 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)
diff -r bea49e443909 -r 5655af3ea5bd src/Pure/build-jars
--- 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
diff -r bea49e443909 -r 5655af3ea5bd src/Tools/VSCode/src/grammar.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": [
diff -r bea49e443909 -r 5655af3ea5bd src/Tools/jEdit/src/plugin.scala
--- 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))