X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2Fmatitadaemon.ml;h=f0baa4ed0a08c22fa72ea4c10605e21887aae8de;hb=0aa993bb1d23567612aa5d63fab74ef6fb918c0d;hp=a53d24f676ae3c3ec9a86e8182700e1a4aa9942c;hpb=5fbe7da7019bda8fead167c8b1da1b06625551b3;p=helm.git diff --git a/matitaB/matita/matitadaemon.ml b/matitaB/matita/matitadaemon.ml index a53d24f67..f0baa4ed0 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,88 @@ 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 + 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 +308,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 = @@ -346,7 +403,7 @@ let retrieve (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = let advance0 sid text = let status = MatitaAuthentication.get_status 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) with @@ -414,16 +471,10 @@ 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; 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 @@ -721,14 +772,14 @@ let gotoBottom (cgi : Netcgi1_compat.Netcgi_types.cgi_activation) = 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 -> + | (* End_of_file *) _ -> 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 + (*| _ -> parsed_len, parsed_txt*) in (* cgi # set_header