prefer typed UUID;

--- a/src/Pure/General/json.scala	Fri Mar 16 22:20:09 2018 +0100
+++ b/src/Pure/General/json.scala	Fri Mar 16 22:50:56 2018 +0100
@@ -242,6 +242,17 @@
 
   object Value
   {
+    object UUID
+    {
+      def unapply(json: T): Option[java.util.UUID] =
+        json match {
+          case x: java.lang.String =>
+            try { Some(java.util.UUID.fromString(x)) }
+            catch { case _: IllegalArgumentException => None }
+          case _ => None
+        }
+    }
+
     object String {
       def unapply(json: T): Option[java.lang.String] =
         json match {
@@ -333,6 +344,9 @@
       case Some(json) => unapply(json)
     }
 
+  def uuid(obj: T, name: String): Option[UUID] =
+    value(obj, name, Value.UUID.unapply)
+
   def string(obj: T, name: String): Option[String] =
     value(obj, name, Value.String.unapply)
   def string_default(obj: T, name: String, default: => String = ""): Option[String] =

--- a/src/Pure/ROOT.scala	Fri Mar 16 22:20:09 2018 +0100
+++ b/src/Pure/ROOT.scala	Fri Mar 16 22:50:56 2018 +0100
@@ -21,4 +21,7 @@
   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/Thy/thy_resources.scala	Fri Mar 16 22:20:09 2018 +0100
+++ b/src/Pure/Thy/thy_resources.scala	Fri Mar 16 22:50:56 2018 +0100
@@ -68,7 +68,7 @@
       theories: List[(String, Position.T)],
       qualifier: String = Sessions.DRAFT,
       master_dir: String = "",
-      id: String = Library.UUID(),
+      id: UUID = UUID(),
       progress: Progress = No_Progress): Theories_Result =
     {
       val requirements =
@@ -112,10 +112,10 @@
 
   sealed case class State(
     theories: Map[Document.Node.Name, Theory] = Map.empty,
-    required: Multi_Map[Document.Node.Name, String] = Multi_Map.empty)
+    required: Multi_Map[Document.Node.Name, UUID] = Multi_Map.empty)
   {
     def update(theory_edits: List[((Document.Node.Name, Theory), List[Document.Edit_Text])],
-        new_required: Multi_Map[Document.Node.Name, String]): (List[Document.Edit_Text], State) =
+        new_required: Multi_Map[Document.Node.Name, UUID]): (List[Document.Edit_Text], State) =
     {
       val edits = theory_edits.flatMap(_._2)
       val st = State(theories ++ theory_edits.map(_._1), new_required)
@@ -171,7 +171,7 @@
 
   def load_theories(
     session: Session,
-    id: String,
+    id: UUID,
     theories: List[(String, Position.T)],
     qualifier: String = Sessions.DRAFT,
     master_dir: String = "",
@@ -203,7 +203,7 @@
     dependencies.theories
   }
 
-  def unload_theories(session: Session, id: String, theories: List[Document.Node.Name])
+  def unload_theories(session: Session, id: UUID, theories: List[Document.Node.Name])
   {
     val edits =
       state.change_result(st =>

--- a/src/Pure/Tools/server.scala	Fri Mar 16 22:20:09 2018 +0100
+++ b/src/Pure/Tools/server.scala	Fri Mar 16 22:50:56 2018 +0100
@@ -67,7 +67,7 @@
         "help" -> { case (_, ()) => table.keySet.toList.sorted },
         "echo" -> { case (_, t) => t },
         "shutdown" -> { case (context, ()) => context.server.close() },
-        "cancel" -> { case (context, JSON.Value.String(id)) => context.cancel_task(id) },
+        "cancel" -> { case (context, JSON.Value.UUID(id)) => context.cancel_task(id) },
         "session_build" ->
           { case (context, Server_Commands.Session_Build(args)) =>
               context.make_task(task =>
@@ -232,7 +232,7 @@
     def remove_task(task: Task): Unit =
       _tasks.change(_ - task)
 
-    def cancel_task(id: String): Unit =
+    def cancel_task(id: UUID): Unit =
       _tasks.change(tasks => { tasks.find(task => task.id == id).foreach(_.cancel); tasks })
 
     def close()
@@ -263,8 +263,8 @@
   {
     task =>
 
-    val id: String = Library.UUID()
-    val ident: JSON.Object.Entry = ("task" -> id)
+    val id: UUID = UUID()
+    val ident: JSON.Object.Entry = ("task" -> id.toString)
 
     val progress: Connection_Progress = context.progress(ident)
     def cancel { progress.stop }
@@ -473,12 +473,12 @@
 {
   server =>
 
-  private val _sessions = Synchronized(Map.empty[String, Thy_Resources.Session])
-  def err_session(id: String): Nothing = error("No session " + Library.single_quote(id))
-  def the_session(id: String): Thy_Resources.Session =
+  private val _sessions = Synchronized(Map.empty[UUID, Thy_Resources.Session])
+  def err_session(id: UUID): Nothing = error("No session " + Library.single_quote(id.toString))
+  def the_session(id: UUID): Thy_Resources.Session =
     _sessions.value.get(id) getOrElse err_session(id)
-  def add_session(entry: (String, Thy_Resources.Session)) { _sessions.change(_ + entry) }
-  def remove_session(id: String): Thy_Resources.Session =
+  def add_session(entry: (UUID, Thy_Resources.Session)) { _sessions.change(_ + entry) }
+  def remove_session(id: UUID): Thy_Resources.Session =
   {
     _sessions.change_result(sessions =>
       sessions.get(id) match {
@@ -492,7 +492,7 @@
   def close() { server_socket.close }
 
   def port: Int = server_socket.getLocalPort
-  val password: String = Library.UUID()
+  val password: String = UUID().toString
 
   override def toString: String = Server.print(port, password)
 

--- a/src/Pure/Tools/server_commands.scala	Fri Mar 16 22:20:09 2018 +0100
+++ b/src/Pure/Tools/server_commands.scala	Fri Mar 16 22:50:56 2018 +0100
@@ -117,7 +117,7 @@
       yield Args(build = build, print_mode = print_mode)
 
     def command(progress: Progress, args: Args, log: Logger = No_Logger)
-      : (JSON.Object.T, (String, Thy_Resources.Session)) =
+      : (JSON.Object.T, (UUID, Thy_Resources.Session)) =
     {
       val base_info = Session_Build.command(progress, args.build)._3
 
@@ -131,8 +131,8 @@
           progress = progress,
           log = log)
 
-      val id = Library.UUID()
-      val res = JSON.Object("session_name" -> base_info.session, "session_id" -> id)
+      val id = UUID()
+      val res = JSON.Object("session_name" -> base_info.session, "session_id" -> id.toString)
 
       (res, id -> session)
     }
@@ -140,8 +140,8 @@
 
   object Session_Stop
   {
-    def unapply(json: JSON.T): Option[String] =
-      JSON.string(json, "session_id")
+    def unapply(json: JSON.T): Option[UUID] =
+      JSON.uuid(json, "session_id")
 
     def command(session: Thy_Resources.Session): (JSON.Object.T, Process_Result) =
     {
@@ -156,14 +156,14 @@
   object Use_Theories
   {
     sealed case class Args(
-      session_id: String,
+      session_id: UUID,
       theories: List[(String, Position.T)],
       qualifier: String = default_qualifier,
       master_dir: String = "")
 
     def unapply(json: JSON.T): Option[Args] =
       for {
-        session_id <- JSON.string(json, "session_id")
+        session_id <- JSON.uuid(json, "session_id")
         theories <- JSON.list(json, "theories", unapply_name_pos _)
         qualifier <- JSON.string_default(json, "qualifier", default_qualifier)
         master_dir <- JSON.string_default(json, "master_dir")
@@ -172,7 +172,7 @@
 
     def command(args: Args,
       session: Thy_Resources.Session,
-      id: String = Library.UUID(),
+      id: UUID = UUID(),
       progress: Progress = No_Progress): (JSON.Object.T, Thy_Resources.Theories_Result) =
     {
       val result =

--- a/src/Pure/library.scala	Fri Mar 16 22:20:09 2018 +0100
+++ b/src/Pure/library.scala	Fri Mar 16 22:50:56 2018 +0100
@@ -270,9 +270,4 @@
 
   def proper_list[A](list: List[A]): Option[List[A]] =
     if (list == null || list.isEmpty) None else Some(list)
-
-
-  /* UUID */
-
-  def UUID(): String = java.util.UUID.randomUUID().toString
 }

--- a/src/Tools/VSCode/src/grammar.scala	Fri Mar 16 22:20:09 2018 +0100
+++ b/src/Tools/VSCode/src/grammar.scala	Fri Mar 16 22:50:56 2018 +0100
@@ -45,7 +45,7 @@
   "name": "Isabelle",
   "scopeName": "source.isabelle",
   "fileTypes": ["thy"],
-  "uuid": """ + JSON.Format(Library.UUID()) + """,
+  "uuid": """ + JSON.Format(UUID().toString) + """,
   "repository": {
     "comment": {
       "patterns": [

--- a/src/Tools/jEdit/src/plugin.scala	Fri Mar 16 22:20:09 2018 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Fri Mar 16 22:50:56 2018 +0100
@@ -413,7 +413,7 @@
 
   /* HTTP server */
 
-  val http_root: String = "/" + Library.UUID()
+  val http_root: String = "/" + UUID()
 
   val http_server: HTTP.Server = HTTP.server(Document_Model.http_handlers(http_root))