(* ||M|| This file is part of HELM, an Hypertextual, Electronic ||A|| Library of Mathematics, developed at the Computer Science ||T|| Department, University of Bologna, Italy. ||I|| ||T|| HELM is free software; you can redistribute it and/or ||A|| modify it under the terms of the GNU General Public License \ / version 2 or (at your option) any later version. \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) module F = Filename module U = NUri module C = Cps module H = Hierarchy module Y = Entity (* internal functions *******************************************************) let base = "xml" let obj_ext = ".xml" let root = "ENTITY" let system = "http://helm.cs.unibo.it/lambda-delta/" ^ base ^ "/ld.dtd" let path_of_uri uri = F.concat base (Str.string_after (U.string_of_uri uri) 3) (* interface functions ******************************************************) type och = string -> unit type attr = string * string type pp = och -> int -> unit let attribute out (name, contents) = if contents <> "" then begin out " "; out name; out "=\""; out contents; out "\"" end let xml out version encoding = out "\n\n" let doctype out root system = out "\n\n" let tag tag attrs ?contents out indent = let spc = String.make indent ' ' in out spc; out "<"; out tag; List.iter (attribute out) attrs; match contents with | None -> out "/>\n" | Some cont -> out ">\n"; cont out (indent + 3); out spc; out "\n" let sort = "Sort" let lref = "LRef" let gref = "GRef" let cast = "Cast" let appl = "Appl" let proj = "Proj" let abst = "Abst" let abbr = "Abbr" let void = "Void" let position i = "position", string_of_int i let offset j = let contents = if j > 0 then string_of_int j else "" in "offset", contents let uri u = "uri", U.string_of_uri u let arity n = let contents = if n > 1 then string_of_int n else "" in "arity", contents let name a = let map f i n r s = let n = if r then n else "^" ^ n in let spc = if i then "" else " " in f (s ^ n ^ spc) in let f s = "name", s in Y.names f map a "" let mark a = let err () = "mark", "" in let f i = "mark", string_of_int i in Y.mark err f a let export_entity pp_term si g (a, u, b) = let path = path_of_uri u in let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in let och = open_out (path ^ obj_ext) in let out = output_string och in xml out "1.0" "UTF-8"; doctype out root system; let a = Y.Name (U.name_of_uri u, true) :: a in let attrs = [uri u; name a; mark a] in let contents = match b with | Y.Abst w -> tag "ABST" attrs ~contents:(pp_term w) | Y.Abbr v -> tag "ABBR" attrs ~contents:(pp_term v) | Y.Void -> assert false in let opts = if si then "si" else "" in let shp = H.string_of_graph g in let attrs = ["hierarchy", shp; "options", opts] in tag root attrs ~contents out 0; close_out och