]> matita.cs.unibo.it Git - helm.git/blob - helm/xmltheory/XmlTheory/iXml.ml
Files control.js graphLinks.js utils.js no longer in use.
[helm.git] / helm / xmltheory / XmlTheory / iXml.ml
1 exception NoOpenNonEmptyElements
2
3 type sectionTree =
4    Leaf of Xml.token Stream.t
5  | Node of string * (string * string) list * sectionTree list ref
6 ;;
7
8 let rec token_stream_of_section_tree_list =
9  function
10     he::tl ->
11      [< token_stream_of_section_tree_list tl; token_stream_of_section_tree he >]
12   | [] -> [<>]
13 and token_stream_of_section_tree =
14  function
15     Leaf t -> [< t >]
16   | Node (elem_name, attr_list, section_tree) ->
17      Xml.xml_nempty elem_name attr_list
18       (token_stream_of_section_tree_list !section_tree)
19 ;;
20
21 let section_stack = ref [];;
22 let xmloutput = ref (ref []);;
23 let filename = ref "";;
24
25 let reset_output fname =
26  filename := fname ;
27  xmloutput := ref [] ;
28  section_stack := []
29 ;;
30
31 let output n =
32  let xmloutput = !xmloutput in
33   xmloutput := (Leaf n) :: !xmloutput
34 ;;
35
36 let open_non_empty_element elem_name  attr_list = 
37  let newxmloutput = ref [] in
38   !xmloutput := (Node (elem_name, attr_list, newxmloutput)) :: !(!xmloutput) ;
39   section_stack := !xmloutput :: !section_stack ;
40   xmloutput := newxmloutput
41 ;;
42
43 let close_non_empty_element () =
44  match !section_stack with
45     oldxmloutput::oldsection_stack ->
46      xmloutput := oldxmloutput ;
47      section_stack := oldsection_stack
48   | _ -> raise NoOpenNonEmptyElements
49 ;;
50
51 let print_output () =
52  Xml.pp (token_stream_of_section_tree_list !(!xmloutput)) (Some !filename)
53 ;;