From: Stefano Zacchiroli Date: Fri, 27 May 2005 16:54:05 +0000 (+0000) Subject: - commented out no longer needed macros Redo, Undo, Abort X-Git-Tag: PRE_INDEX_1~107 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a256fcff08b4a21c736167910c1ce342cffb0388;p=helm.git - commented out no longer needed macros Redo, Undo, Abort - bugfix: correctly handles "cic:" and "cic:/" pseudo-uris in cicBrowser - bugfix: fixed String.sub error on directories shorted than 5 chars --- diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml index cf7939fa7..0178982e9 100644 --- a/helm/matita/matita.ml +++ b/helm/matita/matita.ml @@ -146,6 +146,11 @@ let _ = (fun _ -> let nb = gui#main#hintNotebook in nb#goto_page ((nb#current_page + 1) mod 3)); + addDebugItem "print (on stdout) \"statement\" grammar entry" + (fun _ -> + Grammar.print_entry Format.std_formatter + (Grammar.Entry.obj CicTextualParser2.statement); + Format.pp_print_flush Format.std_formatter ()); end (** *) diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 5fe955b3e..0a2e8f90d 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -378,8 +378,13 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) ignore(win#whelpResultTreeview#connect#row_activated ~callback:(fun _ _ -> let selection = self#_getWhelpResultTreeviewSelection () in + let is_cic s = + try + String.sub s 0 5 = "cic:/" + with Invalid_argument _ -> false + in let txt = - if String.sub selection 0 5 = "cic:/" then + if is_cic selection then selection else win#browserUri#text ^ selection @@ -558,10 +563,12 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) let is_uri txt = try let u = UriManager.strip_xpointer (UriManager.uri_of_string txt) in - ignore(Http_getter.resolve' u); true + ignore (Http_getter.resolve' u); + true with | Http_getter_types.Key_not_found _ - | Http_getter_types.Unresolvable_URI _ -> false + | Http_getter_types.Unresolvable_URI _ + | UriManager.IllFormedUri ("cic:/" | "cic:") -> false | UriManager.IllFormedUri u -> failwith ("Malformed URI '" ^ u ^ "'") in let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index 0d59d6f47..c8fbba9be 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -100,7 +100,7 @@ let eval_with_engine status user_goal parsed_text st = else new_text in - [ new_status, new_text ], parsed_text_length, None + [ new_status, new_text ], parsed_text_length let disambiguate term status = let module MD = MatitaDisambiguator in @@ -114,7 +114,8 @@ let disambiguate term status = | _ -> assert false let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text -script mac = + script mac += let module TA = TacticAst in let module TAPp = TacticAstPp in let module MQ = MetadataQuery in @@ -132,18 +133,18 @@ script mac = let l = MQ.match_term ~dbd term in let entry = `Whelp (TAPp.pp_macro_cic (TA.WMatch (loc, term)), l) in mathviewer#show_uri_list ~reuse:true ~entry l; - [], parsed_text_length, None + [], parsed_text_length | TA.WInstance (loc, term) -> let term = disambiguate term status in let l = MQ.instance ~dbd term in let entry = `Whelp (TAPp.pp_macro_cic (TA.WInstance (loc, term)), l) in mathviewer#show_uri_list ~reuse:true ~entry l; - [], parsed_text_length, None + [], parsed_text_length | TA.WLocate (loc, s) -> let l = MQ.locate ~dbd s in let entry = `Whelp (TAPp.pp_macro_cic (TA.WLocate (loc, s)), l) in mathviewer#show_uri_list ~reuse:true ~entry l; - [], parsed_text_length, None + [], parsed_text_length | TA.WElim (loc, term) -> let term = disambiguate term status in let uri = @@ -154,21 +155,21 @@ script mac = let l = MQ.elim ~dbd uri in let entry = `Whelp (TAPp.pp_macro_cic (TA.WElim (loc, term)), l) in mathviewer#show_uri_list ~reuse:true ~entry l; - [], parsed_text_length, None + [], parsed_text_length | TA.WHint (loc, term) -> let term = disambiguate term status in let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term),0) in let l = List.map fst (MQ.experimental_hint ~dbd s) in let entry = `Whelp (TAPp.pp_macro_cic (TA.WHint (loc, term)), l) in mathviewer#show_uri_list ~reuse:true ~entry l; - [], parsed_text_length, None + [], parsed_text_length (* REAL macro *) | TA.Hint loc -> let s = MatitaMisc.get_proof_status status in let l = List.map fst (MQ.experimental_hint ~dbd s) in let selected = urichooser l in (match selected with - | [] -> [], parsed_text_length, None + | [] -> [], parsed_text_length | [uri] -> let ast = (TA.Executable (loc, @@ -181,7 +182,7 @@ script mac = comment parsed_text ^ "\n" ^ TAPp.pp_statement ast in - [ new_status , extra_text ], parsed_text_length, None + [ new_status , extra_text ], parsed_text_length | _ -> assert false) | TA.Check (_,term) -> let metasenv = MatitaMisc.get_proof_metasenv status in @@ -199,8 +200,8 @@ script mac = let ty,_ = CTC.type_of_aux' metasenv context term ugraph in let t_and_ty = Cic.Cast (term,ty) in mathviewer#show_entry (`Cic (t_and_ty,metasenv)); - [], parsed_text_length, None - | TA.Abort _ -> + [], parsed_text_length +(* | TA.Abort _ -> let rec go_back () = let status = script#status.proof_status in match status with @@ -215,7 +216,7 @@ script mac = | TA.Undo (_, Some i) -> [], parsed_text_length, Some (fun () -> for j = 1 to i do script#retract () done) | TA.Undo (_, None) -> [], parsed_text_length, - Some (fun () -> script#retract ()) + Some (fun () -> script#retract ()) *) (* TODO *) | TA.Quit _ -> failwith "not implemented" | TA.Print (_,kind) -> failwith "not implemented" @@ -249,13 +250,13 @@ user_goal script s = let parsed_text, parsed_text_length = text_of_loc loc in let remain_len = String.length s - parsed_text_length in let s = String.sub s parsed_text_length remain_len in - let s,len, act = + let s,len = eval_statement status mathviewer urichooser user_goal script s in (match s with | (status, text) :: tl -> - ((status, parsed_text ^ text)::tl), (parsed_text_length + len), act - | [] -> [], 0, None) + ((status, parsed_text ^ text)::tl), (parsed_text_length + len) + | [] -> [], 0) | TacticAst.Executable (loc, ex) -> let parsed_text, parsed_text_length = text_of_loc loc in eval_executable @@ -290,7 +291,7 @@ object (self) method private _advance ?statement () = let s = match statement with Some s -> s | None -> self#getFuture in MatitaLog.debug ("evaluating: " ^ first_line s ^ " ..."); - let (entries, parsed_len, post_advance_action) = + let (entries, parsed_len) = eval_statement self#status mathviewer urichooser userGoal self s in let (new_statuses, new_statements) = List.split entries in (* @@ -306,10 +307,7 @@ List.iter (fun s -> prerr_endline ("'" ^ s ^ "'")) new_statements; end; let new_text = String.concat "" new_statements in buffer#insert ~iter:start new_text; - self#moveMark (String.length new_text); - match post_advance_action with - | Some f -> f () - | _ -> () + self#moveMark (String.length new_text) method private _retract () = match statements, history with