snapshot, notably:

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

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 626e456349752d91c84ed3d3d6f2b86df5143f9a..e572f0982f80d7b6cb1d5d2ddf9b0697f05999d6 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -265,11 +265,7 @@ exception Browser_failure of string
 
 let cicBrowsers = ref []
 
-class cicBrowser 
-  ~(disambiguator:MatitaTypes.disambiguator)
-  ~(history:string MatitaMisc.history)
-  ()
-=
+class cicBrowser ~(history:string MatitaMisc.history) () =
   let term_RE = Pcre.regexp "^term:(.*)" in
   let gui = MatitaGui.instance () in
   let win = gui#newBrowserWin () in
@@ -310,6 +306,7 @@ class cicBrowser
       self#_loadUri ~add_to_history:false blank_uri;
       toplevel#show ();
 
+    val disambiguator = MatitaDisambiguator.instance ()
     val currentProof = MatitaProof.instance ()
 
     val mutable current_uri = ""
@@ -426,10 +423,10 @@ let sequents_viewer ~(notebook:GPack.notebook)
 =
   new sequents_viewer ~notebook ~sequent_viewer ~set_goal ()
 
-let cicBrowser ~disambiguator () =
+let cicBrowser () =
   let size = BuildTimeConf.browser_history_size in
   let rec aux history =
-    let browser = new cicBrowser ~disambiguator ~history () in
+    let browser = new cicBrowser ~history () in
     let win = browser#win in
     ignore (win#browserNewButton#connect#clicked (fun () ->
       let history =
@@ -450,12 +447,12 @@ let cicBrowser ~disambiguator () =
 
 let refresh_all_browsers () = List.iter (fun b -> b#refresh ()) !cicBrowsers
 
-class mathViewer ~disambiguator =
+class mathViewer =
   object
     method checkTerm (src:MatitaTypes.term_source) =
-      let browser = cicBrowser ~disambiguator () in
-      browser#loadTerm src
+      (cicBrowser ())#loadTerm src
   end
 
-let mathViewer ~disambiguator () = new mathViewer ~disambiguator
+let mathViewer () = new mathViewer
+let instance = MatitaMisc.singleton mathViewer