X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.ml;h=e572f0982f80d7b6cb1d5d2ddf9b0697f05999d6;hb=6187b40af194fb960d91653682a0eb2096f20f3b;hp=626e456349752d91c84ed3d3d6f2b86df5143f9a;hpb=394bf3a0ca050cf97b1f318363e2e353f67141ad;p=helm.git diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml index 626e45634..e572f0982 100644 --- 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