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.
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_______________________________________________________________ *)
24 (* internal functions *******************************************************)
30 let obj_root = "CONSTANT"
32 let home = "http://lambdadelta.info/"
34 let system = KF.concat (KF.concat home base) "ld.dtd"
36 let xmlns = "xmlns", home
38 let path_of_uri xdir uri =
39 let base = KF.concat xdir base in
40 KF.concat base (Str.string_after (U.string_of_uri uri) 3)
42 (* interface functions ******************************************************)
44 type och = string -> unit
46 type attr = string * string
48 type pp = och -> int -> unit
50 let attribute out (name, contents) =
51 if contents <> "" then begin
52 out " "; out name; out "=\""; out contents; out "\""
55 let xml out version encoding =
57 attribute out ("version", version);
58 attribute out ("encoding", encoding);
61 let doctype out root system =
62 out "<!DOCTYPE "; out root; out " SYSTEM \""; out system; out "\">\n\n"
64 let tag tag attrs ?contents out indent =
65 let spc = String.make indent ' ' in
66 out spc; out "<"; out tag; List.iter (attribute out) attrs;
70 out ">\n"; cont out (indent + 3); out spc;
71 out "</"; out tag; out ">\n"
92 "position", string_of_int i
95 "depth", string_of_int i
98 "uri", U.string_of_uri u
101 let err () = "name", "" in
102 let f n r = "name", if r then n else "-" ^ n in
106 "restricted", KP.sprintf "%b" r
109 "layer", N.to_string st n
111 let main (sort, degr) =
112 ["main-position", string_of_int sort;
113 "main-degree", string_of_int degr;
116 let side (sort, degr) =
117 ["side-position", string_of_int sort;
118 "side-degree", string_of_int degr;
122 "level", string_of_int a.E.n_apix
127 | E.InProp -> "InProp"
128 | E.Progress -> "Progress"
129 | E.Private -> "Private"
131 "meta", String.concat " " (List.rev_map map a.E.r_meta)
133 (* TODO: the string tx must be quoted *)
135 let err () = ["lang", ""; "info", ""] in
136 let f lg tx = ["lang", lg; "info", tx] in
139 let export_entity pp_term (ra, na, u, b) =
140 let path = path_of_uri !G.xdir u in
141 let _ = Sys.command (Printf.sprintf "mkdir -p %s" (KF.dirname path)) in
142 let och = open_out (path ^ ext) in
143 let out = output_string och in
144 xml out "1.0" "UTF-8"; doctype out obj_root system;
145 let ba = E.bind_attrs ~name:(U.name_of_uri u, true) () in
146 let attrs a = uri u :: name ba :: apix na :: meta ra :: info ra @ side a.E.e_side in
147 let contents = match b with
148 | E.Abst (a, w) -> tag "GDec" (attrs a) ~contents:(pp_term w)
149 | E.Abbr (a, v) -> tag "GDef" (attrs a) ~contents:(pp_term v)
150 | E.Void -> assert false
152 let opts = if !G.si then "si" else "" in
153 let shp = H.string_of_graph () in
154 let attrs = [xmlns; "hierarchy", shp; "options", opts] in
155 tag obj_root attrs ~contents out 0;