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_______________________________________________________________ *)
16 (* internal functions *******************************************************)
18 let obj_ext = ".ld.xml"
20 let system = "http://helm.cs.unibo.it/lambda-delta/xml/ld.dtd"
22 let path_of_uri base uri =
23 F.concat base (Str.string_after (U.string_of_uri uri) 3)
26 Format.fprintf frm "<?xml version=%S encoding=%S?>@,@," "1.0" "UTF-8"
29 Format.fprintf frm "<!DOCTYPE KERNEL SYSTEM %S>@,@," system
31 let open_kernel si g frm =
32 let opts = if si then "si" else "" in
34 Format.fprintf frm "<KERNEL hierarchy=%S options=%S>" shp opts
38 let close_kernel frm =
39 Format.fprintf frm "</KERNEL>"
41 (* interface functions ******************************************************)
43 let export_item export_obj si g base = function
45 let _, uri, bind = obj in
46 let path = path_of_uri base uri in
47 let _ = Sys.command (Printf.sprintf "mkdir -p %s" (F.dirname path)) in
48 let och = open_out (path ^ obj_ext) in
49 let frm = Format.formatter_of_out_channel och in
50 Format.pp_set_margin frm max_int;
51 Format.fprintf frm "@[<v>%t%t%t%a%t@]@."
52 pp_head pp_doctype (open_kernel si g) export_obj obj close_kernel;