Implemented standard semantics of Load in MTI: loading a file when the current

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

diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml
index e00e4fdc5107995bce576f8c0f030c6d524c5821..2a17d938b9d74d0017776db845430ec5e1f5f73f 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:
@@ -680,12 +678,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 *)