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