Interface reduction; code clean up.

diff --git a/matita/matita/matitaGui.ml b/matita/matita/matitaGui.ml
index 236d32f6887867e648677893493fb63fd70b9f69..d8916f7fa923e21cf11b9b25644f9628a171a360 100644 (file)
--- a/matita/matita/matitaGui.ml
+++ b/matita/matita/matitaGui.ml
@@ -825,21 +825,13 @@ class gui () =
       connect_menu_item main#newMenuItem self#newScript;
       connect_menu_item main#closeMenuItem self#closeCurrentScript;
       connect_menu_item main#showCoercionsGraphMenuItem 
-        (fun _ -> 
-          let c = MatitaMathView.cicBrowser () in
-          c#load (`About `Coercions));
+        (fun _ -> MatitaMathView.cicBrowser (Some (`About `Coercions)));
       connect_menu_item main#showHintsDbMenuItem 
-        (fun _ -> 
-          let c = MatitaMathView.cicBrowser () in
-          c#load (`About `Hints));
+        (fun _ -> MatitaMathView.cicBrowser (Some (`About `Hints)));
       connect_menu_item main#showTermGrammarMenuItem 
-        (fun _ -> 
-          let c = MatitaMathView.cicBrowser () in
-          c#load (`About `Grammar));
+        (fun _ -> MatitaMathView.cicBrowser (Some (`About `Grammar)));
       connect_menu_item main#showUnicodeTable
-        (fun _ -> 
-          let c = MatitaMathView.cicBrowser () in
-          c#load (`About `TeX));
+        (fun _ -> MatitaMathView.cicBrowser (Some (`About `TeX)));
         (* debug menu *)
       main#debugMenu#misc#hide ();
         (* HBUGS *)
@@ -862,7 +854,7 @@ class gui () =
       main#hpaneScriptSequent#set_position script_w;
       (* math view handling *)
       connect_menu_item main#newCicBrowserMenuItem (fun () ->
-        ignore(MatitaMathView.cicBrowser ()));
+        ignore(MatitaMathView.cicBrowser None));
       connect_menu_item main#increaseFontSizeMenuItem
         MatitaMisc.increase_font_size;
       connect_menu_item main#decreaseFontSizeMenuItem

diff --git a/matita/matita/matitaGuiTypes.mli b/matita/matita/matitaGuiTypes.mli
index fa2583d06d6b98299d374df8983c6390f8cfd08a..f75769fb0daccdc65168e3160db4716770e7a0f0 100644 (file)
--- a/matita/matita/matitaGuiTypes.mli
+++ b/matita/matita/matitaGuiTypes.mli
@@ -43,8 +43,3 @@ object
   method goto_sequent:
    #ApplyTransformation.status -> int -> unit (* to be called _after_ load_sequents *)
 end
-
-class type cicBrowser =
-object
-  method load: MatitaTypes.mathViewer_entry -> unit
-end

diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml
index df8b5359d98b72e54a1361960f008fe03dfc656d..a970c569f96c74ad24e3aa9048b807eac5fe58fc 100644 (file)
--- a/matita/matita/matitaMathView.ml
+++ b/matita/matita/matitaMathView.ml
@@ -633,7 +633,7 @@ let sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) ():
 =
   (new sequentsViewer ~notebook ~cicMathView ():> MatitaGuiTypes.sequentsViewer)
 
-let cicBrowser () =
+let new_cicBrowser () =
   let size = BuildTimeConf.browser_history_size in
   let rec aux history =
     let browser = new cicBrowser_impl ~history () in
@@ -651,17 +651,31 @@ let cicBrowser () =
       GdkKeysyms._W (fun () -> win#toplevel#destroy ());
 *)
     cicBrowsers := browser :: !cicBrowsers;
-    (browser :> MatitaGuiTypes.cicBrowser)
+    browser
   in
   let history = new MatitaMisc.browser_history size (`About `Blank) in
   aux history
 
+(** @param reuse if set reused last opened cic browser otherwise 
+*  opens a new one. default is false *)
+let cicBrowser ?(reuse=false) t =
+ let browser =
+  if reuse then
+   (match !cicBrowsers with [] -> new_cicBrowser () | b :: _ -> b)
+  else
+   new_cicBrowser ()
+ in
+  match t with
+     None -> ()
+   | Some t -> browser#load t
+;;
+
 let default_cicMathView () =
  let res = cicMathView ~show:true () in
   res#set_href_callback
     (Some (fun uri ->
       let uri = `NRef (NReference.reference_of_string uri) in
-       (cicBrowser ())#load uri));
+       cicBrowser (Some uri)));
   res
 
 let cicMathView_instance =
@@ -670,6 +684,7 @@ let cicMathView_instance =
 let default_sequentsViewer notebook =
   let cicMathView = cicMathView_instance () in
   sequentsViewer ~notebook ~cicMathView ()
+
 let sequentsViewer_instance =
  let already_used = ref false in
   fun notebook ->
@@ -678,20 +693,6 @@ let sequentsViewer_instance =
     (already_used := true;
      default_sequentsViewer notebook)
 
-(** @param reuse if set reused last opened cic browser otherwise 
-*  opens a new one. default is false *)
-let show_entry ?(reuse=false) t =
- let browser =
-  if reuse then
-   (match !cicBrowsers with
-       [] -> cicBrowser ()
-     | b :: _ -> (b :> MatitaGuiTypes.cicBrowser))
-  else
-   cicBrowser ()
- in
-  browser#load t
-;;
-
 let refresh_all_browsers () =
   List.iter (fun b -> b#refresh ~force:false ()) !cicBrowsers
 

diff --git a/matita/matita/matitaMathView.mli b/matita/matita/matitaMathView.mli
index 8e323ddc42aa6a35f127d70b77eac0ec0564fc53..dd1e189557ba88cb7bdba3a0b063d9d091631823 100644 (file)
--- a/matita/matita/matitaMathView.mli
+++ b/matita/matita/matitaMathView.mli
@@ -23,21 +23,16 @@
  * http://helm.cs.unibo.it/
  *)
 
-(** {2 Instances} *)
-val cicBrowser: unit -> MatitaGuiTypes.cicBrowser
-
 (** {2 To be called just once} *)
-val sequentsViewer_instance:  GPack.notebook -> MatitaGuiTypes.sequentsViewer
+val sequentsViewer_instance: GPack.notebook -> MatitaGuiTypes.sequentsViewer
 
 (** {2 Global changes} *)
-
 val refresh_all_browsers: unit -> unit  (** act on all cicBrowsers *)
 
 (** {2 Rendering in a browser} *)
-
 (** @param reuse if set reused last opened cic browser otherwise 
 *  opens a new one. default is false *)
-val show_entry: ?reuse:bool -> MatitaTypes.mathViewer_entry -> unit
+val cicBrowser: ?reuse:bool -> MatitaTypes.mathViewer_entry option -> unit
 
 (** {2 Clipboard & Selection handling} *)
 

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index 37e0f92395351c662d8031477b57ae8aadd191e3..f1b20efe5929eff2ca0cde49d2e4edf8efc01789 100644 (file)
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -125,7 +125,7 @@ let eval_nmacro include_paths (buffer : GText.buffer) status unparsed_text parse
             NotationPt.Cast (t,NotationPt.Implicit `JustOne))  
           (* XXX use the metasenv, if possible *)
       in
-      MatitaMathView.show_entry (`NCic (t,ctx,m,s));
+      MatitaMathView.cicBrowser (Some (`NCic (t,ctx,m,s)));
       [status, parsed_text], "", parsed_text_length
   | TA.NIntroGuess _loc ->
       let names_ref = ref [] in