X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitadaemon.ml;h=fc8c9684e87534819f855ba1786723c347738e2a;hb=93db728b3f690d2c683f64833353da685a6f1b65;hp=081ce316538b6563bf38b55650cf1b13e7f458f2;hpb=0d0fca7f894b1aadd4840d550b65183fc4a9c124;p=helm.git diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index 081ce3165..fc8c9684e 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -3,9 +3,14 @@ open Http_types;; exception Emphasized_error of string exception Disamb_error of string +exception Generic_error of string module Stack = Continuationals.Stack +let debug = prerr_endline +(* disable for debug *) +let prerr_endline _ = () + let rt_path () = Helm_registry.get "matita.rt_base_dir" let libdir uid = (rt_path ()) ^ "/users/" ^ uid @@ -37,7 +42,7 @@ let add_user_for_commit uid = Mutex.unlock mutex; ;; -let do_global_commit () = +let do_global_commit (* () *) uid = prerr_endline ("to be committed: " ^ String.concat " " !to_be_committed); List.fold_left (fun out u -> @@ -142,7 +147,11 @@ let do_global_commit () = (* XXX: at the moment, we don't keep track of the order in which users have scheduled their commits, but we should, otherwise we will get a "first come, random served" policy *) - "" (* (List.rev !to_be_committed) *) (MatitaAuthentication.get_users ()) + "" (* (List.rev !to_be_committed) *) + (* replace [uid] to commit all users: + (MatitaAuthentication.get_users ()) + *) + [uid] ;; (*** from matitaScript.ml ***) @@ -200,8 +209,8 @@ let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script Printf.sprintf "\005A href=\"%s\"\006%s\005/A\006" (NReference.string_of_reference r) (NCicPp.r2s status true r) in - if trace = [] then "{}" - else String.concat ", " + (*if trace = [] then "{}" + else*) String.concat ", " (HExtlib.filter_map (function | NotationPt.NRef r -> Some (href r) | _ -> None) @@ -209,6 +218,26 @@ let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script in match ast with + | GrafiteAst.Executable (_, + GrafiteAst.NCommand (_, + GrafiteAst.NObj (loc, astobj,_))) -> + let objname = NotationPt.name_of_obj astobj in + let status = + MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:false status ("",0,ast) + in + let new_parsed_text = Ulexing.from_utf8_string parsed_text in + let interpr = GrafiteDisambiguate.get_interpr status#disambiguate_db in + let outstr = ref "" in + ignore (SmallLexer.mk_small_printer interpr outstr new_parsed_text); + let x, y = HExtlib.loc_of_floc floc in + let pre = Netconversion.ustring_sub `Enc_utf8 0 x !outstr in + let post = Netconversion.ustring_sub `Enc_utf8 x + (Netconversion.ustring_length `Enc_utf8 !outstr - x) !outstr in + outstr := Printf.sprintf + "%s\005img class=\"anchor\" src=\"icons/tick.png\" id=\"%s\" /\006%s" pre objname post; + prerr_endline ("baseuri after advance = " ^ status#baseuri); + (* prerr_endline ("parser output: " ^ !outstr); *) + (status,!outstr, unparsed_txt'),parsed_text_len | GrafiteAst.Executable (_, GrafiteAst.NTactic (_, [GrafiteAst.NAuto (_, (l,a as auto_params))])) when is_auto auto_params @@ -358,6 +387,7 @@ let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = ~content_type:"text/xml; charset=\"utf-8\"" (); *) + let readonly = cgi # argument_value "readonly" in let filename = libdir uid ^ "/" ^ (cgi # argument_value "file") in (* prerr_endline ("reading file " ^ filename); *) let body = @@ -382,16 +412,23 @@ let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = with Librarian.NoRootFor _ | Librarian.FileNotFound _ -> "",[] in include_paths := incpaths; - let status = (MatitaAuthentication.get_status sid)#set_baseuri baseuri in - let history = [status] in - MatitaAuthentication.set_status sid status; - MatitaAuthentication.set_history sid history; + if readonly <> "true" then + (let status = new MatitaEngine.status (Some uid) baseuri in + let history = [status] in + MatitaAuthentication.set_status sid status; + MatitaAuthentication.set_history sid history); cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); cgi#out_channel#output_string body; with + | Sys_error _ -> + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + cgi#out_channel#output_string "" | Not_found _ -> cgi # set_header ~status:`Internal_server_error @@ -445,33 +482,56 @@ let advance0 sid text = let history = MatitaAuthentication.get_history sid in let status = status#reset_disambiguate_db () in let (st,new_statements,new_unparsed),parsed_len = - try - eval_statement !include_paths (*buffer*) status (`Raw text) - with - | HExtlib.Localized (floc,e) as exn -> + let rec do_exc = function + | MatitaEngine.EnrichedWithStatus (e,_) -> do_exc e + | NCicTypeChecker.TypeCheckerFailure s -> raise (Generic_error (Lazy.force s)) + | HExtlib.Localized (floc,e) -> let x, y = HExtlib.loc_of_floc floc in - prerr_endline (Printf.sprintf "ustring_sub caso 2: (%d,%d) parsed=%s" 0 x text); let pre = Netconversion.ustring_sub `Enc_utf8 0 x text in - prerr_endline (Printf.sprintf "ustring_sub caso 3: (%d,%d) parsed=%s" x (y-x) text); let err = Netconversion.ustring_sub `Enc_utf8 x (y-x) text in - prerr_endline (Printf.sprintf "ustring_sub caso 4: (%d,%d) parsed=%s" y (Netconversion.ustring_length `Enc_utf8 text - y) text); let post = Netconversion.ustring_sub `Enc_utf8 y (Netconversion.ustring_length `Enc_utf8 text - y) text in - let _,title = MatitaExcPp.to_string exn in + let _,title = MatitaExcPp.to_string e in (* let title = "" in *) let marked = pre ^ "\005span class=\"error\" title=\"" ^ title ^ "\"\006" ^ err ^ "\005/span\006" ^ post in let marked = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (html_of_matita marked) in - raise (Emphasized_error marked) + raise (Emphasized_error marked) + | Disambiguate.NoWellTypedInterpretation (floc,e) -> + let x, y = HExtlib.loc_of_floc floc in + let pre = Netconversion.ustring_sub `Enc_utf8 0 x text in + let err = Netconversion.ustring_sub `Enc_utf8 x (y-x) text in + let post = Netconversion.ustring_sub `Enc_utf8 y + (Netconversion.ustring_length `Enc_utf8 text - y) text in + (*let _,title = MatitaExcPp.to_string e in*) + (* let title = "" in *) + let marked = + pre ^ "\005span class=\"error\" title=\"" ^ e ^ "\"\006" ^ err ^ "\005/span\006" ^ post in + let marked = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false + () (html_of_matita marked) in + raise (Emphasized_error marked) + | NCicRefiner.Uncertain m as exn -> + let floc, e = Lazy.force m in + let x, y = HExtlib.loc_of_floc floc in + let pre = Netconversion.ustring_sub `Enc_utf8 0 x text in + let err = Netconversion.ustring_sub `Enc_utf8 x (y-x) text in + let post = Netconversion.ustring_sub `Enc_utf8 y + (Netconversion.ustring_length `Enc_utf8 text - y) text in + (* let _,title = MatitaExcPp.to_string e in *) + (* let title = "" in *) + let marked = + pre ^ "\005span class=\"error\" title=\"" ^ e ^ "\"\006" ^ err ^ "\005/span\006" ^ post in + let marked = Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false + () (html_of_matita marked) in + raise (Emphasized_error marked) | NTacStatus.Error (s,None) as e -> prerr_endline - ("NTacStatus.Error " ^ (Lazy.force s)); - raise e + ("NTacStatus.Error " ^ (Lazy.force s)); raise e | NTacStatus.Error (s,Some exc) as e -> prerr_endline ("NTacStatus.Error " ^ Lazy.force s ^ " -- " ^ (Printexc.to_string exc)); - raise e + do_exc exc | GrafiteDisambiguate.Ambiguous_input (loc,choices) -> let x,y = HExtlib.loc_of_floc loc in let choice_of_alias = function @@ -515,9 +575,27 @@ let advance0 sid text = in raise (Disamb_error strchoices) | GrafiteDisambiguate.Error l -> raise (Disamb_error (xml_of_disamb_error l)) (* | End_of_file -> ... *) + | e -> + (* prerr_endline ("matitadaemon *** Unhandled exception " ^ Printexc.to_string e); *) + prerr_endline ("matitadaemon *** Unhandled exception " ^ snd (MatitaExcPp.to_string e)); + raise e + in + + try + eval_statement !include_paths (*buffer*) status (`Raw text) + with e -> do_exc e in + debug "BEGIN PRINTGRAMMAR"; + (*prerr_endline (Print_grammar.ebnf_of_term status);*) + (*let kwds = String.concat ", " status#get_kwds in + debug ("keywords = " ^ kwds );*) + debug "END PRINTGRAMMAR"; MatitaAuthentication.set_status sid st; MatitaAuthentication.set_history sid (st::history); +(* prerr_endline "previous timestamp"; + status#print_timestamp(); + prerr_endline "current timestamp"; + st#print_timestamp(); *) parsed_len, Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () (html_of_matita new_statements), new_unparsed, st @@ -529,8 +607,9 @@ let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = assert (cgi#arguments <> []); let uid = cgi#argument_value "userid" in let userpw = cgi#argument_value "password" in - (try - MatitaAuthentication.add_user uid userpw; + (try + (* currently registering only unprivileged users *) + MatitaAuthentication.add_user uid userpw false; (* env#set_output_header_field "Location" "/index.html" *) cgi#out_channel#output_string ("" @@ -563,6 +642,7 @@ let login (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let userpw = cgi#argument_value "password" in (try MatitaAuthentication.check_pw uid userpw; + NCicLibrary.init (Some uid); let ft = MatitaAuthentication.read_ft uid in let _ = MatitaFilesystem.html_of_library uid ft in let sid = MatitaAuthentication.create_session uid in @@ -663,6 +743,10 @@ let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = cgi#out_channel#output_string "ok" with | File_already_exists -> + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); cgi#out_channel#output_string "cancelled" | Sys_error _ -> cgi # set_header @@ -671,6 +755,10 @@ let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = ~content_type:"text/xml; charset=\"utf-8\"" () | e -> + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); let estr = Printexc.to_string e in cgi#out_channel#output_string ("" ^ estr ^ "")); cgi#out_channel#commit_work() @@ -678,9 +766,13 @@ let save (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let initiate_commit (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in - let _env = cgi#environment in + let env = cgi#environment in (try - let out = do_global_commit () in + let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in + let sid = HExtlib.unopt sid in + MatitaAuthentication.probe_commit_priv sid; + let uid = MatitaAuthentication.user_of_session sid in + let out = do_global_commit (* () *) uid in cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" @@ -690,6 +782,13 @@ let initiate_commit (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = cgi#out_channel#output_string ("
" ^ out ^ "
"); cgi#out_channel#output_string "" with + | Failure _ -> + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + cgi#out_channel#output_string + "no commit privileges" | Not_found _ -> cgi # set_header ~status:`Internal_server_error @@ -706,6 +805,7 @@ let svn_update (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let sid = HExtlib.unopt sid in let uid = MatitaAuthentication.user_of_session sid in (try + MatitaAuthentication.probe_commit_priv sid; let files,anomalies,(added,conflict,del,upd,merged) = MatitaFilesystem.update_user uid in @@ -732,6 +832,13 @@ let svn_update (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = cgi#out_channel#output_string ("
" ^ details ^ "
"); cgi#out_channel#output_string ""; with + | Failure _ -> + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + cgi#out_channel#output_string + "no commit privileges" | Not_found _ -> cgi # set_header ~status:`Internal_server_error @@ -743,6 +850,7 @@ let svn_update (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = (* returns the length of the executed text and an html representation of the * current metasenv*) +(*let advance =*) let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in @@ -771,9 +879,16 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = (); cgi#out_channel#output_string body with + | Generic_error text -> + let body = "" ^ text ^ "" in + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + cgi#out_channel#output_string body | Emphasized_error text -> (* | MultiPassDisambiguator.DisambiguationError (offset,errorll) -> *) - let body = "" ^ text ^ "" in + let body = "" ^ text ^ "" in cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" @@ -786,6 +901,13 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = ~content_type:"text/xml; charset=\"utf-8\"" (); cgi#out_channel#output_string body + | End_of_file _ -> + let body = "" in + cgi # set_header + ~cache:`No_cache + ~content_type:"text/xml; charset=\"utf-8\"" + (); + cgi#out_channel#output_string body | Not_found _ -> cgi # set_header ~status:`Internal_server_error @@ -802,7 +924,6 @@ let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = (* (try *) let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in let sid = HExtlib.unopt sid in - let history = MatitaAuthentication.get_history sid in let error_msg = function | Emphasized_error text -> "" ^ text ^ "" @@ -819,11 +940,12 @@ let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = prerr_endline ("evaluating: " ^ first_line text); let plen,new_parsed,new_unparsed,_new_status = advance0 sid text in aux ((plen,new_parsed)::acc) new_unparsed - with e -> + with e -> acc, error_msg e + (* DON'T SERIALIZE NOW!!! let status = MatitaAuthentication.get_status sid in GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string status#baseuri) status; - acc, error_msg e + acc, error_msg e *) in (* cgi # set_header @@ -907,13 +1029,18 @@ let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = (); *) let history = MatitaAuthentication.get_history sid in + let old_status = MatitaAuthentication.get_status 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 - prerr_endline ("prima della time travel"); +(* prerr_endline "timestamp prima della retract"; + old_status#print_timestamp (); + prerr_endline "timestamp della retract"; + new_status#print_timestamp (); + prerr_endline ("prima della time travel"); *) NCicLibrary.time_travel new_status; prerr_endline ("dopo della time travel"); MatitaAuthentication.set_history sid new_history;