0. core_notation.ma splitted into coq.moo and core_notation.moo

[helm.git] / helm / matita / matitaMathView.ml

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 13035b02b5ca8be6e57ab626f7551796fabf0728..481b8fd6c8c58e8dd528810de2490bb5f09aa368 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -519,12 +519,6 @@ type term_source =
   | `String of string
   ]
 
-let reloadable = function
-  | `About `Current_proof
-  | `Dir _ ->
-      true
-  | _ -> false
-
 class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
   ()
 =
@@ -605,7 +599,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       ignore (win#browserHomeButton#connect#clicked (handle_error' (fun () ->
         self#load (`About `Current_proof))));
       ignore (win#browserRefreshButton#connect#clicked
-        (handle_error' self#refresh));
+        (handle_error' (self#refresh ~force:true)));
       ignore (win#browserBackButton#connect#clicked (handle_error' self#back));
       ignore (win#browserForwardButton#connect#clicked
         (handle_error' self#forward));
@@ -685,9 +679,10 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
 
       (* loads a uri which can be a cic uri or an about:* uri
       * @param uri string *)
-    method private _load entry =
+    method private _load ?(force=false) entry =
       try
-        if entry <> current_entry || reloadable entry then begin
+       if entry <> current_entry || entry = `About `Current_proof || force then
+        begin
           (match entry with
           | `About `Current_proof -> self#home ()
           | `About `Blank -> self#blank ()
@@ -808,8 +803,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     method win = win
     method history = history
     method currentEntry = current_entry
-    method refresh () =
-      if reloadable current_entry then self#_load current_entry
+    method refresh ~force () = self#_load ~force current_entry
 
   end
   
@@ -864,7 +858,8 @@ let mathViewer () =
       (self#get_browser reuse)#load entry
   end
 
-let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers
+let refresh_all_browsers () =
+ List.iter (fun b -> b#refresh ~force:false ()) !cicBrowsers
 
 let update_font_sizes () =
   List.iter (fun b -> b#updateFontSize) !cicBrowsers;