# HG changeset patch
# User wenzelm
# Date 1521216969 -3600
# Node ID 7eb4c966e156ea8453bc1589c71b51ebfc8a3ce0
# Parent  812ed06dadecdbe762dea00a4648c2e764647136
JSON representation for Position.T;

diff -r 812ed06dadec -r 7eb4c966e156 src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Fri Mar 16 16:44:14 2018 +0100
+++ b/src/Pure/General/position.scala	Fri Mar 16 17:16:09 2018 +0100
@@ -148,4 +148,35 @@
       Markup(Markup.POSITION, pos).markup(s)
     }
   }
+
+
+  /* JSON representation */
+
+  object JSON
+  {
+    def apply(pos: T): isabelle.JSON.Object.T =
+      isabelle.JSON.Object.empty ++
+        Line.unapply(pos).map(Line.name -> _) ++
+        Offset.unapply(pos).map(Offset.name -> _) ++
+        End_Offset.unapply(pos).map(End_Offset.name -> _) ++
+        File.unapply(pos).map(File.name -> _) ++
+        Id.unapply(pos).map(Id.name -> _)
+
+    def unapply(json: isabelle.JSON.T): Option[T] =
+      for {
+        line <- isabelle.JSON.int_default(json, Line.name)
+        offset <- isabelle.JSON.int_default(json, Offset.name)
+        end_offset <- isabelle.JSON.int_default(json, End_Offset.name)
+        file <- isabelle.JSON.string_default(json, File.name)
+        id <- isabelle.JSON.long_default(json, Id.name)
+      }
+      yield {
+        def defined(name: String): Boolean = isabelle.JSON.value(json, name).isDefined
+        (if (defined(Line.name)) Line(line) else Nil) :::
+        (if (defined(Offset.name)) Offset(offset) else Nil) :::
+        (if (defined(End_Offset.name)) End_Offset(end_offset) else Nil) :::
+        (if (defined(File.name)) File(file) else Nil) :::
+        (if (defined(Id.name)) Id(id) else Nil)
+      }
+  }
 }