1. reset of statuses simplified

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

diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml
index ec536f60ef6ea5b03beb74121ed2cc8eb07ba24b..ff381b88787df8c80503c83bcdb1a73275c0dba0 100644 (file)
--- a/matita/matita/matitaMathView.ml
+++ b/matita/matita/matitaMathView.ml
@@ -105,8 +105,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
       page2goal <- [];
       goal2page <- [];
       goal2win <- [];
-      _metasenv <- `Old []; 
-      self#script#setGoal None
+      _metasenv <- `Old []
 
     method nload_sequents : 'status. #GrafiteTypes.status as 'status -> unit
     = fun (status : #GrafiteTypes.status) ->
@@ -185,7 +184,6 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
           let goal_switch =
             try List.assoc page page2goal with Not_found -> assert false
           in
-          self#script#setGoal (Some (goal_of_switch goal_switch));
           self#render_page status ~page ~goal_switch))
 
     method private render_page:
@@ -292,7 +290,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       let module Pp = GraphvizPp.Dot in
       let filename, oc = Filename.open_temp_file "matita" ".dot" in
       let fmt = Format.formatter_of_out_channel oc in
-      let status = (get_matita_script_current ())#grafite_status in
+      let status = (get_matita_script_current ())#status in
       Pp.header 
         ~name:"Hints"
         ~graph_type:"graph"
@@ -315,7 +313,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
         ~name:"Coercions"
         ~node_attrs:["fontsize", "9"; "width", ".4"; "height", ".4"]
         ~edge_attrs:["fontsize", "10"] fmt;
-      let status = (get_matita_script_current ())#grafite_status in
+      let status = (get_matita_script_current ())#status in
       NCicCoercion.generate_dot_file status fmt;
       Pp.trailer fmt;
       Pp.raw "@." fmt;
@@ -552,19 +550,17 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       self#_showSearch
 
     method private grammar () =
-      self#_loadText (Print_grammar.ebnf_of_term self#script#grafite_status);
+      self#_loadText (Print_grammar.ebnf_of_term self#script#status);
 
     method private home () =
       self#_showMath;
-      match self#script#grafite_status#ng_mode with
-         `ProofMode ->
-           self#_loadNObj self#script#grafite_status
-           self#script#grafite_status#obj
+      match self#script#status#ng_mode with
+         `ProofMode -> self#_loadNObj self#script#status self#script#status#obj
        | _ -> self#blank ()
 
     method private _loadNReference (NReference.Ref (uri,_)) =
       let obj = NCicEnvironment.get_checked_obj uri in
-      self#_loadNObj self#script#grafite_status obj
+      self#_loadNObj self#script#status obj
 
     method private _loadDir dir = 
       let content = Http_getter.ls ~local:false dir in
@@ -594,7 +590,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
     method private _loadTermNCic term m s c =
       let d = 0 in
       let m = (0,([],c,term))::m in
-      let status = (get_matita_script_current ())#grafite_status in
+      let status = (get_matita_script_current ())#status in
       mathView#nload_sequent status m s d;
       self#_showMath
 
@@ -632,10 +628,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
         self#_load entry;
         self#_historyAdd entry
 
-      (** {2 methods accessing underlying GtkMathView} *)
-
-    method updateFontSize = mathView#set_font_size (MatitaMisc.get_current_font_size ())
-
       (** {2 methods used by constructor only} *)
 
     method win = win
@@ -684,12 +676,16 @@ let default_cicMathView () =
 let cicMathView_instance =
  MatitaMisc.singleton default_cicMathView
 
-let default_sequentsViewer () =
-  let gui = MatitaMisc.get_gui () in
+let default_sequentsViewer notebook =
   let cicMathView = cicMathView_instance () in
-  sequentsViewer ~notebook:gui#main#sequentsNotebook ~cicMathView ()
-let sequentsViewer_instance = MatitaMisc.singleton default_sequentsViewer
-
+  sequentsViewer ~notebook ~cicMathView ()
+let sequentsViewer_instance =
+ let already_used = ref false in
+  fun notebook ->
+   if !already_used then assert false
+   else
+    (already_used := true;
+     default_sequentsViewer notebook)
           
 (** @param reuse if set reused last opened cic browser otherwise 
 *  opens a new one. default is false *)
@@ -708,10 +704,6 @@ let show_entry ?(reuse=false) t =
 let refresh_all_browsers () =
   List.iter (fun b -> b#refresh ~force:false ()) !cicBrowsers
 
-let update_font_sizes () =
-  List.iter (fun b -> b#updateFontSize) !cicBrowsers;
-  (cicMathView_instance ())#update_font_size
-
 let get_math_views () =
   (cicMathView_instance ()) :: (List.map (fun b -> b#mathView) !cicBrowsers)