snapshot, notably:

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

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 7bf464a9d8390b8fea4783e6cd93220a1a4398af..626e456349752d91c84ed3d3d6f2b86df5143f9a 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -267,7 +267,6 @@ let cicBrowsers = ref []
 
 class cicBrowser 
   ~(disambiguator:MatitaTypes.disambiguator)
-  ~(currentProof:MatitaTypes.currentProof)
   ~(history:string MatitaMisc.history)
   ()
 =
@@ -286,24 +285,33 @@ class cicBrowser
     with exn ->
       fail (sprintf "Uncaught exception:\n%s" (Printexc.to_string exn))
   in
+  let handle_error' f = fun () -> handle_error f in  (* used in callbacks *)
   object (self)
     initializer
-      ignore (win#browserUri#connect#activate (fun () ->
-        self#_loadUri win#browserUri#text));
-      ignore (win#browserHomeButton#connect#clicked (fun () ->
-        self#_loadUri current_proof_uri));
-      ignore (win#browserRefreshButton#connect#clicked self#refresh);
-      ignore (win#browserBackButton#connect#clicked self#back);
-      ignore (win#browserForwardButton#connect#clicked self#forward);
+      ignore (win#browserUri#connect#activate (handle_error' (fun () ->
+        self#_loadUri win#browserUri#text)));
+      ignore (win#browserHomeButton#connect#clicked (handle_error' (fun () ->
+        self#_loadUri current_proof_uri)));
+      ignore (win#browserRefreshButton#connect#clicked
+        (handle_error' self#refresh));
+      ignore (win#browserBackButton#connect#clicked (handle_error' self#back));
+      ignore (win#browserForwardButton#connect#clicked
+        (handle_error' self#forward));
       ignore (win#toplevel#event#connect#delete (fun _ ->
         let my_id = Oo.id self in
         cicBrowsers := List.filter (fun b -> Oo.id b <> my_id) !cicBrowsers;
+        if !cicBrowsers = [] &&
+          Helm_registry.get "matita.mode" = "cicbrowser"
+        then
+          GMain.quit ();
         false));
       mathView#set_href_callback (Some (fun uri ->
         handle_error (fun () -> self#_loadUri (UriManager.string_of_uri uri))));
       self#_loadUri ~add_to_history:false blank_uri;
       toplevel#show ();
 
+    val currentProof = MatitaProof.instance ()
+
     val mutable current_uri = ""
     val mutable current_infos = None
     val mutable current_mathml = None
@@ -418,10 +426,10 @@ let sequents_viewer ~(notebook:GPack.notebook)
 =
   new sequents_viewer ~notebook ~sequent_viewer ~set_goal ()
 
-let cicBrowser ~disambiguator ~currentProof () =
+let cicBrowser ~disambiguator () =
   let size = BuildTimeConf.browser_history_size in
   let rec aux history =
-    let browser = new cicBrowser ~disambiguator ~currentProof ~history () in
+    let browser = new cicBrowser ~disambiguator ~history () in
     let win = browser#win in
     ignore (win#browserNewButton#connect#clicked (fun () ->
       let history =
@@ -442,13 +450,12 @@ let cicBrowser ~disambiguator ~currentProof () =
 
 let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers
 
-class mathViewer ~disambiguator ~currentProof =
+class mathViewer ~disambiguator =
   object
     method checkTerm (src:MatitaTypes.term_source) =
-      let browser = cicBrowser ~disambiguator ~currentProof () in
+      let browser = cicBrowser ~disambiguator () in
       browser#loadTerm src
   end
 
-let mathViewer ~disambiguator ~currentProof () =
-  new mathViewer ~disambiguator ~currentProof
+let mathViewer ~disambiguator () = new mathViewer ~disambiguator