helm/software/lambda-delta/common/library.ml

   1 (*
   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.
   5     ||I||
   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_______________________________________________________________ *)
  11
  12 module F = Filename
  13 module U = NUri
  14 module H = Hierarchy
  15
  16 (* internal functions *******************************************************)
  17
  18 let obj_ext = ".ld.xml"
  19
  20 let system = "http://helm.cs.unibo.it/lambda-delta/xml/ld.dtd"
  21
  22 let path_of_uri base uri =
  23    F.concat base (Str.string_after (U.string_of_uri uri) 3)
  24
  25 let pp_head frm =
  26    Format.fprintf frm "<?xml version=%S encoding=%S?>@,@," "1.0" "UTF-8"
  27
  28 let pp_doctype frm =
  29   Format.fprintf frm "<!DOCTYPE KERNEL SYSTEM %S>@,@," system
  30
  31 let open_kernel si g frm =
  32    let opts = if si then "si" else "" in
  33    let f shp =
  34       Format.fprintf frm "<KERNEL hierarchy=%S options=%S>" shp opts
  35    in
  36    H.string_of_graph f g
  37
  38 let close_kernel frm =
  39    Format.fprintf frm "</KERNEL>"
  40
  41 (* interface functions ******************************************************)
  42
  43 let export_item export_obj si g base = function
  44    | Some obj ->
  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;
  53       close_out och
  54    | None     -> ()