src/Pure/General/xml_data.ML
changeset 43725 bebcfcad12d4
parent 43724 4e58485fa320
child 43726 8e2be96f2d94
equal deleted inserted replaced
43724:4e58485fa320 43725:bebcfcad12d4
     6 
     6 
     7 signature XML_DATA =
     7 signature XML_DATA =
     8 sig
     8 sig
     9   structure Make:
     9   structure Make:
    10   sig
    10   sig
    11     val properties: Properties.T -> XML.body
    11     type 'a T = 'a -> XML.body
    12     val string: string -> XML.body
    12     val properties: Properties.T T
    13     val int: int -> XML.body
    13     val string: string T
    14     val bool: bool -> XML.body
    14     val int: int T
    15     val unit: unit -> XML.body
    15     val bool: bool T
    16     val pair: ('a -> XML.body) -> ('b -> XML.body) -> 'a * 'b -> XML.body
    16     val unit: unit T
    17     val triple: ('a -> XML.body) -> ('b -> XML.body) -> ('c -> XML.body) -> 'a * 'b * 'c -> XML.body
    17     val pair: 'a T -> 'b T -> ('a * 'b) T
    18     val list: ('a -> XML.body) -> 'a list -> XML.body
    18     val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
    19     val option: ('a -> XML.body) -> 'a option -> XML.body
    19     val list: 'a T -> 'a list T
    20     val variant: ('a -> XML.body) list -> 'a -> XML.body
    20     val option: 'a T -> 'a option T
       
    21     val variant: 'a T list -> 'a T
    21   end
    22   end
    22   exception XML_ATOM of string
    23   exception XML_ATOM of string
    23   exception XML_BODY of XML.body
    24   exception XML_BODY of XML.body
    24   structure Dest:
    25   structure Dest:
    25   sig
    26   sig
    26     val properties: XML.body -> Properties.T
    27     type 'a T = XML.body -> 'a
    27     val string : XML.body -> string
    28     val properties: Properties.T T
    28     val int : XML.body -> int
    29     val string : string T
    29     val bool: XML.body -> bool
    30     val int : int T
    30     val unit: XML.body -> unit
    31     val bool: bool T
    31     val pair: (XML.body -> 'a) -> (XML.body -> 'b) -> XML.body -> 'a * 'b
    32     val unit: unit T
    32     val triple: (XML.body -> 'a) -> (XML.body -> 'b) -> (XML.body -> 'c) -> XML.body -> 'a * 'b * 'c
    33     val pair: 'a T -> 'b T -> ('a * 'b) T
    33     val list: (XML.body -> 'a) -> XML.body -> 'a list
    34     val triple: 'a T -> 'b T -> 'c T -> ('a * 'b * 'c) T
    34     val option: (XML.body -> 'a) -> XML.body -> 'a option
    35     val list: 'a T -> 'a list T
    35     val variant: (XML.body -> 'a) list -> XML.body -> 'a
    36     val option: 'a T -> 'a option T
       
    37     val variant: 'a T list -> 'a T
    36   end
    38   end
    37 end;
    39 end;
    38 
    40 
    39 structure XML_Data: XML_DATA =
    41 structure XML_Data: XML_DATA =
    40 struct
    42 struct
    41 
    43 
    42 (** make **)
    44 (** make **)
    43 
    45 
    44 structure Make =
    46 structure Make =
    45 struct
    47 struct
       
    48 
       
    49 type 'a T = 'a -> XML.body;
       
    50 
    46 
    51 
    47 (* basic values *)
    52 (* basic values *)
    48 
    53 
    49 fun int_atom i = signed_string_of_int i;
    54 fun int_atom i = signed_string_of_int i;
    50 
    55 
    94 exception XML_ATOM of string;
    99 exception XML_ATOM of string;
    95 exception XML_BODY of XML.tree list;
   100 exception XML_BODY of XML.tree list;
    96 
   101 
    97 structure Dest =
   102 structure Dest =
    98 struct
   103 struct
       
   104 
       
   105 type 'a T = XML.body -> 'a;
       
   106 
    99 
   107 
   100 (* basic values *)
   108 (* basic values *)
   101 
   109 
   102 fun int_atom s =
   110 fun int_atom s =
   103   (case Int.fromString s of
   111   (case Int.fromString s of