# HG changeset patch
# User wenzelm
# Date 1570719107 -7200
# Node ID cb70d84a9f5e8ba34248a78edd555f2b8dbe65bd
# Parent  730251503341e3cee5d9895a2787073caaa57de4
more compact XML representation;

diff -r 730251503341 -r cb70d84a9f5e src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Thu Oct 10 15:52:30 2019 +0200
+++ b/src/Pure/PIDE/xml.ML	Thu Oct 10 16:51:47 2019 +0200
@@ -11,6 +11,7 @@
   type 'a A
   type 'a T
   type 'a V
+  type 'a P
   val int_atom: int A
   val bool_atom: bool A
   val unit_atom: unit A
@@ -290,6 +291,7 @@
 type 'a A = 'a -> string;
 type 'a T = 'a -> body;
 type 'a V = 'a -> string list * body;
+type 'a P = 'a -> string list;
 
 
 (* atomic values *)
@@ -347,6 +349,7 @@
 type 'a A = string -> 'a;
 type 'a T = body -> 'a;
 type 'a V = string list * body -> 'a;
+type 'a P = string list -> 'a;
 
 
 (* atomic values *)
diff -r 730251503341 -r cb70d84a9f5e src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Thu Oct 10 15:52:30 2019 +0200
+++ b/src/Pure/PIDE/xml.scala	Thu Oct 10 16:51:47 2019 +0200
@@ -241,6 +241,7 @@
   {
     type T[A] = A => XML.Body
     type V[A] = PartialFunction[A, (List[String], XML.Body)]
+    type P[A] = PartialFunction[A, List[String]]
 
 
     /* atomic values */
@@ -309,6 +310,7 @@
   {
     type T[A] = XML.Body => A
     type V[A] = (List[String], XML.Body) => A
+    type P[A] = PartialFunction[List[String], A]
 
 
     /* atomic values */
diff -r 730251503341 -r cb70d84a9f5e src/Pure/term_xml.ML
--- a/src/Pure/term_xml.ML	Thu Oct 10 15:52:30 2019 +0200
+++ b/src/Pure/term_xml.ML	Thu Oct 10 16:51:47 2019 +0200
@@ -7,10 +7,13 @@
 signature TERM_XML_OPS =
 sig
   type 'a T
+  type 'a P
+  val indexname: indexname P
   val sort: sort T
+  val typ_raw: typ T
+  val term_raw: term T
   val typ: typ T
   val term: Consts.T -> term T
-  val term_raw: term T
 end
 
 signature TERM_XML =
@@ -27,29 +30,33 @@
 
 open XML.Encode;
 
+fun indexname (a, b) = if b = 0 then [a] else [a, int_atom b];
+
 val sort = list string;
 
-fun typ T = T |> variant
- [fn Type (a, b) => ([a], list typ b),
+fun typ_raw T = T |> variant
+ [fn Type (a, b) => ([a], list typ_raw b),
   fn TFree (a, b) => ([a], sort b),
-  fn TVar ((a, b), c) => ([a, int_atom b], sort c)];
+  fn TVar (a, b) => (indexname a, sort b)];
+
+fun term_raw t = t |> variant
+ [fn Const (a, b) => ([a], typ_raw b),
+  fn Free (a, b) => ([a], typ_raw b),
+  fn Var (a, b) => (indexname a, typ_raw b),
+  fn Bound a => ([int_atom a], []),
+  fn Abs (a, b, c) => ([a], pair typ_raw term_raw (b, c)),
+  fn op $ a => ([], pair term_raw term_raw a)];
+
+fun typ T = option typ_raw (if T = dummyT then NONE else SOME T);
 
 fun term consts t = t |> variant
  [fn Const (a, b) => ([a], list typ (Consts.typargs consts (a, b))),
   fn Free (a, b) => ([a], typ b),
-  fn Var ((a, b), c) => ([a, int_atom b], typ c),
+  fn Var (a, b) => (indexname a, typ b),
   fn Bound a => ([int_atom a], []),
   fn Abs (a, b, c) => ([a], pair typ (term consts) (b, c)),
   fn op $ a => ([], pair (term consts) (term consts) a)];
 
-fun term_raw t = t |> variant
- [fn Const (a, b) => ([a], typ b),
-  fn Free (a, b) => ([a], typ b),
-  fn Var ((a, b), c) => ([a, int_atom b], typ c),
-  fn Bound a => ([int_atom a], []),
-  fn Abs (a, b, c) => ([a], pair typ term_raw (b, c)),
-  fn op $ a => ([], pair term_raw term_raw a)];
-
 end;
 
 structure Decode =
@@ -57,29 +64,34 @@
 
 open XML.Decode;
 
+fun indexname [a] = (a, 0)
+  | indexname [a, b] = (a, int_atom b);
+
 val sort = list string;
 
-fun typ T = T |> variant
- [fn ([a], b) => Type (a, list typ b),
+fun typ_raw body = body |> variant
+ [fn ([a], b) => Type (a, list typ_raw b),
   fn ([a], b) => TFree (a, sort b),
-  fn ([a, b], c) => TVar ((a, int_atom b), sort c)];
+  fn (a, b) => TVar (indexname a, sort b)];
 
-fun term consts t = t |> variant
+fun term_raw body = body |> variant
+ [fn ([a], b) => Const (a, typ_raw b),
+  fn ([a], b) => Free (a, typ_raw b),
+  fn (a, b) => Var (indexname a, typ_raw b),
+  fn ([a], []) => Bound (int_atom a),
+  fn ([a], b) => let val (c, d) = pair typ_raw term_raw b in Abs (a, c, d) end,
+  fn ([], a) => op $ (pair term_raw term_raw a)];
+
+val typ = option typ_raw #> the_default dummyT;
+
+fun term consts body = body |> variant
  [fn ([a], b) => Const (a, Consts.instance consts (a, list typ b)),
   fn ([a], b) => Free (a, typ b),
-  fn ([a, b], c) => Var ((a, int_atom b), typ c),
+  fn (a, b) => Var (indexname a, typ b),
   fn ([a], []) => Bound (int_atom a),
   fn ([a], b) => let val (c, d) = pair typ (term consts) b in Abs (a, c, d) end,
   fn ([], a) => op $ (pair (term consts) (term consts) a)];
 
-fun term_raw t = t |> variant
- [fn ([a], b) => Const (a, typ b),
-  fn ([a], b) => Free (a, typ b),
-  fn ([a, b], c) => Var ((a, int_atom b), typ c),
-  fn ([a], []) => Bound (int_atom a),
-  fn ([a], b) => let val (c, d) = pair typ term_raw b in Abs (a, c, d) end,
-  fn ([], a) => op $ (pair term_raw term_raw a)];
-
 end;
 
 end;
diff -r 730251503341 -r cb70d84a9f5e src/Pure/term_xml.scala
--- a/src/Pure/term_xml.scala	Thu Oct 10 15:52:30 2019 +0200
+++ b/src/Pure/term_xml.scala	Thu Oct 10 16:51:47 2019 +0200
@@ -15,19 +15,26 @@
   {
     import XML.Encode._
 
+    val indexname: P[Indexname] =
+      { case Indexname(a, 0) => List(a)
+        case Indexname(a, b) => List(a, int_atom(b)) }
+
     val sort: T[Sort] = list(string)
 
-    def typ: T[Typ] =
+    def typ_raw: T[Typ] =
       variant[Typ](List(
-        { case Type(a, b) => (List(a), list(typ)(b)) },
+        { case Type(a, b) => (List(a), list(typ_raw)(b)) },
         { case TFree(a, b) => (List(a), sort(b)) },
-        { case TVar(Indexname(a, b), c) => (List(a, int_atom(b)), sort(c)) }))
+        { case TVar(a, b) => (indexname(a), sort(b)) }))
+
+    val typ: T[Typ] =
+      { case t => option(typ_raw)(if (t == dummyT) None else Some(t)) }
 
     def term: T[Term] =
       variant[Term](List(
         { case Const(a, b) => (List(a), list(typ)(b)) },
         { case Free(a, b) => (List(a), typ(b)) },
-        { case Var(Indexname(a, b), c) => (List(a, int_atom(b)), typ(c)) },
+        { case Var(a, b) => (indexname(a), typ(b)) },
         { case Bound(a) => (List(int_atom(a)), Nil) },
         { case Abs(a, b, c) => (List(a), pair(typ, term)(b, c)) },
         { case App(a, b) => (Nil, pair(term, term)(a, b)) }))
@@ -37,19 +44,25 @@
   {
     import XML.Decode._
 
+    val indexname: P[Indexname] =
+      { case List(a) => Indexname(a, 0)
+        case List(a, b) => Indexname(a, int_atom(b)) }
+
     val sort: T[Sort] = list(string)
 
-    def typ: T[Typ] =
+    def typ_raw: T[Typ] =
       variant[Typ](List(
-        { case (List(a), b) => Type(a, list(typ)(b)) },
+        { case (List(a), b) => Type(a, list(typ_raw)(b)) },
         { case (List(a), b) => TFree(a, sort(b)) },
-        { case (List(a, b), c) => TVar(Indexname(a, int_atom(b)), sort(c)) }))
+        { case (a, b) => TVar(indexname(a), sort(b)) }))
+
+    def typ(body: XML.Body): Typ = option(typ_raw)(body).getOrElse(dummyT)
 
     def term: T[Term] =
       variant[Term](List(
         { case (List(a), b) => Const(a, list(typ)(b)) },
         { case (List(a), b) => Free(a, typ(b)) },
-        { case (List(a, b), c) => Var(Indexname(a, int_atom(b)), typ(c)) },
+        { case (a, b) => Var(indexname(a), typ(b)) },
         { case (List(a), Nil) => Bound(int_atom(a)) },
         { case (List(a), b) => val (c, d) = pair(typ, term)(b); Abs(a, c, d) },
         { case (Nil, a) => val (b, c) = pair(term, term)(a); App(b, c) }))