From aac382f935bc72578119fa7ff9f53c3b649dd0dd Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 17 May 2005 15:24:48 +0000 Subject: [PATCH] fixed whelp bar --- helm/matita/matitaGui.ml | 24 ------- helm/matita/matitaMathView.ml | 112 +++++++++++++++++++++++++-------- helm/matita/matitaMathView.mli | 2 +- helm/matita/matitaMisc.ml | 15 +++-- helm/matita/matitaScript.ml | 111 +++++++++++++++++--------------- helm/matita/matitaTypes.ml | 2 +- 6 files changed, 157 insertions(+), 109 deletions(-) diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 5045f36d1..f3b531fb2 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -254,30 +254,6 @@ class gui () = method newBrowserWin () = let win = new browserWin () in - win#whelpImage2#set_file "icons/whelp.png"; - win#whelpBarToggleButton#set_active false; - win#whelpBarBox#misc#hide (); - win#mathOrListNotebook#set_show_tabs false; - connect_toggle_button win#whelpBarToggleButton - (fun () -> - if win#whelpBarToggleButton#active then - win#whelpBarBox#misc#show () - else - win#whelpBarBox#misc#hide ()); - let queries = ["Locate";"Hint";"Match";"Elim";"Instance"] in - let combo,(combo_store,combo_column) = - GEdit.combo_box_text ~strings:queries () - in - combo#set_active 0; - win#comboVbox#add (combo :> GObj.widget); - let start_query () = - let query = String.lowercase (List.nth queries combo#active) in - let input = win#queryInputText#text in - let statement = "whelp " ^ query ^ " " ^ input ^ "." in - (MatitaScript.instance ())#advance ~statement () - in - ignore(win#queryInputText#connect#activate ~callback:start_query); - ignore(combo#connect#changed ~callback:start_query); win#check_widgets (); win diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 1f18e76a6..df10be563 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -281,7 +281,7 @@ let cicBrowsers = ref [] class type cicBrowser = object method load: MatitaTypes.mathViewer_entry -> unit - method loadList: string list -> MatitaTypes.mathViewer_entry-> unit + (* method loadList: string list -> MatitaTypes.mathViewer_entry-> unit *) method loadInput: string -> unit end @@ -289,9 +289,24 @@ 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 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 let gui = MatitaGui.instance () in let win = gui#newBrowserWin () in + let queries = ["Locate";"Hint";"Match";"Elim";"Instance"] in + let combo,_ = GEdit.combo_box_text ~strings:queries () in + let activate_combo_query input q = + let q' = String.lowercase q in + let rec aux i = function + | [] -> failwith ("Whelp query '" ^ q ^ "' not found") + | h::_ when String.lowercase h = q' -> i + | _::tl -> aux (i+1) tl + in + combo#set_active (aux 0 queries); + win#queryInputText#set_text input + in let toplevel = win#toplevel in let mathView = sequentViewer ~packing:win#scrolledBrowser#add () in let fail msg = @@ -307,8 +322,31 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) let handle_error' f = fun () -> handle_error f in (* used in callbacks *) object (self) inherit scriptAccessor + + (* Whelp bar queries *) initializer + activate_combo_query "" "locate"; + win#comboVbox#add (combo :> GObj.widget); + let start_query () = + let query = String.lowercase (List.nth queries combo#active) in + let input = win#queryInputText#text in + let statement = "whelp " ^ query ^ " " ^ input ^ "." in + (MatitaScript.instance ())#advance ~statement () + in + ignore(win#queryInputText#connect#activate ~callback:start_query); + ignore(combo#connect#changed ~callback:start_query); + win#whelpImage2#set_file "icons/whelp.png"; + win#whelpBarToggleButton#set_active false; + win#whelpBarBox#misc#hide (); + win#mathOrListNotebook#set_show_tabs false; + MatitaGtkMisc.connect_toggle_button win#whelpBarToggleButton + (fun () -> + if win#whelpBarToggleButton#active then + win#whelpBarBox#misc#show () + else + win#whelpBarBox#misc#hide ()); + win#browserForwardButton#misc#set_sensitive false; win#browserBackButton#misc#set_sensitive false; ignore (win#browserUri#connect#activate (handle_error' (fun () -> @@ -330,8 +368,14 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) false)); ignore(win#whelpResultTreeview#connect#row_activated ~callback:(fun _ _ -> - let old = win#browserUri#text in - self#loadInput (old ^ self#_getWhelpResultTreeviewSelection ()))); + let selection = self#_getWhelpResultTreeviewSelection () in + let txt = + if String.sub selection 0 5 = "cic:/" then + selection + else + win#browserUri#text ^ selection + in + self#loadInput txt)); mathView#set_href_callback (Some (fun uri -> handle_error (fun () -> self#_load (`Uri uri)))); self#_load (`About `Blank); @@ -352,7 +396,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) * * all operations about history are done using _historyFoo * - * only toplevel function like load loadList loadInput can call + * only toplevel function like load loadInput can call * _historyAdd *) @@ -405,7 +449,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) | `Cic (term, metasenv) -> self#_loadTermCic term metasenv | `Dir dir -> self#_loadDir dir | `Uri uri -> self#_loadUriManagerUri (UriManager.uri_of_string uri) - | `Whelp (query, results) -> self#loadList results entry); + | `Whelp (query, results) -> self#_loadList results); self#setEntry entry end with @@ -414,10 +458,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) fail (sprintf "object not found: %s" (UriManager.string_of_uri uri)) | Browser_failure msg -> fail msg - method private blank () = - mathView#load_root (MatitaMisc.empty_mathml ())#get_documentElement; - self#_showMath + self#_showMath; + mathView#load_root (MatitaMisc.empty_mathml ())#get_documentElement method private _loadCheck term = failwith "not implemented _loadCheck"; @@ -453,8 +496,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) self#_loadList l method private setEntry entry = - win#browserUri#set_text (string_of_entry entry); - current_entry <- entry + win#browserUri#set_text (string_of_entry entry); + current_entry <- entry method private _loadObj obj = self#_showMath; @@ -489,35 +532,50 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) List.iter model#easy_append l; self#_showList - (** { public methods } *) + (** { public methods, all must call _load!! } *) method load uri = handle_error (fun () -> self#_load uri); self#_historyAdd uri - method loadList l entry = - self#_loadList l; - 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 s.[String.length s - 1] <> '/' then s^"/" else 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 = + let is_uri txt = try - ignore(Http_getter.resolve txt); true + 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 _ -> false + | UriManager.IllFormedUri u -> failwith ("Malformed URI '" ^ u ^ "'") in - let entry = - if is_uri then - (`Uri txt) - else - (`Dir (add_terminating_slash txt)) - in - self#_load entry; - self#_historyAdd entry + let is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in + if is_whelp txt then + begin + let q = Pcre.extract ~rex:whelp_query_RE txt in + let query, arg = + try + q.(1), q.(2) + with Invalid_argument _ -> failwith "Malformed Whelp query" + in + activate_combo_query arg query; + (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 (** {2 methods used by constructor only} *) @@ -583,5 +641,5 @@ let mathViewer () = method show_entry ?(reuse=false) t = (self#get_browser reuse)#load t method show_uri_list ?(reuse=false) ~entry l = - (self#get_browser reuse)#loadList l entry + (self#get_browser reuse)#load entry end diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli index 1dc3dabe8..aa9d38ded 100644 --- a/helm/matita/matitaMathView.mli +++ b/helm/matita/matitaMathView.mli @@ -63,7 +63,7 @@ exception Browser_failure of string class type cicBrowser = object method load: MatitaTypes.mathViewer_entry -> unit - method loadList: string list -> MatitaTypes.mathViewer_entry -> unit + (* method loadList: string list -> MatitaTypes.mathViewer_entry -> unit *) method loadInput: string -> unit end diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml index e1c55feb2..07143db99 100644 --- a/helm/matita/matitaMisc.ml +++ b/helm/matita/matitaMisc.ml @@ -139,12 +139,15 @@ class ['a] browser_history ?memento size init = if cur = size then cur <- 0; data.(cur) method add (e:'a) = - cur <- cur + 1; - if cur = size then cur <- 0; - if cur = tl then tl <- tl + 1; - if tl = size then tl <- 0; - hd <- cur; - data.(cur) <- e + if e <> data.(cur) then + begin + cur <- cur + 1; + if cur = size then cur <- 0; + if cur = tl then tl <- tl + 1; + if tl = size then tl <- 0; + hd <- cur; + data.(cur) <- e + end method load (data', hd', tl', cur') = assert (Array.length data = Array.length data'); hd <- hd'; tl <- tl'; cur <- cur'; diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml index fed62fbb3..9842ffdce 100644 --- a/helm/matita/matitaScript.ml +++ b/helm/matita/matitaScript.ml @@ -101,18 +101,68 @@ let eval_with_engine status user_goal parsed_text st = new_text in [ new_status, new_text ], parsed_text_length + +let disambiguate term status = + let module MD = MatitaDisambiguator in + let dbd = MatitaDb.instance () in + let metasenv = MatitaMisc.get_proof_metasenv status in + let context = MatitaMisc.get_proof_context status in + let aliases = MatitaMisc.get_proof_aliases status in + let interps = MD.disambiguate_term dbd context metasenv aliases term in + match interps with + | [_,_,x,_] -> x + | _ -> assert false let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text mac = let module TA = TacticAst in let module TAPp = TacticAstPp in let module MQ = MetadataQuery in - let module MD = MatitaDisambiguator in let module MDB = MatitaDb in + let module CTC = CicTypeChecker in + let module CU = CicUniv in let parsed_text_length = String.length parsed_text in + let dbd = MatitaDb.instance () in match mac with + (* WHELP's stuff *) + | TA.WMatch (loc, term) -> + let term = disambiguate term status in + 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 + | 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 + | 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 + | TA.WElim (loc, term) -> + let term = disambiguate term status in + let uri = + match term with + | Cic.MutInd (uri,n,_) -> UriManager.string_of_uriref (uri,[n]) + | _ -> failwith "Not a MutInd" + in + 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 + | 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 + (* REAL macro *) | TA.Hint loc -> let s = MatitaMisc.get_proof_status status in - let l = List.map fst (MQ.experimental_hint ~dbd:(MDB.instance ()) s) in + let l = List.map fst (MQ.experimental_hint ~dbd s) in let selected = urichooser l in (match selected with | [] -> [], parsed_text_length @@ -130,62 +180,23 @@ let eval_macro status (mathviewer:MatitaTypes.mathViewer) urichooser parsed_text in [ new_status , extra_text ],parsed_text_length | _ -> assert false) - | TA.Match (_,term) -> - let dbd = MatitaDb.instance () in + | TA.Check (_,term) -> let metasenv = MatitaMisc.get_proof_metasenv status in let context = MatitaMisc.get_proof_context status in let aliases = MatitaMisc.get_proof_aliases status in - let (_env,_metasenv,term,_graph) = - let interps = - MD.disambiguate_term dbd context metasenv aliases term - in + let interps = + MatitaDisambiguator.disambiguate_term + dbd context metasenv aliases term + in + let _, metasenv , term, ugraph = match interps with | [x] -> x | _ -> assert false in - let results = MetadataQuery.match_term ~dbd:dbd term in - mathviewer#show_uri_list ~reuse:true ~entry:(`Whelp ("match", results)) - results; - [], parsed_text_length - | TA.Instance (_,term) -> - let dbd = MatitaDb.instance () in - let metasenv = MatitaMisc.get_proof_metasenv status in - let context = MatitaMisc.get_proof_context status in - let aliases = MatitaMisc.get_proof_aliases status in - let (_env,_metasenv,term,_graph) = - let interps = - MD.disambiguate_term dbd context metasenv aliases term - in - match interps with - | [x] -> x - | _ -> assert false - in - let results = MetadataQuery.instance ~dbd term in - mathviewer#show_uri_list ~reuse:true - ~entry:(`Whelp ("instance", results)) results; - [], parsed_text_length - - - | TA.Check (_,t) -> - let metasenv = MatitaMisc.get_proof_metasenv status in - let context = MatitaMisc.get_proof_context status in - let aliases = MatitaMisc.get_proof_aliases status in - let db = MatitaDb.instance () in - let (_env,_metasenv,term,_graph) = - let interps = - MD.disambiguate_term db context metasenv aliases t - in - match interps with - | [x] -> x - | _ -> assert false - in - let ty,_ = - CicTypeChecker.type_of_aux' metasenv context term - CicUniv.empty_ugraph - in + 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 + mathviewer#show_entry (`Cic (t_and_ty,metasenv)); + [], parsed_text_length | TA.Quit _ -> failwith "not implemented quit" | _ -> failwith "not implemented" diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index f5ec78ee0..9b100ca71 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -167,7 +167,7 @@ let string_of_entry = function | `Check _ -> "check:" | `Cic (_, _) -> "term:" | `Dir uri | `Uri uri -> uri - | `Whelp (query, _) -> sprintf "whelp:%s" query + | `Whelp (query, _) -> query class type mathViewer = object -- 2.39.2