let already_included = NCicLibrary.get_transitively_included status in
let asserted,_ =
assert_ng ~already_included ~compiling ~asserted ~include_paths
- mafilename
+ ?uid:status#user mafilename
in
asserted,cmd
| cmd -> asserted,cmd
in
loop asserted status
-and compile ~compiling ~asserted ~include_paths ~outch fname =
+and compile ~compiling ~asserted ~include_paths ~outch ?uid fname =
if List.mem fname compiling then raise (CircularDependency fname);
let compiling = fname::compiling in
let matita_debug = Helm_registry.get_bool "matita.debug" in
activate_extraction baseuri fname ;
(* MATITA 1.0: debbo fare time_travel sulla ng_library? *)
(* FIXME: currently hardcoded to single user mode *)
- let status = new status None baseuri in
+ let status = new status uid baseuri in
let big_bang = Unix.gettimeofday () in
let { Unix.tms_utime = big_bang_u ; Unix.tms_stime = big_bang_s} =
Unix.times ()
let baseuri = NUri.uri_of_string baseuri in
let ngtime_of baseuri =
let ngpath = NCicLibrary.ng_path_of_baseuri uid baseuri in
+ let uid = match uid with Some u -> "Some " ^ u | _ -> "None" in
+ prerr_endline ("uid = " ^ uid);
+ prerr_endline ("ngpath = " ^ ngpath);
try
Some (Unix.stat ngpath).Unix.st_mtime
with Unix.Unix_error (Unix.ENOENT, "stat", f) when f = ngpath -> None in
(fun (asserted,b) mapath ->
let asserted,b1 =
assert_ng ~already_included ~compiling ~asserted ~include_paths
- mapath
+ ?uid mapath
in
asserted, b || b1
|| let _,baseuri,_,_ =
asserted, children_bad || matime > ngtime
| None -> asserted,true
in
+ prerr_endline ("asserted = " ^ (String.concat "," asserted));
if not to_be_compiled then fullmapath::asserted,false
else
if List.mem baseuri already_included then
| None -> open_out (fullmapath ^ ".mad"), true
| Some c -> c, false
in
- let asserted = compile ~compiling ~asserted ~include_paths ~outch fullmapath in
+ prerr_endline ("compiling " ^ fullmapath);
+ let asserted = compile ~compiling ~asserted ~include_paths ~outch ?uid fullmapath in
if is_file_ch then close_out outch;
fullmapath::asserted,true
end
(status, parsed_text, unparsed_txt'),"",(*parsed_text_len*)
utf8_length parsed_text
-(* FIXME: currently hard coded to single user mode *)
-let status = ref (new MatitaEngine.status (Some "ricciott") "cic:/matita");;
-let history = ref [!status];;
let sequent_size = ref 40;;
let include_paths = ref [];;
let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
- cgi # set_header
- ~cache:`No_cache
- ~content_type:"text/xml; charset=\"utf-8\""
- ();
- let filename = cgi # argument_value "file" in
- prerr_endline ("reading file " ^ filename);
- let body =
- Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false ()
- (read_file filename) in
- prerr_endline ("sending:\nBEGIN\n" ^ body ^ "\nEND");
- let body = "<file>" ^ body ^ "</file>" in
- let baseuri, incpaths =
- try
- let root, baseuri, _fname, _tgt =
- Librarian.baseuri_of_script ~include_paths:[] filename in
- let includes =
- try
- Str.split (Str.regexp " ")
- (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
- with Not_found -> []
- in
- let rc = root :: includes in
- List.iter (HLog.debug) rc; baseuri, rc
- with
- Librarian.NoRootFor _ | Librarian.FileNotFound _ -> "",[] in
- include_paths := incpaths;
- status := (!status)#set_baseuri baseuri;
- cgi#out_channel#output_string body;
+ let env = cgi#environment in
+ (try
+ let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
+ let sid = HExtlib.unopt sid in
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
+ let filename = cgi # argument_value "file" in
+ prerr_endline ("reading file " ^ filename);
+ let body =
+ Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false ()
+ (read_file filename) in
+ prerr_endline ("sending:\nBEGIN\n" ^ body ^ "\nEND");
+ let body = "<file>" ^ body ^ "</file>" in
+ let baseuri, incpaths =
+ try
+ let root, baseuri, _fname, _tgt =
+ Librarian.baseuri_of_script ~include_paths:[] filename in
+ let includes =
+ try
+ Str.split (Str.regexp " ")
+ (List.assoc "include_paths" (Librarian.load_root_file (root^"/root")))
+ with Not_found -> []
+ in
+ let rc = root :: includes in
+ List.iter (HLog.debug) rc; baseuri, rc
+ with
+ Librarian.NoRootFor _ | Librarian.FileNotFound _ -> "",[] in
+ include_paths := incpaths;
+ let status = MatitaAuthentication.get_status sid in
+ MatitaAuthentication.set_status sid (status#set_baseuri baseuri);
+ cgi#out_channel#output_string body;
+ with
+ | Not_found _ ->
+ cgi # set_header
+ ~status:`Internal_server_error
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ());
cgi#out_channel#commit_work()
;;
-let advance0 text =
+let advance0 sid text =
+ let status = MatitaAuthentication.get_status sid in
+ let history = MatitaAuthentication.get_history sid in
let (st,new_statements,new_unparsed),(* newtext TODO *) _,parsed_len =
(* try *)
- eval_statement !include_paths (*buffer*) !status (`Raw text)
+ eval_statement !include_paths (*buffer*) status (`Raw text)
(* with End_of_file -> raise Margin *)
in
- status := st;
- history := st :: !history;
- prerr_endline ("after advance0 history.length = " ^ string_of_int (List.length !history));
- parsed_len, new_unparsed
+ MatitaAuthentication.set_status sid st;
+ MatitaAuthentication.set_history sid (st::history);
+ parsed_len, new_unparsed, st
+let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
+ let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
+ let env = cgi#environment in
+
+ prerr_endline "1";
+ assert (cgi#arguments <> []);
+ let uid = cgi#argument_value "userid" in
+ let userpw = cgi#argument_value "password" in
+ prerr_endline ("2: user = " ^ uid);
+ let pw,_ = MatitaAuthentication.lookup_user uid in
+ prerr_endline "3";
+
+ if pw = userpw then
+ begin
+ prerr_endline "4";
+ let sid = MatitaAuthentication.create_session uid in
+ let cookie = Netcgi.Cookie.make "session" (Uuidm.to_string sid) in
+ cgi#set_header ~status:`See_other ~cache:`No_cache ~set_cookies:[cookie] ();
+ env#set_output_header_field "Location" "/index.html"
+ end
+ else
+ begin
+ cgi#set_header
+ ~cache:`No_cache
+ ~content_type:"text/html; charset=\"utf-8\""
+ ();
+ cgi#out_channel#output_string
+ "<html><head></head><body>Authentication error</body></html>"
+ end;
+
+ cgi#out_channel#commit_work()
+
+;;
+
(* returns the length of the executed text and an html representation of the
* current metasenv*)
let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
- cgi # set_header
- ~cache:`No_cache
- ~content_type:"text/xml; charset=\"utf-8\""
- ();
- let text = cgi#argument_value "body" in
- prerr_endline ("body =\n" ^ text);
- let parsed_len, new_unparsed = advance0 text in
- let txt = output_status !status in
- let body =
- "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\" />" ^ txt
- ^ "</response>"
- in
- prerr_endline ("sending advance response:\n" ^ body);
- cgi#out_channel#output_string body;
+ let env = cgi#environment in
+ (try
+ let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
+ let sid = HExtlib.unopt sid in
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
+ let text = cgi#argument_value "body" in
+ prerr_endline ("body =\n" ^ text);
+ let parsed_len, new_unparsed, new_status = advance0 sid text in
+ let txt = output_status new_status in
+ let body =
+ "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\" />" ^ txt
+ ^ "</response>"
+ in
+ prerr_endline ("sending advance response:\n" ^ body);
+ cgi#out_channel#output_string body
+ with
+ | Not_found _ ->
+ cgi # set_header
+ ~status:`Internal_server_error
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ());
cgi#out_channel#commit_work()
;;
let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
- let rec aux parsed_len text =
- try
- prerr_endline ("evaluating: " ^ first_line text);
- let plen,new_unparsed = advance0 text in
- aux (parsed_len+plen) new_unparsed
- with
- | _ -> parsed_len
- in
let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
- cgi # set_header
- ~cache:`No_cache
- ~content_type:"text/xml; charset=\"utf-8\""
- ();
- let text = cgi#argument_value "body" in
- prerr_endline ("body =\n" ^ text);
- let parsed_len = aux 0 text in
- let txt = output_status !status in
- let body =
- "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\" />" ^ txt
- ^ "</response>"
- in
- prerr_endline ("sending goto bottom response:\n" ^ body);
- cgi#out_channel#output_string body;
+ let env = cgi#environment in
+ (try
+ let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
+ let sid = HExtlib.unopt sid in
+
+ let rec aux parsed_len text =
+ try
+ prerr_endline ("evaluating: " ^ first_line text);
+ let plen,new_unparsed,_new_status = advance0 sid text in
+ aux (parsed_len+plen) new_unparsed
+ with
+ | _ -> parsed_len
+ in
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
+ let text = cgi#argument_value "body" in
+ prerr_endline ("body =\n" ^ text);
+ let parsed_len = aux 0 text in
+ let status = MatitaAuthentication.get_status sid in
+ let txt = output_status status in
+ let body =
+ "<response><parsed length=\"" ^ (string_of_int parsed_len) ^ "\" />" ^ txt
+ ^ "</response>"
+ in
+ prerr_endline ("sending goto bottom response:\n" ^ body);
+ cgi#out_channel#output_string body
+ with Not_found -> cgi#set_header ~status:`Internal_server_error
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\"" ());
cgi#out_channel#commit_work()
;;
let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) =
let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in
- cgi # set_header
- ~cache:`No_cache
- ~content_type:"text/xml; charset=\"utf-8\""
- ();
- let new_history,new_status =
- match !history with
- _::(status::_ as history) ->
- history, status
- | [_] -> (prerr_endline "singleton";failwith "retract")
- | _ -> (prerr_endline "nil"; assert false) in
- NCicLibrary.time_travel new_status;
- history := new_history;
- status := new_status;
- prerr_endline ("after retract history.length = " ^ string_of_int (List.length !history));
- let body = output_status !status in
- cgi#out_channel#output_string body;
+ let env = cgi#environment in
+ (try
+ let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in
+ let sid = HExtlib.unopt sid in
+ cgi # set_header
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\""
+ ();
+ let history = MatitaAuthentication.get_history sid in
+ let new_history,new_status =
+ match history with
+ _::(status::_ as history) ->
+ history, status
+ | [_] -> (prerr_endline "singleton";failwith "retract")
+ | _ -> (prerr_endline "nil"; assert false) in
+ NCicLibrary.time_travel new_status;
+ MatitaAuthentication.set_history sid new_history;
+ MatitaAuthentication.set_status sid new_status;
+ prerr_endline ("after retract history.length = " ^
+ string_of_int (List.length new_history));
+ let body = output_status new_status in
+ cgi#out_channel#output_string body
+ with _ -> cgi#set_header ~status:`Internal_server_error
+ ~cache:`No_cache
+ ~content_type:"text/xml; charset=\"utf-8\"" ());
cgi#out_channel#commit_work()
;;
dyn_translator = (fun _ -> ""); (* not needed *)
dyn_accept_all_conditionals = false;
} in
+ let do_login =
+ { Nethttpd_services.dyn_handler = (fun _ -> login);
+ dyn_activation = Nethttpd_services.std_activation `Std_activation_buffered;
+ dyn_uri = None; (* not needed *)
+ dyn_translator = (fun _ -> ""); (* not needed *)
+ dyn_accept_all_conditionals = false;
+ } in
let nethttpd_factory =
Nethttpd_plex.nethttpd_factory
~handlers:[ "advance", do_advance
; "retract", do_retract
; "bottom", goto_bottom
- ; "open", retrieve ]
+ ; "open", retrieve
+ ; "login", do_login ]
() in
MatitaInit.initialize_all ();
(* test begin *)
function initialize()
{
- locked = document.getElementById("locked");
- unlocked = document.getElementById("unlocked");
- workarea = document.getElementById("workarea");
- scriptcell = document.getElementById("scriptcell");
- goalcell = document.getElementById("goalcell");
- goals = document.getElementById("goals");
- goalview = document.getElementById("goalview");
- filename = document.getElementById("filename");
- logarea = document.getElementById("logarea");
- advanceButton = document.getElementById("advance");
- retractButton = document.getElementById("retract");
- cursorButton = document.getElementById("cursor");
- bottomButton = document.getElementById("bottom");
-
- // hide sequent view at start
- hideSequent();
+ if (readCookie("session") == null) {
+ window.location = "/login.html"
+ } else {
+ locked = document.getElementById("locked");
+ unlocked = document.getElementById("unlocked");
+ workarea = document.getElementById("workarea");
+ scriptcell = document.getElementById("scriptcell");
+ goalcell = document.getElementById("goalcell");
+ goals = document.getElementById("goals");
+ goalview = document.getElementById("goalview");
+ filename = document.getElementById("filename");
+ logarea = document.getElementById("logarea");
+ advanceButton = document.getElementById("advance");
+ retractButton = document.getElementById("retract");
+ cursorButton = document.getElementById("cursor");
+ bottomButton = document.getElementById("bottom");
+
+ // hide sequent view at start
+ hideSequent();
+ }
}
function debug(txt)
function test () {
debug("cursor test: " + unlocked.innerHTML.substr(0,getCursorPos()));
}
+
+function readCookie(name) {
+ var nameEQ = name + "=";
+ var ca = document.cookie.split(';');
+ for(var i=0;i < ca.length;i++) {
+ var c = ca[i];
+ while (c.charAt(0)==' ') c = c.substring(1,c.length);
+ if (c.indexOf(nameEQ) == 0) return c.substring(nameEQ.length,c.length);
+ }
+ return null;
+}
projects / helm.git / commitdiff