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_______________________________________________________________ *)
21 (* internal functions *******************************************************)
27 let obj_root = "ENTITY"
29 let ccs_name = "ccs.ldc"
33 let home = "http://lambdadelta.info/"
35 let system = F.concat (F.concat home base) "ld.dtd"
37 let xmlns = "xmlns", home
39 let path_of_uri xdir uri =
40 let base = F.concat xdir base in
41 F.concat base (Str.string_after (U.string_of_uri uri) 3)
43 (* interface functions ******************************************************)
45 type och = string -> unit
47 type attr = string * string
49 type pp = och -> int -> unit
51 let attribute out (name, contents) =
52 if contents <> "" then begin
53 out " "; out name; out "=\""; out contents; out "\""
56 let xml out version encoding =
58 attribute out ("version", version);
59 attribute out ("encoding", encoding);
62 let doctype out root system =
63 out "<!DOCTYPE "; out root; out " SYSTEM \""; out system; out "\">\n\n"
65 let tag tag attrs ?contents out indent =
66 let spc = String.make indent ' ' in
67 out spc; out "<"; out tag; List.iter (attribute out) attrs;
71 out ">\n"; cont out (indent + 3); out spc;
72 out "</"; out tag; out ">\n"
93 "position", string_of_int i
96 let contents = if j > 0 then string_of_int j else "" in
100 "uri", U.string_of_uri u
104 | None -> List.length l
107 let contents = if n > 1 then string_of_int n else "" in
112 let n = if r then n else "-" ^ n in
113 let spc = if i then "" else " " in
116 let f s = "name", s in
120 let err () = "mark", "" in
121 let f i = "mark", string_of_int i in
125 "level", N.to_string n
130 | E.InProp -> "InProp"
131 | E.Progress -> "Progress"
132 | E.Private -> "Private"
134 let err () = "meta", "" in
135 let f ms = "meta", String.concat " " (List.rev_map map ms) in
138 (* TODO: the string tx must be quoted *)
140 let err () = ["lang", ""; "info", ""] in
141 let f lg tx = ["lang", lg; "info", tx] in
144 let export_entity pp_term (a, u, b) =
145 let path = path_of_uri !G.xdir u in
146 let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
147 let och = open_out (path ^ ext) in
148 let out = output_string och in
149 xml out "1.0" "UTF-8"; doctype out obj_root system;
150 let a = E.Name (U.name_of_uri u, true) :: a in
151 let attrs = uri u :: name a :: mark a :: meta a :: info a in
152 let contents = match b with
153 | E.Abst (n, w) -> tag "ABST" (level n :: attrs) ~contents:(pp_term w)
154 | E.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v)
155 | E.Void -> assert false
157 let opts = if !G.si then "si" else "" in
158 let shp = H.string_of_graph () in
159 let attrs = [xmlns; "hierarchy", shp; "options", opts] in
160 tag obj_root attrs ~contents out 0;
163 let prec_map (i, _) = string_of_int i
165 let next_map (_, i) = string_of_int i
169 | l -> "mark", String.concat " " (List.rev_map string_of_int l)
173 | l -> "prec", String.concat " " (List.rev_map prec_map l)
177 | l -> "next", String.concat " " (List.rev_map next_map l)
180 let path = path_of_uri !G.xdir s.Q.buri in
181 let _ = Sys.command (Printf.sprintf "mkdir -p %s" path) in
182 let name = F.concat path (ccs_name ^ ext) in
183 let och = open_out name in
184 let out = output_string och in
185 xml out "1.0" "UTF-8"; doctype out ccs_root system;
186 let attrs = [xmlns; uri s.Q.buri] in
187 let contents out tab =
188 tag "ToPositive" [arity s.Q.tp; marks s.Q.tp] out tab;
189 tag "ToOne" [arity s.Q.t1; marks s.Q.t1] out tab;
190 tag "ToNext" [arity s.Q.tn; precs s.Q.tn; nexts s.Q.tn] out tab
192 tag ccs_root attrs ~contents out 0;