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_______________________________________________________________ *)
18 (* internal functions *******************************************************)
26 let system = "http://helm.cs.unibo.it/lambda-delta/" ^ base ^ "/ld.dtd"
28 let path_of_uri xdir uri =
29 let base = F.concat xdir base in
30 F.concat base (Str.string_after (U.string_of_uri uri) 3)
32 (* interface functions ******************************************************)
34 type och = string -> unit
36 type attr = string * string
38 type pp = och -> int -> unit
40 let attribute out (name, contents) =
41 if contents <> "" then begin
42 out " "; out name; out "=\""; out contents; out "\""
45 let xml out version encoding =
47 attribute out ("version", version);
48 attribute out ("encoding", encoding);
51 let doctype out root system =
52 out "<!DOCTYPE "; out root; out " SYSTEM \""; out system; out "\">\n\n"
54 let tag tag attrs ?contents out indent =
55 let spc = String.make indent ' ' in
56 out spc; out "<"; out tag; List.iter (attribute out) attrs;
60 out ">\n"; cont out (indent + 3); out spc;
61 out "</"; out tag; out ">\n"
82 "position", string_of_int i
85 let contents = if j > 0 then string_of_int j else "" in
89 "uri", U.string_of_uri u
92 let contents = if n > 1 then string_of_int n else "" in
97 let n = if r then n else "-" ^ n in
98 let spc = if i then "" else " " in
101 let f s = "name", s in
105 let err () = "mark", "" in
106 let f i = "mark", string_of_int i in
109 (* TODO: the string s must be quoted *)
111 let err () = "meta", "" in
112 let f s = "meta", s in
115 let export_entity pp_term si xdir (a, u, b) =
116 let path = path_of_uri xdir u in
117 let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
118 let och = open_out (path ^ obj_ext) in
119 let out = output_string och in
120 xml out "1.0" "UTF-8"; doctype out root system;
121 let a = E.Name (U.name_of_uri u, true) :: a in
122 let attrs = [uri u; name a; mark a; meta a] in
123 let contents = match b with
124 | E.Abst w -> tag "ABST" attrs ~contents:(pp_term w)
125 | E.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v)
126 | E.Void -> assert false
128 let opts = if si then "si" else "" in
129 let shp = H.string_of_graph () in
130 let attrs = ["hierarchy", shp; "options", opts] in
131 tag root attrs ~contents out 0;