# HG changeset patch
# User wenzelm
# Date 1281471983 -7200
# Node ID 492d377ecfe28979531affff752df93b70bfb248
# Parent  cc9fde54311f85f657c784a67715d02e87e08bf0
type XML.body as basic data representation language;
tuned;

diff -r cc9fde54311f -r 492d377ecfe2 src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Tue Aug 10 20:13:52 2010 +0200
+++ b/src/Pure/General/xml.ML	Tue Aug 10 22:26:23 2010 +0200
@@ -10,6 +10,7 @@
   datatype tree =
       Elem of Markup.T * tree list
     | Text of string
+  type body = tree list
   val add_content: tree -> Buffer.T -> Buffer.T
   val header: string
   val text: string -> string
@@ -35,6 +36,8 @@
     Elem of Markup.T * tree list
   | Text of string;
 
+type body = tree list;
+
 fun add_content (Elem (_, ts)) = fold add_content ts
   | add_content (Text s) = Buffer.add s;
 
diff -r cc9fde54311f -r 492d377ecfe2 src/Pure/General/xml_data.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/xml_data.ML	Tue Aug 10 22:26:23 2010 +0200
@@ -0,0 +1,125 @@
+(*  Title:      Pure/General/xml_data.ML
+    Author:     Makarius
+
+XML as basic data representation language.
+*)
+
+signature XML_DATA =
+sig
+  exception XML_ATOM of string
+  exception XML_BODY of XML.body
+  val make_properties: Properties.T -> XML.body
+  val dest_properties: XML.body -> Properties.T
+  val make_string: string -> XML.body
+  val dest_string : XML.body -> string
+  val make_int: int -> XML.body
+  val dest_int : XML.body -> int
+  val make_bool: bool -> XML.body
+  val dest_bool: XML.body -> bool
+  val make_unit: unit -> XML.body
+  val dest_unit: XML.body -> unit
+  val make_pair: ('a -> XML.body) -> ('b -> XML.body) -> 'a * 'b -> XML.body
+  val dest_pair: (XML.body -> 'a) -> (XML.body -> 'b) -> XML.body -> 'a * 'b
+  val make_triple:
+    ('a -> XML.body) -> ('b -> XML.body) -> ('c -> XML.body) -> 'a * 'b * 'c -> XML.body
+  val dest_triple:
+    (XML.body -> 'a) -> (XML.body -> 'b) -> (XML.body -> 'c) -> XML.body -> 'a * 'b * 'c
+  val make_list: ('a -> XML.body) -> 'a list -> XML.body
+  val dest_list: (XML.body -> 'a) -> XML.body -> 'a list
+  val make_option: ('a -> XML.body) -> 'a option -> XML.body
+  val dest_option: (XML.body -> 'a) -> XML.body -> 'a option
+end;
+
+structure XML_Data: XML_DATA =
+struct
+
+(* basic values *)
+
+exception XML_ATOM of string;
+
+
+fun make_int_atom i = signed_string_of_int i;
+
+fun dest_int_atom s =
+  (case Int.fromString s of
+    SOME i => i
+  | NONE => raise XML_ATOM s);
+
+
+fun make_bool_atom false = "0"
+  | make_bool_atom true = "1";
+
+fun dest_bool_atom "0" = false
+  | dest_bool_atom "1" = true
+  | dest_bool_atom s = raise XML_ATOM s;
+
+fun make_unit_atom () = "";
+
+fun dest_unit_atom "" = ()
+  | dest_unit_atom s = raise XML_ATOM s;
+
+
+(* structural nodes *)
+
+exception XML_BODY of XML.tree list;
+
+fun make_node ts = XML.Elem ((":", []), ts);
+
+fun dest_node (XML.Elem ((":", []), ts)) = ts
+  | dest_node t = raise XML_BODY [t];
+
+
+(* representation of standard types *)
+
+fun make_properties props = [XML.Elem ((":", props), [])];
+
+fun dest_properties [XML.Elem ((":", props), [])] = props
+  | dest_properties ts = raise XML_BODY ts;
+
+
+fun make_string s = [XML.Text s];
+
+fun dest_string [XML.Text s] = s
+  | dest_string ts = raise XML_BODY ts;
+
+
+val make_int = make_string o make_int_atom;
+val dest_int = dest_int_atom o dest_string;
+
+val make_bool = make_string o make_bool_atom;
+val dest_bool = dest_bool_atom o dest_string;
+
+val make_unit = make_string o make_unit_atom;
+val dest_unit = dest_unit_atom o dest_string;
+
+
+fun make_pair make1 make2 (x, y) = [make_node (make1 x), make_node (make2 y)];
+
+fun dest_pair dest1 dest2 [t1, t2] = (dest1 (dest_node t1), dest2 (dest_node t2))
+  | dest_pair _ _ ts = raise XML_BODY ts;
+
+
+fun make_triple make1 make2 make3 (x, y, z) =
+  [make_node (make1 x), make_node (make2 y), make_node (make3 z)];
+
+fun dest_triple dest1 dest2 dest3 [t1, t2, t3] =
+      (dest1 (dest_node t1), dest2 (dest_node t2), dest3 (dest_node t3))
+  | dest_triple _ _ _ ts = raise XML_BODY ts;
+
+
+fun make_list make xs = map (make_node o make) xs;
+
+fun dest_list dest ts = map (dest o dest_node) ts;
+
+
+fun make_option make NONE = make_list make []
+  | make_option make (SOME x) = make_list make [x];
+
+fun dest_option dest ts =
+  (case dest_list dest ts of
+    [] => NONE
+  | [x] => SOME x
+  | _ => raise XML_BODY ts);
+
+end;
+
diff -r cc9fde54311f -r 492d377ecfe2 src/Pure/General/yxml.ML
--- a/src/Pure/General/yxml.ML	Tue Aug 10 20:13:52 2010 +0200
+++ b/src/Pure/General/yxml.ML	Tue Aug 10 22:26:23 2010 +0200
@@ -19,7 +19,7 @@
   val output_markup: Markup.T -> string * string
   val element: string -> XML.attributes -> string list -> string
   val string_of: XML.tree -> string
-  val parse_body: string -> XML.tree list
+  val parse_body: string -> XML.body
   val parse: string -> XML.tree
 end;
 
diff -r cc9fde54311f -r 492d377ecfe2 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Tue Aug 10 20:13:52 2010 +0200
+++ b/src/Pure/IsaMakefile	Tue Aug 10 22:26:23 2010 +0200
@@ -59,31 +59,31 @@
   General/sha1_polyml.ML General/secure.ML General/seq.ML		\
   General/source.ML General/stack.ML General/symbol.ML			\
   General/symbol_pos.ML General/table.ML General/url.ML General/xml.ML	\
-  General/yxml.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML		\
-  Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML	\
-  Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML		\
-  Isar/expression.ML Isar/isar_cmd.ML Isar/isar_document.ML		\
-  Isar/isar_syn.ML Isar/keyword.ML Isar/local_defs.ML			\
-  Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML		\
-  Isar/method.ML Isar/object_logic.ML Isar/obtain.ML			\
-  Isar/outer_syntax.ML Isar/overloading.ML Isar/parse.ML		\
-  Isar/parse_spec.ML Isar/parse_value.ML Isar/proof.ML			\
-  Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML	\
-  Isar/rule_cases.ML Isar/rule_insts.ML Isar/runtime.ML			\
-  Isar/skip_proof.ML Isar/spec_rules.ML Isar/specification.ML		\
-  Isar/theory_target.ML Isar/token.ML Isar/toplevel.ML			\
-  Isar/typedecl.ML ML/ml_antiquote.ML ML/ml_compiler.ML			\
-  ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML ML/ml_env.ML		\
-  ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML		\
-  ML-Systems/install_pp_polyml.ML ML-Systems/install_pp_polyml-5.3.ML	\
-  ML-Systems/use_context.ML Proof/extraction.ML PIDE/document.ML	\
-  Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML			\
-  Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/pgip.ML	\
-  ProofGeneral/pgip_input.ML ProofGeneral/pgip_isabelle.ML		\
-  ProofGeneral/pgip_markup.ML ProofGeneral/pgip_output.ML		\
-  ProofGeneral/pgip_parser.ML ProofGeneral/pgip_tests.ML		\
-  ProofGeneral/pgip_types.ML ProofGeneral/preferences.ML		\
-  ProofGeneral/proof_general_emacs.ML					\
+  General/xml_data.ML General/yxml.ML Isar/args.ML Isar/attrib.ML	\
+  Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML			\
+  Isar/class_target.ML Isar/code.ML Isar/constdefs.ML			\
+  Isar/context_rules.ML Isar/element.ML Isar/expression.ML		\
+  Isar/isar_cmd.ML Isar/isar_document.ML Isar/isar_syn.ML		\
+  Isar/keyword.ML Isar/local_defs.ML Isar/local_syntax.ML		\
+  Isar/local_theory.ML Isar/locale.ML Isar/method.ML			\
+  Isar/object_logic.ML Isar/obtain.ML Isar/outer_syntax.ML		\
+  Isar/overloading.ML Isar/parse.ML Isar/parse_spec.ML			\
+  Isar/parse_value.ML Isar/proof.ML Isar/proof_context.ML		\
+  Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML		\
+  Isar/rule_insts.ML Isar/runtime.ML Isar/skip_proof.ML			\
+  Isar/spec_rules.ML Isar/specification.ML Isar/theory_target.ML	\
+  Isar/token.ML Isar/toplevel.ML Isar/typedecl.ML ML/ml_antiquote.ML	\
+  ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML	\
+  ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML		\
+  ML/ml_thms.ML ML-Systems/install_pp_polyml.ML				\
+  ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.ML		\
+  Proof/extraction.ML PIDE/document.ML Proof/proof_rewrite_rules.ML	\
+  Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML	\
+  ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML			\
+  ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML		\
+  ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML		\
+  ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML			\
+  ProofGeneral/preferences.ML ProofGeneral/proof_general_emacs.ML	\
   ProofGeneral/proof_general_pgip.ML Pure.thy ROOT.ML Syntax/ast.ML	\
   Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML			\
   Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML		\
diff -r cc9fde54311f -r 492d377ecfe2 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Tue Aug 10 20:13:52 2010 +0200
+++ b/src/Pure/ROOT.ML	Tue Aug 10 22:26:23 2010 +0200
@@ -50,6 +50,7 @@
 use "General/buffer.ML";
 use "General/file.ML";
 use "General/xml.ML";
+use "General/xml_data.ML";
 use "General/yxml.ML";
 
 use "General/sha1.ML";