From 8631b0d6a32380ceb540fdb31ccea35ed8c7af18 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 8 Jun 2005 16:53:28 +0000 Subject: [PATCH] rewritten cicBrowser handling of uri text entry, still some issued with browser history --- helm/matita/matitaEngine.ml | 4 +- helm/matita/matitaMathView.ml | 89 ++++++++++++++++++---------------- helm/matita/matitaMathView.mli | 1 - 3 files changed, 48 insertions(+), 46 deletions(-) diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 6ca720830..3c141126d 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -25,7 +25,8 @@ let tactic_of_ast = function PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) () | TacticAst.Intros (_, Some num, names) -> (* TODO Zack implement intros length *) - PrimitiveTactics.intros_tac ~howmany:num ~mk_fresh_name_callback:(namer_of names) () + PrimitiveTactics.intros_tac ~howmany:num + ~mk_fresh_name_callback:(namer_of names) () | TacticAst.Reflexivity _ -> Tactics.reflexivity | TacticAst.Assumption _ -> Tactics.assumption | TacticAst.Contradiction _ -> Tactics.contradiction @@ -335,7 +336,6 @@ let eval_command status cmd = UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con") in let metasenv = MatitaMisc.get_proof_metasenv status in - debug_print ("XXXXXXXXXX" ^ CicPp.ppterm body); let (body_type, ugraph) = CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph in diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 6db20400e..1cb23366a 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -39,6 +39,17 @@ let list_map_fail f = in aux +let add_trailing_slash = + let rex = Pcre.regexp "/$" in + fun s -> + if Pcre.pmatch ~rex s then s + else s ^ "/" + +let strip_blanks = + let rex = Pcre.regexp "^\\s*([^\\s]*)\\s*$" in + fun s -> + (Pcre.extract ~rex s).(1) + (** inherit from this class if you want to access current script *) class scriptAccessor = object (self) @@ -290,6 +301,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) = let term_RE = Pcre.regexp "^term:(.*)" in let whelp_RE = Pcre.regexp "^\\s*whelp" in + let uri_RE = + Pcre.regexp + "^cic:/(\\w+/)*\\w+\\.(con|ind|var)(#xpointer\\(\\d+(/\\d+)+\\))?$" + in + let dir_RE = Pcre.regexp "^cic:((/(\\w+/)*\\w+(/)?)|/|)$" in let whelp_query_RE = Pcre.regexp "^\\s*whelp\\s+([^\\s]+)\\s+(.*)$" in let trailing_slash_RE = Pcre.regexp "/$" in let has_xpointer_RE = Pcre.regexp "#xpointer\\(\\d+/\\d+(/\\d+)?\\)$" in @@ -510,10 +526,12 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method private _loadDir dir = let content = Http_getter.ls dir in - let l = List.map (function - | Http_getter_types.Ls_section sec -> "dir", sec - | Http_getter_types.Ls_object obj -> "obj", obj.Http_getter_types.uri - ) content + let l = + List.map + (function + | Http_getter_types.Ls_section s -> "dir", s + | Http_getter_types.Ls_object o -> "obj", o.Http_getter_types.uri) + content in self#_loadList l @@ -556,48 +574,33 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) (** { public methods, all must call _load!! } *) - method load uri = - handle_error (fun () -> self#_load uri); - self#_historyAdd uri + method load entry = + handle_error (fun () -> self#_load entry; self#_historyAdd entry) (** this is what the browser does when you enter a string an hit enter *) - method loadInput txt = - let add_terminating_slash s = - if not(Pcre.pmatch ~rex:trailing_slash_RE s) && - not(Pcre.pmatch ~rex:has_xpointer_RE s) then s^"/" else s - in - let is_uri txt = - try - let u = UriManager.strip_xpointer (UriManager.uri_of_string txt) in - ignore (Http_getter.resolve' u); - true - with - | Http_getter_types.Key_not_found _ - | Http_getter_types.Unresolvable_URI _ - | UriManager.IllFormedUri ("cic:/" | "cic:") -> false - | UriManager.IllFormedUri u -> failwith ("Malformed URI '" ^ u ^ "'") - in + method loadInput txt = + let txt = strip_blanks txt in let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in - if is_whelp txt then - begin - set_whelp_query txt; - - - (MatitaScript.instance ())#advance ~statement:(txt^".") () - end - else - begin - let entry = - if is_uri txt then - (`Uri txt) - else - (`Dir (add_terminating_slash txt)) - in - self#_load entry; - self#_historyAdd entry - end - - + let is_uri txt = Pcre.pmatch ~rex:uri_RE txt in + let is_dir txt = Pcre.pmatch ~rex:dir_RE txt in + let fix_uri txt = + UriManager.string_of_uri + (UriManager.strip_xpointer (UriManager.uri_of_string txt)) + in + if is_whelp txt then begin + set_whelp_query txt; + (MatitaScript.instance ())#advance ~statement:(txt ^ ".") () + end else begin + let entry = + match txt with + | txt when is_uri txt -> `Uri (fix_uri txt) + | txt when is_dir txt -> `Dir (add_trailing_slash txt) + | _ -> raise (Browser_failure (sprintf "unsupported uri: %s" txt)) + in + self#_load entry; + self#_historyAdd entry + end + (** {2 methods used by constructor only} *) method win = win diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli index aa9d38ded..b11befe4e 100644 --- a/helm/matita/matitaMathView.mli +++ b/helm/matita/matitaMathView.mli @@ -59,7 +59,6 @@ class type sequentsViewer = exception Browser_failure of string - class type cicBrowser = object method load: MatitaTypes.mathViewer_entry -> unit -- 2.39.2