type XML.body as basic data representation language;
authorwenzelm
Tue Aug 10 22:26:23 2010 +0200 (2010-08-10)
changeset 38266492d377ecfe2
parent 38265 cc9fde54311f
child 38267 e50c283dd125
type XML.body as basic data representation language;
tuned;
src/Pure/General/xml.ML
src/Pure/General/xml_data.ML
src/Pure/General/yxml.ML
src/Pure/IsaMakefile
src/Pure/ROOT.ML
     1.1 --- a/src/Pure/General/xml.ML	Tue Aug 10 20:13:52 2010 +0200
     1.2 +++ b/src/Pure/General/xml.ML	Tue Aug 10 22:26:23 2010 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4    datatype tree =
     1.5        Elem of Markup.T * tree list
     1.6      | Text of string
     1.7 +  type body = tree list
     1.8    val add_content: tree -> Buffer.T -> Buffer.T
     1.9    val header: string
    1.10    val text: string -> string
    1.11 @@ -35,6 +36,8 @@
    1.12      Elem of Markup.T * tree list
    1.13    | Text of string;
    1.14  
    1.15 +type body = tree list;
    1.16 +
    1.17  fun add_content (Elem (_, ts)) = fold add_content ts
    1.18    | add_content (Text s) = Buffer.add s;
    1.19  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/General/xml_data.ML	Tue Aug 10 22:26:23 2010 +0200
     2.3 @@ -0,0 +1,125 @@
     2.4 +(*  Title:      Pure/General/xml_data.ML
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +XML as basic data representation language.
     2.8 +*)
     2.9 +
    2.10 +signature XML_DATA =
    2.11 +sig
    2.12 +  exception XML_ATOM of string
    2.13 +  exception XML_BODY of XML.body
    2.14 +  val make_properties: Properties.T -> XML.body
    2.15 +  val dest_properties: XML.body -> Properties.T
    2.16 +  val make_string: string -> XML.body
    2.17 +  val dest_string : XML.body -> string
    2.18 +  val make_int: int -> XML.body
    2.19 +  val dest_int : XML.body -> int
    2.20 +  val make_bool: bool -> XML.body
    2.21 +  val dest_bool: XML.body -> bool
    2.22 +  val make_unit: unit -> XML.body
    2.23 +  val dest_unit: XML.body -> unit
    2.24 +  val make_pair: ('a -> XML.body) -> ('b -> XML.body) -> 'a * 'b -> XML.body
    2.25 +  val dest_pair: (XML.body -> 'a) -> (XML.body -> 'b) -> XML.body -> 'a * 'b
    2.26 +  val make_triple:
    2.27 +    ('a -> XML.body) -> ('b -> XML.body) -> ('c -> XML.body) -> 'a * 'b * 'c -> XML.body
    2.28 +  val dest_triple:
    2.29 +    (XML.body -> 'a) -> (XML.body -> 'b) -> (XML.body -> 'c) -> XML.body -> 'a * 'b * 'c
    2.30 +  val make_list: ('a -> XML.body) -> 'a list -> XML.body
    2.31 +  val dest_list: (XML.body -> 'a) -> XML.body -> 'a list
    2.32 +  val make_option: ('a -> XML.body) -> 'a option -> XML.body
    2.33 +  val dest_option: (XML.body -> 'a) -> XML.body -> 'a option
    2.34 +end;
    2.35 +
    2.36 +structure XML_Data: XML_DATA =
    2.37 +struct
    2.38 +
    2.39 +(* basic values *)
    2.40 +
    2.41 +exception XML_ATOM of string;
    2.42 +
    2.43 +
    2.44 +fun make_int_atom i = signed_string_of_int i;
    2.45 +
    2.46 +fun dest_int_atom s =
    2.47 +  (case Int.fromString s of
    2.48 +    SOME i => i
    2.49 +  | NONE => raise XML_ATOM s);
    2.50 +
    2.51 +
    2.52 +fun make_bool_atom false = "0"
    2.53 +  | make_bool_atom true = "1";
    2.54 +
    2.55 +fun dest_bool_atom "0" = false
    2.56 +  | dest_bool_atom "1" = true
    2.57 +  | dest_bool_atom s = raise XML_ATOM s;
    2.58 +
    2.59 +fun make_unit_atom () = "";
    2.60 +
    2.61 +fun dest_unit_atom "" = ()
    2.62 +  | dest_unit_atom s = raise XML_ATOM s;
    2.63 +
    2.64 +
    2.65 +(* structural nodes *)
    2.66 +
    2.67 +exception XML_BODY of XML.tree list;
    2.68 +
    2.69 +fun make_node ts = XML.Elem ((":", []), ts);
    2.70 +
    2.71 +fun dest_node (XML.Elem ((":", []), ts)) = ts
    2.72 +  | dest_node t = raise XML_BODY [t];
    2.73 +
    2.74 +
    2.75 +(* representation of standard types *)
    2.76 +
    2.77 +fun make_properties props = [XML.Elem ((":", props), [])];
    2.78 +
    2.79 +fun dest_properties [XML.Elem ((":", props), [])] = props
    2.80 +  | dest_properties ts = raise XML_BODY ts;
    2.81 +
    2.82 +
    2.83 +fun make_string s = [XML.Text s];
    2.84 +
    2.85 +fun dest_string [XML.Text s] = s
    2.86 +  | dest_string ts = raise XML_BODY ts;
    2.87 +
    2.88 +
    2.89 +val make_int = make_string o make_int_atom;
    2.90 +val dest_int = dest_int_atom o dest_string;
    2.91 +
    2.92 +val make_bool = make_string o make_bool_atom;
    2.93 +val dest_bool = dest_bool_atom o dest_string;
    2.94 +
    2.95 +val make_unit = make_string o make_unit_atom;
    2.96 +val dest_unit = dest_unit_atom o dest_string;
    2.97 +
    2.98 +
    2.99 +fun make_pair make1 make2 (x, y) = [make_node (make1 x), make_node (make2 y)];
   2.100 +
   2.101 +fun dest_pair dest1 dest2 [t1, t2] = (dest1 (dest_node t1), dest2 (dest_node t2))
   2.102 +  | dest_pair _ _ ts = raise XML_BODY ts;
   2.103 +
   2.104 +
   2.105 +fun make_triple make1 make2 make3 (x, y, z) =
   2.106 +  [make_node (make1 x), make_node (make2 y), make_node (make3 z)];
   2.107 +
   2.108 +fun dest_triple dest1 dest2 dest3 [t1, t2, t3] =
   2.109 +      (dest1 (dest_node t1), dest2 (dest_node t2), dest3 (dest_node t3))
   2.110 +  | dest_triple _ _ _ ts = raise XML_BODY ts;
   2.111 +
   2.112 +
   2.113 +fun make_list make xs = map (make_node o make) xs;
   2.114 +
   2.115 +fun dest_list dest ts = map (dest o dest_node) ts;
   2.116 +
   2.117 +
   2.118 +fun make_option make NONE = make_list make []
   2.119 +  | make_option make (SOME x) = make_list make [x];
   2.120 +
   2.121 +fun dest_option dest ts =
   2.122 +  (case dest_list dest ts of
   2.123 +    [] => NONE
   2.124 +  | [x] => SOME x
   2.125 +  | _ => raise XML_BODY ts);
   2.126 +
   2.127 +end;
   2.128 +
     3.1 --- a/src/Pure/General/yxml.ML	Tue Aug 10 20:13:52 2010 +0200
     3.2 +++ b/src/Pure/General/yxml.ML	Tue Aug 10 22:26:23 2010 +0200
     3.3 @@ -19,7 +19,7 @@
     3.4    val output_markup: Markup.T -> string * string
     3.5    val element: string -> XML.attributes -> string list -> string
     3.6    val string_of: XML.tree -> string
     3.7 -  val parse_body: string -> XML.tree list
     3.8 +  val parse_body: string -> XML.body
     3.9    val parse: string -> XML.tree
    3.10  end;
    3.11  
     4.1 --- a/src/Pure/IsaMakefile	Tue Aug 10 20:13:52 2010 +0200
     4.2 +++ b/src/Pure/IsaMakefile	Tue Aug 10 22:26:23 2010 +0200
     4.3 @@ -59,31 +59,31 @@
     4.4    General/sha1_polyml.ML General/secure.ML General/seq.ML		\
     4.5    General/source.ML General/stack.ML General/symbol.ML			\
     4.6    General/symbol_pos.ML General/table.ML General/url.ML General/xml.ML	\
     4.7 -  General/yxml.ML Isar/args.ML Isar/attrib.ML Isar/auto_bind.ML		\
     4.8 -  Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML	\
     4.9 -  Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML		\
    4.10 -  Isar/expression.ML Isar/isar_cmd.ML Isar/isar_document.ML		\
    4.11 -  Isar/isar_syn.ML Isar/keyword.ML Isar/local_defs.ML			\
    4.12 -  Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML		\
    4.13 -  Isar/method.ML Isar/object_logic.ML Isar/obtain.ML			\
    4.14 -  Isar/outer_syntax.ML Isar/overloading.ML Isar/parse.ML		\
    4.15 -  Isar/parse_spec.ML Isar/parse_value.ML Isar/proof.ML			\
    4.16 -  Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML	\
    4.17 -  Isar/rule_cases.ML Isar/rule_insts.ML Isar/runtime.ML			\
    4.18 -  Isar/skip_proof.ML Isar/spec_rules.ML Isar/specification.ML		\
    4.19 -  Isar/theory_target.ML Isar/token.ML Isar/toplevel.ML			\
    4.20 -  Isar/typedecl.ML ML/ml_antiquote.ML ML/ml_compiler.ML			\
    4.21 -  ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML ML/ml_env.ML		\
    4.22 -  ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML		\
    4.23 -  ML-Systems/install_pp_polyml.ML ML-Systems/install_pp_polyml-5.3.ML	\
    4.24 -  ML-Systems/use_context.ML Proof/extraction.ML PIDE/document.ML	\
    4.25 -  Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML			\
    4.26 -  Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/pgip.ML	\
    4.27 -  ProofGeneral/pgip_input.ML ProofGeneral/pgip_isabelle.ML		\
    4.28 -  ProofGeneral/pgip_markup.ML ProofGeneral/pgip_output.ML		\
    4.29 -  ProofGeneral/pgip_parser.ML ProofGeneral/pgip_tests.ML		\
    4.30 -  ProofGeneral/pgip_types.ML ProofGeneral/preferences.ML		\
    4.31 -  ProofGeneral/proof_general_emacs.ML					\
    4.32 +  General/xml_data.ML General/yxml.ML Isar/args.ML Isar/attrib.ML	\
    4.33 +  Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML			\
    4.34 +  Isar/class_target.ML Isar/code.ML Isar/constdefs.ML			\
    4.35 +  Isar/context_rules.ML Isar/element.ML Isar/expression.ML		\
    4.36 +  Isar/isar_cmd.ML Isar/isar_document.ML Isar/isar_syn.ML		\
    4.37 +  Isar/keyword.ML Isar/local_defs.ML Isar/local_syntax.ML		\
    4.38 +  Isar/local_theory.ML Isar/locale.ML Isar/method.ML			\
    4.39 +  Isar/object_logic.ML Isar/obtain.ML Isar/outer_syntax.ML		\
    4.40 +  Isar/overloading.ML Isar/parse.ML Isar/parse_spec.ML			\
    4.41 +  Isar/parse_value.ML Isar/proof.ML Isar/proof_context.ML		\
    4.42 +  Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML		\
    4.43 +  Isar/rule_insts.ML Isar/runtime.ML Isar/skip_proof.ML			\
    4.44 +  Isar/spec_rules.ML Isar/specification.ML Isar/theory_target.ML	\
    4.45 +  Isar/token.ML Isar/toplevel.ML Isar/typedecl.ML ML/ml_antiquote.ML	\
    4.46 +  ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML ML/ml_context.ML	\
    4.47 +  ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML		\
    4.48 +  ML/ml_thms.ML ML-Systems/install_pp_polyml.ML				\
    4.49 +  ML-Systems/install_pp_polyml-5.3.ML ML-Systems/use_context.ML		\
    4.50 +  Proof/extraction.ML PIDE/document.ML Proof/proof_rewrite_rules.ML	\
    4.51 +  Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML	\
    4.52 +  ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML			\
    4.53 +  ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML		\
    4.54 +  ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML		\
    4.55 +  ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML			\
    4.56 +  ProofGeneral/preferences.ML ProofGeneral/proof_general_emacs.ML	\
    4.57    ProofGeneral/proof_general_pgip.ML Pure.thy ROOT.ML Syntax/ast.ML	\
    4.58    Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML			\
    4.59    Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML		\
     5.1 --- a/src/Pure/ROOT.ML	Tue Aug 10 20:13:52 2010 +0200
     5.2 +++ b/src/Pure/ROOT.ML	Tue Aug 10 22:26:23 2010 +0200
     5.3 @@ -50,6 +50,7 @@
     5.4  use "General/buffer.ML";
     5.5  use "General/file.ML";
     5.6  use "General/xml.ML";
     5.7 +use "General/xml_data.ML";
     5.8  use "General/yxml.ML";
     5.9  
    5.10  use "General/sha1.ML";