X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=cd600f0403c4c663d18e9ad330124c8e1db63b78;hb=12cc5b2b8e7f7bb0b5e315094b008a293a4df6b1;hp=1f18e76a6a3aebc46af710b19b85fda96acfd958;hpb=de4483296d06aac3df4da10d5401b1f97c4350ab;p=helm.git diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 1f18e76a6..cd600f040 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -39,12 +39,33 @@ 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) method private script = MatitaScript.instance () end +let cicBrowsers = ref [] + +let default_font_size () = + Helm_registry.get_opt_default Helm_registry.int + ~default:BuildTimeConf.default_font_size "matita.font_size" +let current_font_size = ref ~-1 +let increase_font_size () = incr current_font_size +let decrease_font_size () = decr current_font_size +let reset_font_size () = current_font_size := default_font_size () + class clickableMathView obj = let href = Gdome.domString "href" in let xref = Gdome.domString "xref" in @@ -55,23 +76,24 @@ class clickableMathView obj = method set_href_callback f = href_callback <- f initializer + self#set_font_size !current_font_size; ignore (self#connect#selection_changed self#choose_selection); ignore (self#connect#click (fun (gdome_elt, _, _, _) -> match gdome_elt with | Some elt (* element is an hyperlink, use href_callback on it *) - when elt#hasAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href -> + when elt#hasAttributeNS ~namespaceURI:DomMisc.xlink_ns ~localName:href -> (match href_callback with | None -> () | Some f -> let uri = - elt#getAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href + elt#getAttributeNS ~namespaceURI:DomMisc.xlink_ns ~localName:href in f (uri#to_string)) | Some elt -> ignore (self#action_toggle elt) | None -> ())) method private choose_selection gdome_elt = let rec aux elt = - if elt#hasAttributeNS ~namespaceURI:Misc.helm_ns ~localName:xref then + if elt#hasAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref then self#set_selection (Some elt) else try @@ -84,6 +106,10 @@ class clickableMathView obj = match gdome_elt with | Some elt -> aux elt | None -> self#set_selection None + + method update_font_size = + self#set_font_size !current_font_size + end let clickableMathView ?hadjustment ?vadjustment ?font_size ?log_verbosity = @@ -100,14 +126,14 @@ class sequentViewer obj = inherit clickableMathView obj val mutable current_infos = None - + method get_selected_terms = let selections = self#get_selections in list_map_fail (fun node -> let xpath = ((node : Gdome.element)#getAttributeNS - ~namespaceURI:Misc.helm_ns + ~namespaceURI:DomMisc.helm_ns ~localName:(Gdome.domString "xref"))#to_string in if xpath = "" then assert false (* "ERROR: No xref found!!!" *) @@ -124,7 +150,7 @@ class sequentViewer obj = (fun node -> let xpath = ((node : Gdome.element)#getAttributeNS - ~namespaceURI:Misc.helm_ns + ~namespaceURI:DomMisc.helm_ns ~localName:(Gdome.domString "xref"))#to_string in if xpath = "" then assert false (* "ERROR: No xref found!!!" *) @@ -143,7 +169,7 @@ class sequentViewer obj = current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses); (* debug_print "load_sequent: dumping MathML to ./prova"; - ignore (Misc.domImpl#saveDocumentToFile ~name:"./prova" ~doc:mathml ()); + ignore (DomMisc.domImpl#saveDocumentToFile ~name:"./prova" ~doc:mathml ()); *) self#load_root ~root:mathml#get_documentElement end @@ -274,47 +300,99 @@ type term_source = | `String of string ] -exception Browser_failure of string - -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 +let reloadable = function + | `About `Current_proof + | `Dir _ -> + true + | _ -> false + 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:/([^/]+/)*[^/]+\\.(con|ind|var)(#xpointer\\(\\d+(/\\d+)+\\))?$" + in + let dir_RE = Pcre.regexp "^cic:((/([^/]+/)*[^/]+(/)?)|/|)$" 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 is_whelp txt = Pcre.pmatch ~rex:whelp_RE txt in + let is_uri txt = Pcre.pmatch ~rex:uri_RE txt in + let is_dir txt = Pcre.pmatch ~rex:dir_RE txt 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 = - ignore (MatitaGtkMisc.ask_confirmation ~gui:(MatitaGui.instance ()) - ~title:"Cic browser" ~msg ~cancel:false ()); + let fail message = + MatitaGtkMisc.report_error ~title:"Cic browser" ~message + ~parent:toplevel () + in + let tags = + [ "dir", GdkPixbuf.from_file (MatitaMisc.image_path "matita-folder.png"); + "obj", GdkPixbuf.from_file (MatitaMisc.image_path "matita-object.png") ] in let handle_error f = try f () - with exn -> - fail (sprintf "Uncaught exception:\n%s" (Printexc.to_string exn)) + with exn -> fail (MatitaExcPp.to_string exn) in - let handle_error' f = fun () -> handle_error f in (* used in callbacks *) + let handle_error' f = (fun () -> handle_error (fun () -> f ())) in object (self) inherit scriptAccessor + + (* Whelp bar queries *) initializer + activate_combo_query "" "locate"; + win#whelpBarComboVbox#add combo#coerce; + 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#whelpBarImage#set_file (MatitaMisc.image_path "whelp.png"); + win#mathOrListNotebook#set_show_tabs false; + win#browserForwardButton#misc#set_sensitive false; win#browserBackButton#misc#set_sensitive false; - ignore (win#browserUri#connect#activate (handle_error' (fun () -> - self#loadInput win#browserUri#text))); + ignore (win#browserUri#entry#connect#activate (handle_error' (fun () -> + self#loadInput win#browserUri#entry#text))); ignore (win#browserHomeButton#connect#clicked (handle_error' (fun () -> - self#_load (`About `Current_proof)))); + self#load (`About `Current_proof)))); ignore (win#browserRefreshButton#connect#clicked (handle_error' self#refresh)); ignore (win#browserBackButton#connect#clicked (handle_error' self#back)); @@ -330,10 +408,10 @@ 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 ()))); + handle_error (fun () -> self#loadInput (self#_getSelectedUri ())))); mathView#set_href_callback (Some (fun uri -> - handle_error (fun () -> self#_load (`Uri uri)))); + handle_error (fun () -> + self#load (`Uri (UriManager.uri_of_string uri))))); self#_load (`About `Blank); toplevel#show () @@ -341,19 +419,22 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) val mutable current_infos = None val mutable current_mathml = None - val model = new MatitaGtkMisc.stringListModel win#whelpResultTreeview + val model = + new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview + + val mutable lastDir = "" (* last loaded "directory" *) - method private _getWhelpResultTreeviewSelection () = + method private _getSelectedUri () = match model#easy_selection () with - | [u] -> u - | _ -> assert false + | [sel] when is_uri sel -> sel (* absolute URI selected *) +(* | [sel] -> win#browserUri#entry#text ^ sel |+ relative URI selected +| *) + | [sel] -> lastDir ^ sel + | _ -> assert false (** history RATIONALE * - * all operations about history are done using _historyFoo - * - * only toplevel function like load loadList loadInput can call - * _historyAdd + * All operations about history are done using _historyFoo. + * Only toplevel functions (ATM load and loadInput) call _historyAdd. *) method private _historyAdd item = @@ -380,8 +461,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method private _showList = win#mathOrListNotebook#goto_page 1 method private _showMath = win#mathOrListNotebook#goto_page 0 - - method private back () = try self#_load (self#_historyPrev ()) @@ -396,28 +475,26 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) * @param uri string *) method private _load entry = try - if entry <> current_entry || entry = `About `Current_proof then begin - (match entry with - | `About `Current_proof -> self#home () - | `About `Blank -> self#blank () - | `About `Us -> () (* TODO implement easter egg here :-] *) - | `Check term -> self#_loadCheck term - | `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); - self#setEntry entry - end - with - | UriManager.IllFormedUri uri -> fail (sprintf "invalid uri: %s" uri) - | CicEnvironment.Object_not_found uri -> - fail (sprintf "object not found: %s" (UriManager.string_of_uri uri)) - | Browser_failure msg -> fail msg - + if entry <> current_entry || reloadable entry then begin + (match entry with + | `About `Current_proof -> self#home () + | `About `Blank -> self#blank () + | `About `Us -> () (* TODO implement easter egg here :-] *) + | `Check term -> self#_loadCheck term + | `Cic (term, metasenv) -> self#_loadTermCic term metasenv + | `Dir dir -> self#_loadDir dir + | `Uri uri -> self#_loadUriManagerUri uri + | `Whelp (query, results) -> + set_whelp_query query; + self#_loadList (List.map (fun r -> "obj", + UriManager.string_of_uri r) results)); + self#setEntry entry + end + with exn -> fail (MatitaExcPp.to_string exn) 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"; @@ -445,16 +522,19 @@ 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 -> sec - | Http_getter_types.Ls_object 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 + lastDir <- dir; self#_loadList l method private setEntry entry = - win#browserUri#set_text (string_of_entry entry); - current_entry <- entry + win#browserUri#entry#set_text (string_of_entry entry); + current_entry <- entry method private _loadObj obj = self#_showMath; @@ -486,50 +566,52 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) method private _loadList l = model#list_store#clear (); - List.iter model#easy_append l; + List.iter (fun (tag, s) -> model#easy_append ~tag s) 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 - - method loadInput txt = - let add_terminating_slash s = - if s.[String.length s - 1] <> '/' then s^"/" else s - in - let is_uri = - try - ignore(Http_getter.resolve txt); true - with - | Http_getter_types.Key_not_found _ - | Http_getter_types.Unresolvable_URI _ -> false + 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 txt = strip_blanks txt in + let fix_uri txt = + UriManager.string_of_uri + (UriManager.strip_xpointer (UriManager.uri_of_string txt)) in - let entry = - if is_uri then - (`Uri txt) - else - (`Dir (add_terminating_slash txt)) - in - self#_load entry; - self#_historyAdd entry - - + 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 (UriManager.uri_of_string (fix_uri txt)) + | txt when is_dir txt -> `Dir (add_trailing_slash txt) + | txt -> + (try + entry_of_string txt + with Invalid_argument _ -> + command_error (sprintf "unsupported uri: %s" txt)) + in + self#_load entry; + self#_historyAdd entry + end + + (** {2 methods accessing underlying GtkMathView} *) + + method updateFontSize = mathView#set_font_size !current_font_size + (** {2 methods used by constructor only} *) method win = win method history = history method currentEntry = current_entry method refresh () = - if current_entry = `About `Current_proof then - self#_load (`About `Current_proof) - end + if reloadable current_entry then self#_load current_entry + end let sequentsViewer ~(notebook:GPack.notebook) ~(sequentViewer:sequentViewer) () @@ -559,8 +641,6 @@ let cicBrowser () = let history = new MatitaMisc.browser_history size (`About `Blank) in aux history -let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers - let default_sequentViewer () = sequentViewer ~show:true () let sequentViewer_instance = MatitaMisc.singleton default_sequentViewer @@ -583,5 +663,12 @@ 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 + +let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers + +let update_font_sizes () = + List.iter (fun b -> b#updateFontSize) !cicBrowsers; + (sequentViewer_instance ())#update_font_size +