--- 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;
--- /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;
+
--- 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;
--- 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 \
--- 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";