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