matita/matita/contribs/lambdadelta/bin/roles/webEngine.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 KP = Printf
  13
  14 module EG = RolesGlobal
  15 module EE = RolesEngine
  16
  17 let open_out_html author description title css icon =
  18 (*
  19   YW.open_out "application/xhtml+xml" 0;
  20 *)
  21   KP.printf "<?xml version=\"1.0\" encoding=\"UTF-8\"?>\n";
  22   KP.printf "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.1//EN\" \"http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd\">\n";
  23   KP.printf "<html xmlns=\"http://www.w3.org/1999/xhtml\" dir=\"ltr\" lang=\"en-us\">\n";
  24   KP.printf "<head>\n";
  25   KP.printf "  <meta http-equiv=\"Pragma\" content=\"no-cache\"/>\n";
  26   KP.printf "  <meta http-equiv=\"Expires\" content=\"-1\"/>\n";
  27   KP.printf "  <meta http-equiv=\"CACHE-CONTROL\" content=\"NO-CACHE\"/>\n";
  28   KP.printf "  <meta http-equiv=\"Content-Type\" content=\"text/html; charset=UTF-8\"/>\n";
  29   KP.printf "  <meta http-equiv=\"Content-Language\" content=\"en-us\"/>\n";
  30   KP.printf "  <meta http-equiv=\"Content-Style-Type\" content=\"text/css\"/>\n";
  31   KP.printf "  <meta name=\"author\" content=\"%s\"/>\n" author;
  32   KP.printf "  <meta name=\"description\" content=\"%s\"/>\n" description;
  33   KP.printf "  <title>%s</title>" title;
  34   KP.printf "  <link rel=\"stylesheet\" type=\"text/css\" href=\"%s\"/>\n" css;
  35   KP.printf "  <link rel=\"shortcut icon\" href=\"%s\"/>\n" icon;
  36   KP.printf "</head>\n";
  37   KP.printf "<body lang=\"en-US\">\n"
  38
  39 let close_out_html () =
  40   KP.printf "</body>\n";
  41   KP.printf "</html>\n"
  42 (*
  43   YW.close_out ()
  44 *)
  45 let open_out () =
  46   let author = "λδ development binary: roles manager" in
  47   let description = "λδ development binary: roles manager" in
  48   let title = "Roles Manager" in
  49   let css = Filename.concat !EG.base_url "css/roles.css" in
  50   let icon = Filename.concat !EG.base_url "images/crux_32.ico" in
  51   open_out_html author description title css icon
  52
  53 let close_out () =
  54   close_out_html ()
  55
  56 let status_out () =
  57   let before_atoms a p count =
  58     let c, str =
  59       if a then "object", "objects"
  60       else "name", "names"
  61     in
  62     KP.printf "<div class=\"atoms-head %s\">\n" c;
  63     KP.printf "<a href=\"\">%s:</a>\n" str;
  64     KP.printf "<span class=\"count\">%s</span>\n" count;
  65     KP.printf "</div>\n";
  66     KP.printf "<div class=\"atoms\"><table><tr>\n"
  67   in
  68   let each_atom a p b str =
  69     let c = if a then "object" else "name" in
  70     let s = if b then " selected" else "" in
  71     KP.printf "<td class=\"atom %s%s\"><a href=\"\">%s</a></td>\n" c s str
  72   in
  73   let after_atoms () =
  74     KP.printf "</tr></table></div>\n"
  75   in
  76   EE.visit_status
  77     (before_atoms true) (each_atom true) after_atoms
  78     (before_atoms false) (each_atom false) after_atoms
  79
  80 let init () =
  81   open_out ();
  82   status_out ();
  83   close_out ()