X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=b9affc23645e4d65ad8df81cfb306a85a7d53765;hb=84c9131c30a4a991c595f61620794b1b75a5a16d;hp=4d0eace3ae6f7d6cf6ae1ff8b66e67b3cd05ee82;hpb=94c9255e1f3095440f4d49ea1d75443a5a343185;p=helm.git diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 4d0eace3a..b9affc236 100644 --- a/helm/matita/matitaMathView.ml +++ b/helm/matita/matitaMathView.ml @@ -66,6 +66,13 @@ 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 () + (* is there any lablgtk2 constant corresponding to the left mouse button??? *) +let left_button = 1 + +let near (x1, y1) (x2, y2) = + let distance = sqrt (((x2 -. x1) ** 2.) +. ((y2 -. y1) ** 2.)) in + (distance < 4.) + class clickableMathView obj = let href = Gdome.domString "href" in let xref = Gdome.domString "xref" in @@ -78,9 +85,11 @@ class clickableMathView obj = initializer self#set_font_size !current_font_size; ignore (self#connect#selection_changed self#choose_selection); - ignore (self#connect#click (fun (gdome_elt, _, _, _) -> + ignore (self#event#connect#button_press self#button_press); + ignore (self#event#connect#button_release self#button_release); +(* ignore (self#connect#click (fun (gdome_elt, _, _, _) -> match gdome_elt with - | Some elt (* element is an hyperlink, use href_callback on it *) + | Some elt |+ element is an hyperlink, use href_callback on it +| when elt#hasAttributeNS ~namespaceURI:DomMisc.xlink_ns ~localName:href -> (match href_callback with | None -> () @@ -90,7 +99,57 @@ class clickableMathView obj = in f (uri#to_string)) | Some elt -> ignore (self#action_toggle elt) - | None -> ())) + | None -> ())) *) + + val mutable button_press_x = -1. + val mutable button_press_y = -1. + + method private button_press gdk_button = + button_press_x <- GdkEvent.Button.x gdk_button; + button_press_y <- GdkEvent.Button.y gdk_button; + false + + method private button_release gdk_button = + let button_release_x = GdkEvent.Button.x gdk_button in + let button_release_y = GdkEvent.Button.y gdk_button in + (if near (button_press_x, button_press_y) + (button_release_x, button_release_y) + then + let x = int_of_float button_press_x in + let y = int_of_float button_press_y in + (match self#get_element_at x y with + | None -> () + | Some elt -> + let namespaceURI = DomMisc.xlink_ns in + let localName = href in + if elt#hasAttributeNS ~namespaceURI ~localName then + self#invoke_href_callback + (elt#getAttributeNS ~namespaceURI ~localName)#to_string + gdk_button + else + ignore (self#action_toggle elt))); + false + + method private invoke_href_callback href_value gdk_button = + let button = GdkEvent.Button.button gdk_button in + if button = left_button then + let time = GdkEvent.Button.time gdk_button in + match href_callback with + | None -> () + | Some f -> + (match MatitaMisc.split href_value with + | [ uri ] -> f uri + | uris -> + let menu = GMenu.menu () in + List.iter + (fun uri -> + let menu_item = + GMenu.menu_item ~label:uri ~packing:menu#append () + in + ignore (menu_item#connect#activate (fun () -> f uri))) + uris; + menu#popup ~button ~time) + method private choose_selection gdome_elt = let rec aux elt = if elt#hasAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref then @@ -167,10 +226,9 @@ class sequentViewer obj = ApplyTransformation.mml_of_cic_sequent metasenv sequent in current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses); -(* - debug_print "load_sequent: dumping MathML to ./prova"; - ignore (DomMisc.domImpl#saveDocumentToFile ~name:"./prova" ~doc:mathml ()); -*) + let name = "sequent_viewer.xml" in + prerr_endline ("load_sequent: dumping MathML to ./" ^ name); + ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ()); self#load_root ~root:mathml#get_documentElement end @@ -300,8 +358,6 @@ type term_source = | `String of string ] -exception Browser_failure of string - class type cicBrowser = object method load: MatitaTypes.mathViewer_entry -> unit @@ -309,6 +365,12 @@ object method loadInput: string -> unit end +let reloadable = function + | `About `Current_proof + | `Dir _ -> + true + | _ -> false + class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) () = @@ -316,9 +378,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) let whelp_RE = Pcre.regexp "^\\s*whelp" in let uri_RE = Pcre.regexp - "^cic:/(\\w+/)*\\w+\\.(con|ind|var)(#xpointer\\(\\d+(/\\d+)+\\))?$" + "^cic:/([^/]+/)*[^/]+\\.(con|ind|var)(#xpointer\\(\\d+(/\\d+)+\\))?$" in - let dir_RE = Pcre.regexp "^cic:((/(\\w+/)*\\w+(/)?)|/|)$" 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 @@ -351,7 +413,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) let toplevel = win#toplevel in let mathView = sequentViewer ~packing:win#scrolledBrowser#add () in let fail message = - MatitaGtkMisc.report_error ~title:"Cic browser" ~message () + MatitaGtkMisc.report_error ~title:"Cic browser" ~message + ~parent:toplevel () in let tags = [ "dir", GdkPixbuf.from_file (MatitaMisc.image_path "matita-folder.png"); @@ -360,8 +423,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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 (fun () -> f ())) in object (self) @@ -403,9 +465,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) GMain.quit (); false)); ignore(win#whelpResultTreeview#connect#row_activated - ~callback:(fun _ _ -> self#loadInput (self#_getSelectedUri ()))); + ~callback:(fun _ _ -> + handle_error (fun () -> self#loadInput (self#_getSelectedUri ())))); mathView#set_href_callback (Some (fun uri -> - handle_error (fun () -> self#load (`Uri (UriManager.uri_of_string uri))))); + handle_error (fun () -> + self#load (`Uri (UriManager.uri_of_string uri))))); self#_load (`About `Blank); toplevel#show () @@ -416,10 +480,13 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) val model = new MatitaGtkMisc.taggedStringListModel tags win#whelpResultTreeview + val mutable lastDir = "" (* last loaded "directory" *) + method private _getSelectedUri () = match model#easy_selection () with | [sel] when is_uri sel -> sel (* absolute URI selected *) - | [sel] -> win#browserUri#entry#text ^ sel (* relative URI selected *) +(* | [sel] -> win#browserUri#entry#text ^ sel |+ relative URI selected +| *) + | [sel] -> lastDir ^ sel | _ -> assert false (** history RATIONALE @@ -466,25 +533,22 @@ 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 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 - | 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 () = self#_showMath; @@ -517,13 +581,15 @@ 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 s -> "dir", s - | Http_getter_types.Ls_object o -> "obj", o.Http_getter_types.uri) - content + List.fast_sort + Pervasives.compare + (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 - if l = [] then raise (Browser_failure "no such directory"); + lastDir <- dir; self#_loadList l method private setEntry entry = @@ -548,6 +614,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) XmlDiff.update_dom ~from:current_mathml mathml; mathView#thaw | _ -> + let name = "cic_browser.xml" in + prerr_endline ("cic_browser: dumping MathML to ./" ^ name); + ignore (DomMisc.domImpl#saveDocumentToFile ~name ~doc:mathml ()); mathView#load_root ~root:mathml#get_documentElement; current_mathml <- Some mathml); @@ -587,7 +656,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) (try entry_of_string txt with Invalid_argument _ -> - raise (Browser_failure (sprintf "unsupported uri: %s" txt))) + command_error (sprintf "unsupported uri: %s" txt)) in self#_load entry; self#_historyAdd entry @@ -603,10 +672,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) 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) ()