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