X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=b9affc23645e4d65ad8df81cfb306a85a7d53765;hb=84c9131c30a4a991c595f61620794b1b75a5a16d;hp=1cb23366a2102ed820990e6e4a9dc87999655a1c;hpb=8631b0d6a32380ceb540fdb31ccea35ed8c7af18;p=helm.git

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 1cb23366a..b9affc236 100644
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -56,6 +56,23 @@ 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 ()
+
+  (* 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
@@ -66,23 +83,76 @@ 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, _, _, _) ->
+      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 *)
-          when elt#hasAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href ->
+        | 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 -> ()
             | 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 -> ()))
+        | 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:Misc.helm_ns ~localName:xref then
+        if elt#hasAttributeNS ~namespaceURI:DomMisc.helm_ns ~localName:xref then
           self#set_selection (Some elt)
         else
           try
@@ -95,6 +165,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 =
@@ -111,14 +185,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!!!" *)
@@ -135,7 +209,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!!!" *)
@@ -152,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 (Misc.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
 
@@ -285,10 +358,6 @@ type term_source =
   | `String of string
   ]
 
-exception Browser_failure of string
-
-let cicBrowsers = ref []
-
 class type cicBrowser =
 object
   method load: MatitaTypes.mathViewer_entry -> unit
@@ -296,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)
   ()
 =
@@ -303,12 +378,15 @@ 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
+  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
@@ -334,9 +412,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   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");
@@ -345,10 +423,9 @@ 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 f in  (* used in callbacks *)
+  let handle_error' f = (fun () -> handle_error (fun () -> f ())) in
   object (self)
     inherit scriptAccessor
     
@@ -356,7 +433,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
 
     initializer
       activate_combo_query "" "locate";
-      win#comboVbox#add (combo :> GObj.widget);
+      win#whelpBarComboVbox#add combo#coerce;
       let start_query () = 
         let query = String.lowercase (List.nth queries combo#active) in
         let input = win#queryInputText#text in
@@ -365,23 +442,15 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       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#whelpBarImage#set_file (MatitaMisc.image_path "whelp.png");
       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 () ->
-        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));
@@ -397,21 +466,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
         false));
       ignore(win#whelpResultTreeview#connect#row_activated 
         ~callback:(fun _ _ ->
-          let selection = self#_getWhelpResultTreeviewSelection () in
-          let is_cic s =
-            try
-              String.sub s 0 5 = "cic:/"
-            with Invalid_argument _ -> false
-          in
-          let txt = 
-            if is_cic selection then
-              selection
-            else
-              win#browserUri#text ^ selection 
-          in
-          self#loadInput txt));
+          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 ()
 
@@ -419,21 +477,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
 
-    method private _getWhelpResultTreeviewSelection () =
+    val mutable lastDir = ""  (* last loaded "directory" *)
+
+    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 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 = 
@@ -460,8 +519,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 ())
@@ -476,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 (UriManager.uri_of_string uri)
-            | `Whelp (query, results) -> 
-                set_whelp_query query;
-                self#_loadList (List.map (fun r -> "obj", 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;
@@ -527,16 +581,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 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
+      lastDir <- dir;
       self#_loadList l
 
     method private setEntry entry =
-      win#browserUri#set_text (string_of_entry entry);
+      win#browserUri#entry#set_text (string_of_entry entry);
       current_entry <- entry
 
     method private _loadObj obj =
@@ -557,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);
 
@@ -580,9 +640,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     (**  this is what the browser does when you enter a string an hit enter *)
     method loadInput txt =
       let txt = strip_blanks txt 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 fix_uri txt =
         UriManager.string_of_uri
           (UriManager.strip_xpointer (UriManager.uri_of_string txt))
@@ -593,24 +650,31 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       end else begin
         let entry =
           match txt with
-          | txt when is_uri txt -> `Uri (fix_uri txt)
+          | txt when is_uri txt -> `Uri (UriManager.uri_of_string (fix_uri txt))
           | txt when is_dir txt -> `Dir (add_trailing_slash txt)
-          | _ -> raise (Browser_failure (sprintf "unsupported uri: %s" 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) ()
@@ -640,8 +704,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
 
@@ -666,3 +728,10 @@ let mathViewer () =
     method show_uri_list ?(reuse=false) ~entry l =
       (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
+