X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=5fe955b3ea5f8124e428b0a7fd28f1815472ee26;hb=a6dd077a2b3e4d0c4395c2ee4cc2e1b6d10ab963;hp=1f18e76a6a3aebc46af710b19b85fda96acfd958;hpb=de4483296d06aac3df4da10d5401b1f97c4350ab;p=helm.git diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 1f18e76a6..5fe955b3e 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,33 @@ 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 set_whelp_query txt = + let query, arg = + try + let q = Pcre.extract ~rex:whelp_query_RE txt in + q.(1), q.(2) + with Invalid_argument _ -> failwith "Malformed Whelp query" + in + activate_combo_query arg query + in let toplevel = win#toplevel in let mathView = sequentViewer ~packing:win#scrolledBrowser#add () in let fail msg = @@ -307,8 +331,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 +377,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 +405,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 +458,9 @@ 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) -> + set_whelp_query query; + self#_loadList results); self#setEntry entry end with @@ -414,10 +469,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 +507,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 +543,46 @@ 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 + 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 (** {2 methods used by constructor only} *) @@ -583,5 +648,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