X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matitaB%2Fmatita%2Fmatitadaemon.ml;h=14bcf1db6d9b757d34c50263f8fd26194cef33e3;hb=c6dc6200c1e3022bf76b9589a8e30dd1cc6e864c;hp=9fc2b1bbcf05b30e9cc327f39ba847dc0d29b5d4;hpb=0e3d8e00433a9a4dd72310c1e889814848a96c10;p=helm.git diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index 9fc2b1bbc..14bcf1db6 100644 --- a/matitaB/matita/matitadaemon.ml +++ b/matitaB/matita/matitadaemon.ml @@ -16,6 +16,18 @@ let mutex = Mutex.create ();; let to_be_committed = ref [];; +let html_of_matita s = + let patt1 = Str.regexp "\005" in + let patt2 = Str.regexp "\006" in + let patt3 = Str.regexp "<" in + let patt4 = Str.regexp ">" in + let res = Str.global_replace patt4 ">" s in + let res = Str.global_replace patt3 "<" res in + let res = Str.global_replace patt2 ">" res in + let res = Str.global_replace patt1 "<" res in + res +;; + (* adds a user to the commit queue; concurrent instances possible, so we * enclose the update in a CS *) @@ -143,31 +155,89 @@ let eval_statement include_paths (* (buffer : GText.buffer) *) status (* script match statement with | `Raw text -> (* if Pcre.pmatch ~rex:only_dust_RE text then raise Margin; *) + prerr_endline ("raw text = " ^ text); let strm = GrafiteParser.parsable_statement status (Ulexing.from_utf8_string text) in + prerr_endline "before get_ast"; let ast = MatitaEngine.get_ast status include_paths strm in + prerr_endline "after get_ast"; ast, text | `Ast (st, text) -> st, text in + + (* do we want to generate a trace? *) + let is_auto (l,a) = + not (List.mem_assoc "demod" a || List.mem_assoc "paramod" a || + List.mem_assoc "fast_paramod" a || List.assoc "depth" a = "1" || + l <> None) + in + + let get_param a param = + try + Some (param ^ "=" ^ List.assoc param a) + with Not_found -> None + in + let floc = match ast with | GrafiteAst.Executable (loc, _) | GrafiteAst.Comment (loc, _) -> loc in - let _,lend = HExtlib.loc_of_floc floc in + let lstart,lend = HExtlib.loc_of_floc floc in let parsed_text, _parsed_text_len = HExtlib.utf8_parsed_text unparsed_text (HExtlib.floc_of_loc (0,lend)) in + let parsed_text_len = utf8_length parsed_text in let byte_parsed_text_len = String.length parsed_text in let unparsed_txt' = String.sub unparsed_text byte_parsed_text_len (String.length unparsed_text - byte_parsed_text_len) in + prerr_endline (Printf.sprintf "ustring_sub caso 1: lstart=%d, parsed=%s" lstart parsed_text); + let pre = Netconversion.ustring_sub `Enc_utf8 0 lstart parsed_text in + + let mk_univ trace = + let href r = + 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 ", " + (HExtlib.filter_map (function + | NotationPt.NRef r -> Some (href r) + | _ -> None) + trace) + in - let status = - MatitaEngine.eval_ast ~include_paths ~do_heavy_checks:false status ("",0,ast) - in - (status, parsed_text, unparsed_txt'),"",(*parsed_text_len*) - utf8_length parsed_text + match ast with + | GrafiteAst.Executable (_, + GrafiteAst.NTactic (_, + [GrafiteAst.NAuto (_, (l,a as auto_params))])) when is_auto auto_params + -> + let l = match l with + | None -> None + | Some (_,l') -> Some (List.map (fun x -> "",0,x) l') + in + let trace_ref = ref [] in + let status = NnAuto.auto_tac ~params:(l,a) ~trace_ref status in + let new_parsed_text = pre ^ (Printf.sprintf + "/\005span class='autotactic'\006%s\005span class='autotrace'\006 trace %s\005/span\006\005/span\006/" + (String.concat " " + (List.assoc "depth" a:: + HExtlib.filter_map (get_param a) ["width";"size"])) + (mk_univ !trace_ref)) + in + (status,new_parsed_text, unparsed_txt'),parsed_text_len + | _ -> + 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); + prerr_endline ("baseuri after advance = " ^ status#baseuri); + (* prerr_endline ("parser output: " ^ !outstr); *) + (status,!outstr, unparsed_txt'),parsed_text_len (*let save_moo status = let script = MatitaScript.current () in @@ -239,18 +309,6 @@ let output_status s = (* prerr_endline ("sending metasenv:\n" ^ res); res *) ;; -let html_of_matita s = - let patt1 = Str.regexp "\005" in - let patt2 = Str.regexp "\006" in - let patt3 = Str.regexp "<" in - let patt4 = Str.regexp ">" in - let res = Str.global_replace patt4 ">" s in - let res = Str.global_replace patt3 "<" res in - let res = Str.global_replace patt2 ">" res in - let res = Str.global_replace patt1 "<" res in - res -;; - let heading_nl_RE = Pcre.regexp "^\\s*\n\\s*";; let first_line s = @@ -345,15 +403,19 @@ let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let advance0 sid text = let status = MatitaAuthentication.get_status sid in + let history = MatitaAuthentication.get_history sid in let status = status#reset_disambiguate_db () in - let (st,new_statements,new_unparsed),(* newtext TODO *) _,parsed_len = + let (st,new_statements,new_unparsed),parsed_len = try - eval_statement !include_paths (*buffer*) status (`Raw text) + eval_statement !include_paths (*buffer*) status (`Raw text) with | HExtlib.Localized (floc,e) as exn -> 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 @@ -363,6 +425,14 @@ let advance0 sid text = 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 (s,Some exc) as e -> + prerr_endline + ("NTacStatus.Error " ^ Lazy.force s ^ " -- " ^ (Printexc.to_string exc)); + raise e | GrafiteDisambiguate.Ambiguous_input (loc,choices) -> let x,y = HExtlib.loc_of_floc loc in let choice_of_alias = function @@ -406,16 +476,11 @@ let advance0 sid text = in raise (Ambiguous strchoices) (* | End_of_file -> ... *) in - let stringbuf = Ulexing.from_utf8_string new_statements in - let interpr = GrafiteDisambiguate.get_interpr st#disambiguate_db in - let outstr = ref "" in - ignore (SmallLexer.mk_small_printer interpr outstr stringbuf); - prerr_endline ("baseuri after advance = " ^ st#baseuri); - (* prerr_endline ("parser output: " ^ !outstr); *) MatitaAuthentication.set_status sid st; + MatitaAuthentication.set_history sid (st::history); parsed_len, Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false - () (html_of_matita !outstr), new_unparsed, st + () (html_of_matita new_statements), new_unparsed, st let register (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in @@ -659,9 +724,7 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = *) let text = cgi#argument_value "body" in (* prerr_endline ("body =\n" ^ text); *) - let history = MatitaAuthentication.get_history sid in let parsed_len, new_parsed, new_unparsed, new_status = advance0 sid text in - MatitaAuthentication.set_history sid (new_status::history); let txt = output_status new_status in let body = "" ^ @@ -695,32 +758,39 @@ let advance (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = ~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 cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in - (try +(* (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 rec aux parsed_len parsed_txt text = + let error_msg = function + | Emphasized_error text -> "" ^ text ^ "" + | Ambiguous text -> (* *) text + | End_of_file _ -> (* not an error *) "" + | e -> (* unmanaged error *) + "" ^ + (Netencoding.Html.encode ~in_enc:`Enc_utf8 ~prefer_name:false () + (Printexc.to_string e)) ^ "" + in + + let rec aux acc text = try prerr_endline ("evaluating: " ^ first_line text); let plen,new_parsed,new_unparsed,_new_status = advance0 sid text in - aux (parsed_len+plen) (parsed_txt ^ new_parsed) new_unparsed - with - | End_of_file -> + aux ((plen,new_parsed)::acc) new_unparsed + with e -> let status = MatitaAuthentication.get_status sid in GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string status#baseuri) status; - if parsed_len > 0 then - MatitaAuthentication.set_history sid (status::history); - parsed_len, parsed_txt - | _ -> parsed_len, parsed_txt + acc, error_msg e in (* cgi # set_header @@ -730,27 +800,27 @@ let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = *) let text = cgi#argument_value "body" in (* prerr_endline ("body =\n" ^ text); *) - let parsed_len, new_parsed = aux 0 "" text in + let len_parsedlist, err_msg = aux [] text in let status = MatitaAuthentication.get_status sid in let txt = output_status status in + let parsed_tag (len,txt) = + "" ^ txt ^ "" + in + (* List.rev: the list begins with the older parsed txt *) let body = - "" ^ - new_parsed ^ "" ^ txt - ^ "" - in - (*let body = - "" ^ txt - ^ "" - in*) + "" ^ + String.concat "" (List.rev (List.map parsed_tag len_parsedlist)) ^ + txt ^ err_msg ^ "" + in (* prerr_endline ("sending goto bottom response:\n" ^ body); *) cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" (); - cgi#out_channel#output_string body - with Not_found -> cgi#set_header ~status:`Internal_server_error + 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\"" ()); + ~content_type:"text/xml; charset=\"utf-8\"" ()); *) cgi#out_channel#commit_work() ;; @@ -772,12 +842,12 @@ let gotoTop (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let baseuri = status#baseuri in let new_status = new MatitaEngine.status (Some uid) baseuri in prerr_endline "gototop prima della time travel"; - NCicLibrary.time_travel new_status; + (* NCicLibrary.time_travel new_status; *) prerr_endline "gototop dopo della time travel"; let new_history = [new_status] in MatitaAuthentication.set_history sid new_history; MatitaAuthentication.set_status sid new_status; - NCicLibrary.time_travel new_status; + (* NCicLibrary.time_travel new_status; *) cgi # set_header ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" @@ -794,7 +864,7 @@ let gotoTop (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let cgi = Netcgi1_compat.Netcgi_types.of_compat_activation cgi in let env = cgi#environment in - (try + (try let sid = Uuidm.of_string (Netcgi.Cookie.value (env#cookie "session")) in let sid = HExtlib.unopt sid in (* @@ -822,7 +892,9 @@ let retract (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = ~content_type:"text/xml; charset=\"utf-8\"" (); cgi#out_channel#output_string body - with _ -> cgi#set_header ~status:`Internal_server_error + with e -> + prerr_endline ("error in retract: " ^ Printexc.to_string e); + cgi#set_header ~status:`Internal_server_error ~cache:`No_cache ~content_type:"text/xml; charset=\"utf-8\"" ()); cgi#out_channel#commit_work()