src/Pure/General/json.scala
changeset 69458 5655af3ea5bd
parent 68943 e564605d4cac
child 71298 93b097726667
--- 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] =