added output_markup (from Tools/isabelle_process.ML);
authorwenzelm
Thu Apr 03 18:42:37 2008 +0200 (2008-04-03)
changeset 26539a0754be538ab
parent 26538 d65504ffb47d
child 26540 173d548ce9d2
added output_markup (from Tools/isabelle_process.ML);
major cleanup of signature;
src/Pure/General/xml.ML
     1.1 --- a/src/Pure/General/xml.ML	Thu Apr 03 18:42:36 2008 +0200
     1.2 +++ b/src/Pure/General/xml.ML	Thu Apr 03 18:42:37 2008 +0200
     1.3 @@ -11,9 +11,9 @@
     1.4    val detect: string -> bool
     1.5    val header: string
     1.6    val text: string -> string
     1.7 -  type attributes = (string * string) list
     1.8 -  val attribute: string * string -> string
     1.9 +  type attributes = Markup.property list
    1.10    val element: string -> attributes -> string list -> string
    1.11 +  val output_markup: Markup.T -> output * output
    1.12    (*tree functions*)
    1.13    datatype tree =
    1.14        Elem of string * attributes * tree list
    1.15 @@ -21,14 +21,14 @@
    1.16      | Output of output
    1.17    type content = tree list
    1.18    type element = string * attributes * content
    1.19 -  val string_of_tree: tree -> string
    1.20 +  val string_of: tree -> string
    1.21    val plain_content: tree -> string
    1.22    val parse_string : string -> string option
    1.23 +  val parse_comment_whspc: string list -> unit * string list
    1.24    val parse_content: string list -> tree list * string list
    1.25    val parse_elem: string list -> tree * string list
    1.26    val parse_document: string list -> (string option * tree) * string list
    1.27 -  val tree_of_string: string -> tree
    1.28 -  val scan_comment_whspc: string list -> unit * string list
    1.29 +  val parse: string -> tree
    1.30  end;
    1.31  
    1.32  structure XML: XML =
    1.33 @@ -62,23 +62,25 @@
    1.34  
    1.35  (* elements *)
    1.36  
    1.37 -fun attribute (a, x) = a ^ " = \"" ^ text x ^ "\"";
    1.38 +type attributes = Markup.property list;
    1.39 +
    1.40 +fun elem name atts =
    1.41 +  space_implode " " (name :: map (fn (a, x) => a ^ " = \"" ^ text x ^ "\"") atts);
    1.42  
    1.43  fun element name atts body =
    1.44 -  let
    1.45 -    val elem = space_implode " " (name :: map attribute atts);
    1.46 -    val b = implode body;
    1.47 -  in
    1.48 -    if b = "" then enclose "<" "/>" elem
    1.49 -    else enclose "<" ">" elem ^ b ^ enclose "</" ">" name
    1.50 +  let val b = implode body in
    1.51 +    if b = "" then enclose "<" "/>" (elem name atts)
    1.52 +    else enclose "<" ">" (elem name atts) ^ b ^ enclose "</" ">" name
    1.53    end;
    1.54  
    1.55 +fun output_markup (name, atts) =
    1.56 + (enclose "<" ">" (elem name atts),
    1.57 +  enclose "</" ">" name);
    1.58 +
    1.59  
    1.60  
    1.61  (** explicit XML trees **)
    1.62  
    1.63 -type attributes = (string * string) list;
    1.64 -
    1.65  datatype tree =
    1.66      Elem of string * attributes * tree list
    1.67    | Text of string
    1.68 @@ -87,13 +89,12 @@
    1.69  type content = tree list;
    1.70  type element = string * attributes * content;
    1.71  
    1.72 -fun string_of_tree t =
    1.73 +fun string_of t =
    1.74    let
    1.75 -    fun name_atts name atts = fold Buffer.add (separate " " (name :: map attribute atts));
    1.76      fun tree (Elem (name, atts, [])) =
    1.77 -          Buffer.add "<" #> name_atts name atts #> Buffer.add "/>"
    1.78 +          Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add "/>"
    1.79        | tree (Elem (name, atts, ts)) =
    1.80 -          Buffer.add "<" #> name_atts name atts #> Buffer.add ">" #>
    1.81 +          Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add ">" #>
    1.82            fold tree ts #>
    1.83            Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
    1.84        | tree (Text s) = Buffer.add (text s)
    1.85 @@ -136,7 +137,7 @@
    1.86    Scan.repeat (Scan.unless (Scan.this_string "-->") (Scan.one Symbol.is_regular)) --
    1.87    Scan.this_string "-->";
    1.88  
    1.89 -val scan_comment_whspc =
    1.90 +val parse_comment_whspc =
    1.91    (scan_whspc >> K()) --| (Scan.repeat (parse_comment |-- (scan_whspc >> K())));
    1.92  
    1.93  val parse_pi = Scan.this_string "<?" |--
    1.94 @@ -169,7 +170,7 @@
    1.95        (Scan.one Symbol.is_regular)) >> implode) --| $$ ">" --| scan_whspc) --
    1.96    parse_elem;
    1.97  
    1.98 -fun tree_of_string s =
    1.99 +fun parse s =
   1.100    (case Scan.finite Symbol.stopper (Scan.error (!! (err "Malformed element")
   1.101        (scan_whspc |-- parse_elem --| scan_whspc))) (Symbol.explode s) of
   1.102      (x, []) => x