inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
authorwenzelm
Sun Jul 10 20:59:04 2011 +0200 (2011-07-10)
changeset 4373170072780e095
parent 43730 a0ed7bc688b5
child 43743 8786e36b8142
inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
tuned signature;
NEWS
src/Pure/General/xml_data.ML
src/Pure/General/xml_data.scala
src/Pure/General/yxml.ML
src/Pure/Isar/token.ML
src/Pure/PIDE/isar_document.ML
src/Pure/PIDE/isar_document.scala
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/Thy/thy_header.scala
src/Pure/Tools/find_theorems.ML
src/Pure/term.scala
src/Pure/term_xml.ML
     1.1 --- a/NEWS	Sun Jul 10 17:58:11 2011 +0200
     1.2 +++ b/NEWS	Sun Jul 10 20:59:04 2011 +0200
     1.3 @@ -146,6 +146,12 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* The inner syntax of sort/type/term/prop supports inlined YXML
     1.8 +representations within quoted string tokens.  By encoding logical
     1.9 +entities via Term_XML (in ML or Scala) concrete syntax can be
    1.10 +bypassed, which is particularly useful for producing bits of text
    1.11 +under external program control.
    1.12 +
    1.13  * Antiquotations for ML and document preparation are managed as theory
    1.14  data, which requires explicit setup.
    1.15  
     2.1 --- a/src/Pure/General/xml_data.ML	Sun Jul 10 17:58:11 2011 +0200
     2.2 +++ b/src/Pure/General/xml_data.ML	Sun Jul 10 20:59:04 2011 +0200
     2.3 @@ -21,18 +21,18 @@
     2.4  
     2.5  signature XML_DATA =
     2.6  sig
     2.7 -  structure Make: XML_DATA_OPS where type 'a T = 'a -> XML.body
     2.8 +  structure Encode: XML_DATA_OPS where type 'a T = 'a -> XML.body
     2.9    exception XML_ATOM of string
    2.10    exception XML_BODY of XML.body
    2.11 -  structure Dest: XML_DATA_OPS where type 'a T = XML.body -> 'a
    2.12 +  structure Decode: XML_DATA_OPS where type 'a T = XML.body -> 'a
    2.13  end;
    2.14  
    2.15  structure XML_Data: XML_DATA =
    2.16  struct
    2.17  
    2.18 -(** make **)
    2.19 +(** encode **)
    2.20  
    2.21 -structure Make =
    2.22 +structure Encode =
    2.23  struct
    2.24  
    2.25  type 'a T = 'a -> XML.body;
    2.26 @@ -83,12 +83,12 @@
    2.27  
    2.28  
    2.29  
    2.30 -(** dest **)
    2.31 +(** decode **)
    2.32  
    2.33  exception XML_ATOM of string;
    2.34  exception XML_BODY of XML.tree list;
    2.35  
    2.36 -structure Dest =
    2.37 +structure Decode =
    2.38  struct
    2.39  
    2.40  type 'a T = XML.body -> 'a;
     3.1 --- a/src/Pure/General/xml_data.scala	Sun Jul 10 17:58:11 2011 +0200
     3.2 +++ b/src/Pure/General/xml_data.scala	Sun Jul 10 20:59:04 2011 +0200
     3.3 @@ -10,9 +10,9 @@
     3.4  
     3.5  object XML_Data
     3.6  {
     3.7 -  /** make **/
     3.8 +  /** encode **/
     3.9  
    3.10 -  object Make
    3.11 +  object Encode
    3.12    {
    3.13      type T[A] = A => XML.Body
    3.14  
    3.15 @@ -76,12 +76,12 @@
    3.16  
    3.17  
    3.18  
    3.19 -  /** dest **/
    3.20 +  /** decode **/
    3.21  
    3.22    class XML_Atom(s: String) extends Exception(s)
    3.23    class XML_Body(body: XML.Body) extends Exception
    3.24  
    3.25 -  object Dest
    3.26 +  object Decode
    3.27    {
    3.28      type T[A] = XML.Body => A
    3.29  
     4.1 --- a/src/Pure/General/yxml.ML	Sun Jul 10 17:58:11 2011 +0200
     4.2 +++ b/src/Pure/General/yxml.ML	Sun Jul 10 20:59:04 2011 +0200
     4.3 @@ -16,6 +16,7 @@
     4.4  signature YXML =
     4.5  sig
     4.6    val escape_controls: string -> string
     4.7 +  val detect: string -> bool
     4.8    val output_markup: Markup.T -> string * string
     4.9    val element: string -> XML.attributes -> string list -> string
    4.10    val string_of_body: XML.body -> string
    4.11 @@ -49,6 +50,8 @@
    4.12  val XY = X ^ Y;
    4.13  val XYX = XY ^ X;
    4.14  
    4.15 +val detect = exists_string (fn s => s = X);
    4.16 +
    4.17  
    4.18  (* output *)
    4.19  
     5.1 --- a/src/Pure/Isar/token.ML	Sun Jul 10 17:58:11 2011 +0200
     5.2 +++ b/src/Pure/Isar/token.ML	Sun Jul 10 20:59:04 2011 +0200
     5.3 @@ -180,8 +180,9 @@
     5.4  
     5.5  (* token content *)
     5.6  
     5.7 -fun source_of (Token ((source, (pos, _)), _, _)) =
     5.8 -  YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source]));
     5.9 +fun source_of (Token ((source, (pos, _)), (_, x), _)) =
    5.10 +  if YXML.detect x then x
    5.11 +  else YXML.string_of (XML.Elem (Markup.token (Position.properties_of pos), [XML.Text source]));
    5.12  
    5.13  fun source_position_of (Token ((source, (pos, _)), _, _)) = (source, pos);
    5.14  
     6.1 --- a/src/Pure/PIDE/isar_document.ML	Sun Jul 10 17:58:11 2011 +0200
     6.2 +++ b/src/Pure/PIDE/isar_document.ML	Sun Jul 10 20:59:04 2011 +0200
     6.3 @@ -18,10 +18,10 @@
     6.4          val old_id = Document.parse_id old_id_string;
     6.5          val new_id = Document.parse_id new_id_string;
     6.6          val edits = YXML.parse_body edits_yxml |>
     6.7 -          let open XML_Data.Dest
     6.8 +          let open XML_Data.Decode
     6.9            in list (pair string (option (list (pair (option int) (option int))))) end;
    6.10          val headers = YXML.parse_body headers_yxml |>
    6.11 -          let open XML_Data.Dest
    6.12 +          let open XML_Data.Decode
    6.13            in list (pair string (triple string (list string) (list string))) end;
    6.14  
    6.15        val await_cancellation = Document.cancel_execution state;
     7.1 --- a/src/Pure/PIDE/isar_document.scala	Sun Jul 10 17:58:11 2011 +0200
     7.2 +++ b/src/Pure/PIDE/isar_document.scala	Sun Jul 10 20:59:04 2011 +0200
     7.3 @@ -143,12 +143,12 @@
     7.4        edits: List[Document.Edit_Command_ID], headers: List[(String, Thy_Header.Header)])
     7.5    {
     7.6      val arg1 =
     7.7 -    { import XML_Data.Make._
     7.8 +    { import XML_Data.Encode._
     7.9        list(pair(string, option(list(pair(option(long), option(long))))))(edits) }
    7.10  
    7.11      val arg2 =
    7.12 -    { import XML_Data.Make._
    7.13 -      list(pair(string, Thy_Header.make_xml_data))(headers) }
    7.14 +    { import XML_Data.Encode._
    7.15 +      list(pair(string, Thy_Header.encode_xml_data))(headers) }
    7.16  
    7.17      input("Isar_Document.edit_version",
    7.18        Document.ID(old_id), Document.ID(new_id),
     8.1 --- a/src/Pure/Syntax/syntax.ML	Sun Jul 10 17:58:11 2011 +0200
     8.2 +++ b/src/Pure/Syntax/syntax.ML	Sun Jul 10 20:59:04 2011 +0200
     8.3 @@ -17,7 +17,8 @@
     8.4    val ambiguity_level: int Config.T
     8.5    val ambiguity_limit: int Config.T
     8.6    val read_token: string -> Symbol_Pos.T list * Position.T
     8.7 -  val parse_token: Proof.context -> Markup.T -> string -> Symbol_Pos.T list * Position.T
     8.8 +  val parse_token: Proof.context -> (XML.tree list -> 'a) ->
     8.9 +    Markup.T -> (Symbol_Pos.T list * Position.T -> 'a) -> string -> 'a
    8.10    val parse_sort: Proof.context -> string -> sort
    8.11    val parse_typ: Proof.context -> string -> typ
    8.12    val parse_term: Proof.context -> string -> term
    8.13 @@ -193,11 +194,10 @@
    8.14    Config.int (Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10));
    8.15  
    8.16  
    8.17 -(* read token -- with optional YXML encoding of position *)
    8.18 +(* outer syntax token -- with optional YXML content *)
    8.19  
    8.20 -fun read_token str =
    8.21 +fun explode_token tree =
    8.22    let
    8.23 -    val tree = YXML.parse str handle Fail msg => error msg;
    8.24      val text = XML.content_of [tree];
    8.25      val pos =
    8.26        (case tree of
    8.27 @@ -207,15 +207,26 @@
    8.28        | XML.Text _ => Position.none);
    8.29    in (Symbol_Pos.explode (text, pos), pos) end;
    8.30  
    8.31 +fun read_token str = explode_token (YXML.parse str handle Fail msg => error msg);
    8.32 +
    8.33 +fun parse_token ctxt decode markup parse str =
    8.34 +  let
    8.35 +    fun parse_tree tree =
    8.36 +      let
    8.37 +        val (syms, pos) = explode_token tree;
    8.38 +        val _ = Context_Position.report ctxt pos markup;
    8.39 +      in parse (syms, pos) end;
    8.40 +  in
    8.41 +    (case YXML.parse_body str handle Fail msg => error msg of
    8.42 +      body as [tree as XML.Elem ((name, _), _)] =>
    8.43 +        if name = Markup.tokenN then parse_tree tree else decode body
    8.44 +    | [tree as XML.Text _] => parse_tree tree
    8.45 +    | body => decode body)
    8.46 +  end;
    8.47 +
    8.48  
    8.49  (* (un)parsing *)
    8.50  
    8.51 -fun parse_token ctxt markup str =
    8.52 -  let
    8.53 -    val (syms, pos) = read_token str;
    8.54 -    val _ = Context_Position.report ctxt pos markup;
    8.55 -  in (syms, pos) end;
    8.56 -
    8.57  val parse_sort = operation #parse_sort;
    8.58  val parse_typ = operation #parse_typ;
    8.59  val parse_term = operation #parse_term;
     9.1 --- a/src/Pure/Syntax/syntax_phases.ML	Sun Jul 10 17:58:11 2011 +0200
     9.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Sun Jul 10 20:59:04 2011 +0200
     9.3 @@ -320,80 +320,79 @@
     9.4    cat_error msg ("Failed to parse " ^ kind ^
     9.5      Markup.markup Markup.report (Context_Position.reported_text ctxt pos Markup.bad ""));
     9.6  
     9.7 -fun parse_sort ctxt text =
     9.8 -  let
     9.9 -    val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
    9.10 -    val S =
    9.11 +fun parse_sort ctxt =
    9.12 +  Syntax.parse_token ctxt Term_XML.Decode.sort Markup.sort
    9.13 +    (fn (syms, pos) =>
    9.14        parse_raw ctxt "sort" (syms, pos)
    9.15        |> report_result ctxt pos
    9.16        |> sort_of_term
    9.17 -      handle ERROR msg => parse_failed ctxt pos msg "sort";
    9.18 -  in Type.minimize_sort (Proof_Context.tsig_of ctxt) S end;
    9.19 +      |> Type.minimize_sort (Proof_Context.tsig_of ctxt)
    9.20 +      handle ERROR msg => parse_failed ctxt pos msg "sort");
    9.21  
    9.22 -fun parse_typ ctxt text =
    9.23 -  let
    9.24 -    val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
    9.25 -    val T =
    9.26 +fun parse_typ ctxt =
    9.27 +  Syntax.parse_token ctxt Term_XML.Decode.typ Markup.typ
    9.28 +    (fn (syms, pos) =>
    9.29        parse_raw ctxt "type" (syms, pos)
    9.30        |> report_result ctxt pos
    9.31        |> (fn t => typ_of_term (Proof_Context.get_sort ctxt (term_sorts t)) t)
    9.32 -      handle ERROR msg => parse_failed ctxt pos msg "type";
    9.33 -  in T end;
    9.34 +      handle ERROR msg => parse_failed ctxt pos msg "type");
    9.35  
    9.36 -fun parse_term is_prop ctxt text =
    9.37 +fun parse_term is_prop ctxt =
    9.38    let
    9.39      val (markup, kind, root, constrain) =
    9.40        if is_prop
    9.41        then (Markup.prop, "proposition", "prop", Type.constraint propT)
    9.42        else (Markup.term, "term", Config.get ctxt Syntax.root, I);
    9.43 -    val (syms, pos) = Syntax.parse_token ctxt markup text;
    9.44 +    val decode = constrain o Term_XML.Decode.term;
    9.45    in
    9.46 -    let
    9.47 -      val results = parse_raw ctxt root (syms, pos) |> map (decode_term ctxt);
    9.48 -      val ambiguity = length (proper_results results);
    9.49 -
    9.50 -      val level = Config.get ctxt Syntax.ambiguity_level;
    9.51 -      val limit = Config.get ctxt Syntax.ambiguity_limit;
    9.52 +    Syntax.parse_token ctxt decode markup
    9.53 +      (fn (syms, pos) =>
    9.54 +        let
    9.55 +          val results = parse_raw ctxt root (syms, pos) |> map (decode_term ctxt);
    9.56 +          val ambiguity = length (proper_results results);
    9.57  
    9.58 -      val ambig_msg =
    9.59 -        if ambiguity > 1 andalso ambiguity <= level then
    9.60 -          ["Got more than one parse tree.\n\
    9.61 -          \Retry with smaller syntax_ambiguity_level for more information."]
    9.62 -        else [];
    9.63 +          val level = Config.get ctxt Syntax.ambiguity_level;
    9.64 +          val limit = Config.get ctxt Syntax.ambiguity_limit;
    9.65  
    9.66 -      (*brute-force disambiguation via type-inference*)
    9.67 -      fun check t = (Syntax.check_term ctxt (constrain t); Exn.Result t)
    9.68 -        handle exn as ERROR _ => Exn.Exn exn;
    9.69 +          val ambig_msg =
    9.70 +            if ambiguity > 1 andalso ambiguity <= level then
    9.71 +              ["Got more than one parse tree.\n\
    9.72 +              \Retry with smaller syntax_ambiguity_level for more information."]
    9.73 +            else [];
    9.74 +
    9.75 +          (*brute-force disambiguation via type-inference*)
    9.76 +          fun check t = (Syntax.check_term ctxt (constrain t); Exn.Result t)
    9.77 +            handle exn as ERROR _ => Exn.Exn exn;
    9.78  
    9.79 -      val results' =
    9.80 -        if ambiguity > 1 then
    9.81 -          (Par_List.map_name "Syntax_Phases.parse_term" o apsnd o Exn.maps_result)
    9.82 -            check results
    9.83 -        else results;
    9.84 -      val reports' = fst (hd results');
    9.85 +          val results' =
    9.86 +            if ambiguity > 1 then
    9.87 +              (Par_List.map_name "Syntax_Phases.parse_term" o apsnd o Exn.maps_result)
    9.88 +                check results
    9.89 +            else results;
    9.90 +          val reports' = fst (hd results');
    9.91  
    9.92 -      val errs = map snd (failed_results results');
    9.93 -      val checked = map snd (proper_results results');
    9.94 -      val len = length checked;
    9.95 +          val errs = map snd (failed_results results');
    9.96 +          val checked = map snd (proper_results results');
    9.97 +          val len = length checked;
    9.98  
    9.99 -      val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt);
   9.100 -    in
   9.101 -      if len = 0 then
   9.102 -        report_result ctxt pos
   9.103 -          [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msg @ errs)))]
   9.104 -      else if len = 1 then
   9.105 -        (if ambiguity > level then
   9.106 -          Context_Position.if_visible ctxt warning
   9.107 -            "Fortunately, only one parse tree is type correct.\n\
   9.108 -            \You may still want to disambiguate your grammar or your input."
   9.109 -        else (); report_result ctxt pos results')
   9.110 -      else
   9.111 -        report_result ctxt pos
   9.112 -          [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg @
   9.113 -            (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
   9.114 -              (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
   9.115 -              map show_term (take limit checked))))))]
   9.116 -    end handle ERROR msg => parse_failed ctxt pos msg kind
   9.117 +          val show_term = Syntax.string_of_term (Config.put Printer.show_brackets true ctxt);
   9.118 +        in
   9.119 +          if len = 0 then
   9.120 +            report_result ctxt pos
   9.121 +              [(reports', Exn.Exn (Exn.EXCEPTIONS (map ERROR ambig_msg @ errs)))]
   9.122 +          else if len = 1 then
   9.123 +            (if ambiguity > level then
   9.124 +              Context_Position.if_visible ctxt warning
   9.125 +                "Fortunately, only one parse tree is type correct.\n\
   9.126 +                \You may still want to disambiguate your grammar or your input."
   9.127 +            else (); report_result ctxt pos results')
   9.128 +          else
   9.129 +            report_result ctxt pos
   9.130 +              [(reports', Exn.Exn (ERROR (cat_lines (ambig_msg @
   9.131 +                (("Ambiguous input, " ^ string_of_int len ^ " terms are type correct" ^
   9.132 +                  (if len <= limit then "" else " (" ^ string_of_int limit ^ " displayed)") ^ ":") ::
   9.133 +                  map show_term (take limit checked))))))]
   9.134 +        end handle ERROR msg => parse_failed ctxt pos msg kind)
   9.135    end;
   9.136  
   9.137  
    10.1 --- a/src/Pure/Thy/thy_header.scala	Sun Jul 10 17:58:11 2011 +0200
    10.2 +++ b/src/Pure/Thy/thy_header.scala	Sun Jul 10 20:59:04 2011 +0200
    10.3 @@ -31,10 +31,10 @@
    10.4        Header(f(name), imports.map(f), uses.map(f))
    10.5    }
    10.6  
    10.7 -  val make_xml_data: XML_Data.Make.T[Header] =
    10.8 +  val encode_xml_data: XML_Data.Encode.T[Header] =
    10.9    {
   10.10      case Header(name, imports, uses) =>
   10.11 -      import XML_Data.Make._
   10.12 +      import XML_Data.Encode._
   10.13        triple(string, list(string), list(string))(name, imports, uses)
   10.14    }
   10.15  
    11.1 --- a/src/Pure/Tools/find_theorems.ML	Sun Jul 10 17:58:11 2011 +0200
    11.2 +++ b/src/Pure/Tools/find_theorems.ML	Sun Jul 10 20:59:04 2011 +0200
    11.3 @@ -139,8 +139,8 @@
    11.4            |> (if rem_dups then cons ("rem_dups", "") else I)
    11.5            |> (if is_some limit then cons ("limit", Markup.print_int (the limit)) else I);
    11.6        in
    11.7 -        XML.Elem (("Query", properties), XML_Data.Make.list
    11.8 -          (XML_Data.Make.pair XML_Data.Make.bool (single o xml_of_criterion)) criteria)
    11.9 +        XML.Elem (("Query", properties), XML_Data.Encode.list
   11.10 +          (XML_Data.Encode.pair XML_Data.Encode.bool (single o xml_of_criterion)) criteria)
   11.11        end
   11.12    | xml_of_query _ = raise Fail "cannot serialize goal";
   11.13  
   11.14 @@ -149,7 +149,7 @@
   11.15          val rem_dups = Properties.defined properties "rem_dups";
   11.16          val limit = Properties.get properties "limit" |> Option.map Markup.parse_int;
   11.17          val criteria =
   11.18 -          XML_Data.Dest.list (XML_Data.Dest.pair XML_Data.Dest.bool 
   11.19 +          XML_Data.Decode.list (XML_Data.Decode.pair XML_Data.Decode.bool
   11.20              (criterion_of_xml o the_single)) body;
   11.21        in
   11.22          {goal=NONE, limit=limit, rem_dups=rem_dups, criteria=criteria}
   11.23 @@ -190,12 +190,12 @@
   11.24      val properties =
   11.25        if is_some opt_found then [("found", Markup.print_int (the opt_found))] else [];
   11.26    in
   11.27 -    XML.Elem (("Result", properties), XML_Data.Make.list (single o xml_of_theorem) theorems)
   11.28 +    XML.Elem (("Result", properties), XML_Data.Encode.list (single o xml_of_theorem) theorems)
   11.29    end;
   11.30  
   11.31  fun result_of_xml (XML.Elem (("Result", properties), body)) =
   11.32        (Properties.get properties "found" |> Option.map Markup.parse_int,
   11.33 -       XML_Data.Dest.list (theorem_of_xml o the_single) body)
   11.34 +       XML_Data.Decode.list (theorem_of_xml o the_single) body)
   11.35    | result_of_xml tree = raise XML_Syntax.XML ("result_of_xml: bad tree", tree);
   11.36  
   11.37  fun prop_of (Internal (_, thm)) = Thm.full_prop_of thm
    12.1 --- a/src/Pure/term.scala	Sun Jul 10 17:58:11 2011 +0200
    12.2 +++ b/src/Pure/term.scala	Sun Jul 10 20:59:04 2011 +0200
    12.3 @@ -31,58 +31,61 @@
    12.4    case class Bound(index: Int) extends Term
    12.5    case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term
    12.6    case class App(fun: Term, arg: Term) extends Term
    12.7 +}
    12.8 +
    12.9 +
   12.10 +object Term_XML
   12.11 +{
   12.12 +  import Term._
   12.13  
   12.14  
   12.15    /* XML data representation */
   12.16  
   12.17 -  object XML
   12.18 +  object Encode
   12.19    {
   12.20 -    object Make
   12.21 -    {
   12.22 -      import XML_Data.Make._
   12.23 +    import XML_Data.Encode._
   12.24  
   12.25 -      val indexname: T[Indexname] = pair(string, int)
   12.26 +    val indexname: T[Indexname] = pair(string, int)
   12.27  
   12.28 -      val sort: T[Sort] = list(string)
   12.29 +    val sort: T[Sort] = list(string)
   12.30  
   12.31 -      def typ: T[Typ] =
   12.32 -        variant[Typ](List(
   12.33 -          { case Type(a, b) => pair(string, list(typ))((a, b)) },
   12.34 -          { case TFree(a, b) => pair(string, sort)((a, b)) },
   12.35 -          { case TVar(a, b) => pair(indexname, sort)((a, b)) }))
   12.36 +    def typ: T[Typ] =
   12.37 +      variant[Typ](List(
   12.38 +        { case Type(a, b) => pair(string, list(typ))((a, b)) },
   12.39 +        { case TFree(a, b) => pair(string, sort)((a, b)) },
   12.40 +        { case TVar(a, b) => pair(indexname, sort)((a, b)) }))
   12.41  
   12.42 -      def term: T[Term] =
   12.43 -        variant[Term](List(
   12.44 -          { case Const(a, b) => pair(string, typ)((a, b)) },
   12.45 -          { case Free(a, b) => pair(string, typ)((a, b)) },
   12.46 -          { case Var(a, b) => pair(indexname, typ)((a, b)) },
   12.47 -          { case Bound(a) => int(a) },
   12.48 -          { case Abs(a, b, c) => triple(string, typ, term)((a, b, c)) },
   12.49 -          { case App(a, b) => pair(term, term)((a, b)) }))
   12.50 -    }
   12.51 +    def term: T[Term] =
   12.52 +      variant[Term](List(
   12.53 +        { case Const(a, b) => pair(string, typ)((a, b)) },
   12.54 +        { case Free(a, b) => pair(string, typ)((a, b)) },
   12.55 +        { case Var(a, b) => pair(indexname, typ)((a, b)) },
   12.56 +        { case Bound(a) => int(a) },
   12.57 +        { case Abs(a, b, c) => triple(string, typ, term)((a, b, c)) },
   12.58 +        { case App(a, b) => pair(term, term)((a, b)) }))
   12.59 +  }
   12.60  
   12.61 -    object Dest
   12.62 -    {
   12.63 -      import XML_Data.Dest._
   12.64 +  object Decode
   12.65 +  {
   12.66 +    import XML_Data.Decode._
   12.67  
   12.68 -      val indexname: T[Indexname] = pair(string, int)
   12.69 +    val indexname: T[Indexname] = pair(string, int)
   12.70  
   12.71 -      val sort: T[Sort] = list(string)
   12.72 +    val sort: T[Sort] = list(string)
   12.73  
   12.74 -      def typ: T[Typ] =
   12.75 -        variant[Typ](List(
   12.76 -          (x => { val (a, b) = pair(string, list(typ))(x); Type(a, b) }),
   12.77 -          (x => { val (a, b) = pair(string, sort)(x); TFree(a, b) }),
   12.78 -          (x => { val (a, b) = pair(indexname, sort)(x); TVar(a, b) })))
   12.79 +    def typ: T[Typ] =
   12.80 +      variant[Typ](List(
   12.81 +        (x => { val (a, b) = pair(string, list(typ))(x); Type(a, b) }),
   12.82 +        (x => { val (a, b) = pair(string, sort)(x); TFree(a, b) }),
   12.83 +        (x => { val (a, b) = pair(indexname, sort)(x); TVar(a, b) })))
   12.84  
   12.85 -      def term: T[Term] =
   12.86 -        variant[Term](List(
   12.87 -          (x => { val (a, b) = pair(string, typ)(x); Const(a, b) }),
   12.88 -          (x => { val (a, b) = pair(string, typ)(x); Free(a, b) }),
   12.89 -          (x => { val (a, b) = pair(indexname, typ)(x); Var(a, b) }),
   12.90 -          (x => Bound(int(x))),
   12.91 -          (x => { val (a, b, c) = triple(string, typ, term)(x); Abs(a, b, c) }),
   12.92 -          (x => { val (a, b) = pair(term, term)(x); App(a, b) })))
   12.93 -    }
   12.94 +    def term: T[Term] =
   12.95 +      variant[Term](List(
   12.96 +        (x => { val (a, b) = pair(string, typ)(x); Const(a, b) }),
   12.97 +        (x => { val (a, b) = pair(string, typ)(x); Free(a, b) }),
   12.98 +        (x => { val (a, b) = pair(indexname, typ)(x); Var(a, b) }),
   12.99 +        (x => Bound(int(x))),
  12.100 +        (x => { val (a, b, c) = triple(string, typ, term)(x); Abs(a, b, c) }),
  12.101 +        (x => { val (a, b) = pair(term, term)(x); App(a, b) })))
  12.102    }
  12.103  }
    13.1 --- a/src/Pure/term_xml.ML	Sun Jul 10 17:58:11 2011 +0200
    13.2 +++ b/src/Pure/term_xml.ML	Sun Jul 10 20:59:04 2011 +0200
    13.3 @@ -15,19 +15,19 @@
    13.4  
    13.5  signature TERM_XML =
    13.6  sig
    13.7 -  structure Make: TERM_XML_OPS where type 'a T = 'a XML_Data.Make.T
    13.8 -  structure Dest: TERM_XML_OPS where type 'a T = 'a XML_Data.Dest.T
    13.9 +  structure Encode: TERM_XML_OPS where type 'a T = 'a XML_Data.Encode.T
   13.10 +  structure Decode: TERM_XML_OPS where type 'a T = 'a XML_Data.Decode.T
   13.11  end;
   13.12  
   13.13  structure Term_XML: TERM_XML =
   13.14  struct
   13.15  
   13.16 -(* make *)
   13.17 +(* encode *)
   13.18  
   13.19 -structure Make =
   13.20 +structure Encode =
   13.21  struct
   13.22  
   13.23 -open XML_Data.Make;
   13.24 +open XML_Data.Encode;
   13.25  
   13.26  val indexname = pair string int;
   13.27  
   13.28 @@ -49,12 +49,12 @@
   13.29  end;
   13.30  
   13.31  
   13.32 -(* dest *)
   13.33 +(* decode *)
   13.34  
   13.35 -structure Dest =
   13.36 +structure Decode =
   13.37  struct
   13.38  
   13.39 -open XML_Data.Dest;
   13.40 +open XML_Data.Decode;
   13.41  
   13.42  val indexname = pair string int;
   13.43