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 EE = RolesEngine
  15 module EG = RolesGlobal
  16 module ET = RolesTypes
  17 module EU = RolesUtils
  18 module WS = WebLWS
  19
  20 let error = ref ""
  21
  22 let open_out () =
  23   let author = "λδ development binary: role manager" in
  24   let description = "λδ development binary: role manager" in
  25   let title = "Role Manager" in
  26   let css = Filename.concat !EG.base_url "css/roles.css" in
  27   let icon = Filename.concat !EG.base_url "images/crux_32.ico" in
  28   WS.open_out_html author description title css icon
  29
  30 let close_out () =
  31   WS.close_out_html ()
  32
  33 let string_of_request req arg =
  34   WS.string_of_request "roles" (["system-"^req, arg], "")
  35
  36 let status_out () =
  37   let button_specs = [
  38     "default", "Refresh";
  39     "save", "Save";
  40     "add", "Add";
  41     "match", "Match";
  42     "remove", "Remove";
  43   ] in
  44   let each_button (action, str) =
  45     let req = string_of_request action "" in
  46     KP.printf "<span class=\"button\"><a href=\"%s\">%s</a></span>\n" req str
  47   in
  48   let before_roles p count =
  49     let req = string_of_request "select" p in
  50     KP.printf "<div class=\"roles-head role-color\">\n";
  51     KP.printf "<a href=\"%s\">Roles:</a>\n" req;
  52     KP.printf "<span class=\"count\">%s</span>\n" count
  53   in
  54   let each_role p b str =
  55     let req_x = string_of_request "expand" p in
  56     let req_s = string_of_request "select" p in
  57     let s = if b then " selected" else "" in
  58     KP.printf "<div class=\"role role-color%s\">" s;
  59     KP.printf "<a href=\"%s\">⮞</a> " req_x;
  60     KP.printf "<a href=\"%s\">%s</a>" req_s str
  61   in
  62   let before_role x n o =
  63     let msg_n = if n then " (added)" else "" in
  64     let msg_o = if o then " (removed)" else "" in
  65     KP.printf "%s%s</div>\n" msg_n msg_o;
  66     if x then KP.printf "<div class=\"roles\">\n"
  67   in
  68   let after_role x =
  69     if x then KP.printf "</div>\n"
  70   in
  71   let after_roles () =
  72     KP.printf "</div>\n";
  73     KP.printf "<div class=\"buttons\">\n";
  74     List.iter each_button button_specs;
  75     KP.printf "</div>\n"
  76   in
  77   let stage s m =
  78     let msg_m = if m then " (modified)" else "" in
  79     KP.printf "<div class=\"stage role-color\">";
  80     KP.printf "Stage: %s%s" s msg_m;
  81     KP.printf "</div>\n"
  82   in
  83   let before_atoms a p count =
  84     let c, str =
  85       if a then "object-color", "objects"
  86       else "name-color", "names"
  87     in
  88     let req = string_of_request "select" p in
  89     KP.printf "<div class=\"atoms-head %s\">\n" c;
  90     KP.printf "<a href=\"%s\">%s:</a>\n" req str;
  91     KP.printf "<span class=\"count\">%s</span>\n" count;
  92     KP.printf "</div>\n";
  93     KP.printf "<div class=\"atoms\"><table class=\"atoms-table\"><tr>\n"
  94   in
  95   let each_atom a p b str =
  96     let c = if a then "object-color" else "name-color" in
  97     let s = if b then " selected" else "" in
  98     let req = string_of_request "select" p in
  99     KP.printf "<td class=\"atom %s%s\"><a href=\"%s\">%s</a></td>\n" c s req str
 100   in
 101   let after_atoms () =
 102     KP.printf "</tr></table></div>\n"
 103   in
 104   KP.printf "<div class=\"head\">Role Manager</div>\n";
 105   EE.visit_status
 106     before_roles each_role before_role after_role after_roles stage
 107     (before_atoms true) (each_atom true) after_atoms
 108     (before_atoms false) (each_atom false) after_atoms;
 109   if !error <> "" then
 110     KP.printf "<div class=\"error error-color\">Error: %s</div>\n" !error
 111
 112 let handler opt arg () =
 113   begin try match opt with
 114   | "system-default" -> ()
 115   | "system-add"     -> EE.add_role ()
 116   | "system-remove"  -> EE.remove_roles ()
 117   | "system-match"   -> EE.add_matching ()
 118   | "system-select"  -> EE.select_entry (EU.pointer_of_string arg)
 119   | "system-save"    -> EE.write_status ()
 120   | "system-expand"  -> EE.expand_entry (EU.pointer_of_string arg)
 121   | _                -> EU.raise_error (ET.EWrongRequest (opt, arg))
 122   with
 123   | ET.Error e -> error := EU.string_of_error e
 124   | e          -> error := Printexc.to_string e
 125   end;
 126   open_out ();
 127   status_out ();
 128   close_out ();
 129   error := ""
 130
 131 let init () =
 132   WS.loop_in ignore handler ignore ()