(*
||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 = Format
module N = 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 =
N.concat base (Str.string_after (U.string_of_uri uri) 3)
let pp_head frm =
F.fprintf frm "@,@," "1.0" "UTF-8"
let pp_doctype frm =
F.fprintf frm "@,@," system
let open_entity si g frm =
let opts = if si then "si" else "" in
let f shp =
F.fprintf frm "" shp opts
in
H.string_of_graph f g
let close_entity frm =
F.fprintf frm ""
let name frm a =
let f s = function
| true -> F.fprintf frm " name=%S" s
| false -> F.fprintf frm " name=%S" ("^" ^ s)
in
Y.name C.start f a
let pp_entity pp_term frm = function
| a, u, Y.Abst w ->
let str = U.string_of_uri u in
let a = Y.Name (U.name_of_uri u, true) :: a in
F.fprintf frm "%a" str name a pp_term w
| a, u, Y.Abbr v ->
let str = U.string_of_uri u in
let a = Y.Name (U.name_of_uri u, true) :: a in
F.fprintf frm "%a" str name a pp_term v
let pp_boxed pp_term frm entity =
F.fprintf frm "@,@[ %a@]@," (pp_entity pp_term) entity
(* interface functions ******************************************************)
let old_export_entity pp_term si g entity =
let _, uri, _ = entity in
let path = path_of_uri uri in
let _ = Sys.command (Printf.sprintf "mkdir -p %s" (N.dirname path)) in
let och = open_out (path ^ obj_ext) in
let frm = F.formatter_of_out_channel och in
F.pp_set_margin frm max_int;
F.fprintf frm "@[%t%t%t%a%t@]@."
pp_head pp_doctype
(open_entity si g) (pp_boxed pp_term) entity close_entity;
close_out och
let old_name = name
(****************************************************************************)
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 ""; out tag; 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" (N.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)
in
let opts = if si then "si" else "" in
let shp = H.string_of_graph C.start g in
let attrs = ["hierarchy", shp; "options", opts] in
tag root attrs ~contents out 0;
close_out och