]> matita.cs.unibo.it Git - helm.git/blob - helm/software/helena/src/xml/xmlLibrary.ml
update in basic_2
[helm.git] / helm / software / helena / src / xml / xmlLibrary.ml
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department, University of Bologna, Italy.                     
5     ||I||                                                                
6     ||T||  HELM is free software; you can redistribute it and/or         
7     ||A||  modify it under the terms of the GNU General Public License   
8     \   /  version 2 or (at your option) any later version.              
9      \ /   This software is distributed as is, NO WARRANTY.              
10       V_______________________________________________________________ *)
11
12 module KF = Filename
13
14 module U  = NUri
15 module C  = Cps
16 module G  = Options
17 module H  = Hierarchy
18 module N  = Layer
19 module E  = Entity
20
21 IFDEF OBJECTS THEN
22
23 (* internal functions *******************************************************)
24
25 let base = "xml"
26
27 let ext = ".xml"
28
29 let obj_root = "CONSTANT"
30
31 let home = "http://lambdadelta.info/"
32
33 let system = KF.concat (KF.concat home base) "ld.dtd"
34
35 let xmlns = "xmlns", home
36
37 let path_of_uri xdir uri =
38    let base = KF.concat xdir base in 
39    KF.concat base (Str.string_after (U.string_of_uri uri) 3)
40
41 (* interface functions ******************************************************)
42
43 type och = string -> unit
44
45 type attr = string * string
46
47 type pp = och -> int -> unit
48
49 let attribute out (name, contents) =
50    if contents <> "" then begin
51       out " "; out name; out "=\""; out contents; out "\""
52    end
53
54 let xml out version encoding =
55    out "<?xml";
56       attribute out ("version", version);
57       attribute out ("encoding", encoding);
58    out "?>\n\n"
59
60 let doctype out root system =
61    out "<!DOCTYPE "; out root; out " SYSTEM \""; out system; out "\">\n\n"
62
63 let tag tag attrs ?contents out indent =
64    let spc = String.make indent ' ' in
65    out spc; out "<"; out tag; List.iter (attribute out) attrs;
66    match contents with
67       | None      -> out "/>\n"
68       | Some cont -> 
69          out ">\n"; cont out (indent + 3); out spc; 
70          out "</"; out tag; out ">\n"
71
72 let sort = "Sort"
73
74 let lref = "LRef"
75
76 let gref = "GRef"
77
78 let cast = "Cast"
79
80 let appl x = if x then "Appx" else "Appr"
81
82 let proj = "Proj"
83
84 let abst = "Abst"
85
86 let abbr = "Abbr"
87
88 let void = "Void"
89
90 let position i =
91    "position", string_of_int i
92
93 let depth i =
94    "depth", string_of_int i
95
96 let uri u =
97    "uri", U.string_of_uri u
98
99 let name a =
100    let err () = "name", "" in
101    let f n r = "name", if r then n else "-" ^ n in 
102    E.name err f a
103
104 let layer st n =
105    "layer", N.to_string st n
106
107 let main a =
108    let sort, degr = a.E.b_main in
109    ["main-position", string_of_int sort;
110     "main-degree", string_of_int degr;
111    ]
112
113 let side a =
114    let sort, degr = a.E.b_side in
115    ["side-position", string_of_int sort;
116     "side-degree", string_of_int degr;
117    ]
118
119 let apix a =
120    "level", string_of_int a.E.n_apix
121
122 let meta a =
123    let map = function
124       | E.Main     -> "Main"
125       | E.InProp   -> "InProp"
126       | E.Progress -> "Progress"
127       | E.Private  -> "Private"
128    in
129    "meta", String.concat " " (List.rev_map map a.E.r_meta)
130
131 (* TODO: the string tx must be quoted *)
132 let info a =
133    let err () = ["lang", ""; "info", ""] in
134    let f lg tx = ["lang", lg; "info", tx] in
135    E.info err f a
136
137 let export_entity pp_term (ra, na, u, b) = 
138    let path = path_of_uri !G.xdir u in
139    let _ = Sys.command (Printf.sprintf "mkdir -p %s" (KF.dirname path)) in
140    let och = open_out (path ^ ext) in
141    let out = output_string och in
142    xml out "1.0" "UTF-8"; doctype out obj_root system;
143    let ba = E.bind_attrs ~name:(U.name_of_uri u, true) () in
144    let attrs = uri u :: name ba :: apix na :: meta ra :: info ra in 
145    let contents = match b with
146       | E.Abst w -> tag "GDec" attrs ~contents:(pp_term w) 
147       | E.Abbr v -> tag "GDef" attrs ~contents:(pp_term v)
148       | E.Void   -> assert false
149    in
150    let opts = if !G.si then "si" else "" in
151    let shp = H.string_of_graph () in
152    let attrs = [xmlns; "hierarchy", shp; "options", opts] in
153    tag obj_root attrs ~contents out 0;
154    close_out och
155
156 END