X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaMathView.ml;h=723170fa50812cc9b510b21c6e3ab0fc07348d72;hb=153b6f35ae08d0904f8fec079133ad3ca1186544;hp=5b40bb4195ed2795b1dd6b2cbc563b34d38172e9;hpb=4f5afdc73a5331357c3410858d5202a98832e59b;p=helm.git

diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml
index 5b40bb419..723170fa5 100644
--- a/matita/matita/matitaMathView.ml
+++ b/matita/matita/matitaMathView.ml
@@ -34,12 +34,6 @@ open CicMathView
 
 module Stack = Continuationals.Stack
 
-(** inherit from this class if you want to access current script *)
-class scriptAccessor =
-object (self)
-  method private script = get_matita_script_current ()
-end
-
 let cicBrowsers = ref []
 
 let tab_label meta_markup =
@@ -57,8 +51,6 @@ let goal_of_switch = function Stack.Open g | Stack.Closed g -> g
 
 class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
   object (self)
-    inherit scriptAccessor
-
     method cicMathView = cicMathView  (** clickableMathView accessor *)
 
     val mutable pages = 0
@@ -66,7 +58,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
     val mutable page2goal = []  (* associative list: page no -> goal no *)
     val mutable goal2page = []  (* the other way round *)
     val mutable goal2win = []   (* associative list: goal no -> scrolled win *)
-    val mutable _metasenv = `Old []
+    val mutable _metasenv = [],[]
     val mutable scrolledWin: GBin.scrolled_window option = None
       (* scrolled window to which the sequentViewer is currently attached *)
     val logo = (GMisc.image
@@ -105,12 +97,12 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
       page2goal <- [];
       goal2page <- [];
       goal2win <- [];
-      _metasenv <- `Old []
+      _metasenv <- [],[]
 
     method nload_sequents : 'status. #GrafiteTypes.status as 'status -> unit
     = fun (status : #GrafiteTypes.status) ->
      let _,_,metasenv,subst,_ = status#obj in
-      _metasenv <- `New (metasenv,subst);
+      _metasenv <- metasenv,subst;
       pages <- 0;
       let win goal_switch =
         let w =
@@ -119,16 +111,21 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
         in
         let reparent () =
           scrolledWin <- Some w;
-          match cicMathView#misc#parent with
-          | None -> w#add cicMathView#coerce
-          | Some parent ->
-             let parent =
-              match cicMathView#misc#parent with
-                 None -> assert false
-               | Some p -> GContainer.cast_container p
-             in
-              parent#remove cicMathView#coerce;
-              w#add cicMathView#coerce
+          (match cicMathView#misc#parent with
+            | None -> ()
+            | Some parent ->
+               let parent =
+                match cicMathView#misc#parent with
+                   None -> assert false
+                 | Some p -> GContainer.cast_container p
+               in
+                parent#remove cicMathView#coerce);
+          w#add cicMathView#coerce;
+          ignore (w#vadjustment#set_value
+           (w#vadjustment#upper -. w#vadjustment#page_size));
+          ignore (w#vadjustment#connect#changed (fun _ ->
+            w#vadjustment#set_value
+             (w#vadjustment#upper -. w#vadjustment#page_size)))
         in
         goal2win <- (goal_switch, reparent) :: goal2win;
         w#coerce
@@ -192,10 +189,8 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
      = fun status ~page ~goal_switch ->
       (match goal_switch with
       | Stack.Open goal ->
-         (match _metasenv with
-             `Old menv -> assert false (* MATITA 1.0 *)
-           | `New (menv,subst) ->
-               cicMathView#nload_sequent status menv subst goal)
+         let menv,subst = _metasenv in
+          cicMathView#nload_sequent status menv subst goal
       | Stack.Closed goal ->
           let root = Lazy.force closed_goal_mathml in
           cicMathView#load_root ~root);
@@ -328,8 +323,6 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       HExtlib.safe_remove filename
   in
   object (self)
-    inherit scriptAccessor
-    
     val mutable gviz_uri = NReference.reference_of_string "cic:/dummy.dec";
 
     val dep_contextual_menu = GMenu.menu ()
@@ -551,17 +544,20 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       self#_showSearch
 
     method private grammar () =
-      self#_loadText (Print_grammar.ebnf_of_term self#script#status);
+      self#_loadText
+       (Print_grammar.ebnf_of_term (get_matita_script_current ())#status);
 
     method private home () =
       self#_showMath;
-      match self#script#status#ng_mode with
-         `ProofMode -> self#_loadNObj self#script#status self#script#status#obj
-       | _ -> self#blank ()
+      let status = (get_matita_script_current ())#status in
+       match status#ng_mode with
+          `ProofMode -> self#_loadNObj status status#obj
+        | _ -> self#blank ()
 
     method private _loadNReference (NReference.Ref (uri,_)) =
-      let obj = NCicEnvironment.get_checked_obj uri in
-      self#_loadNObj self#script#status obj
+      let status = (get_matita_script_current ())#status in
+      let obj = NCicEnvironment.get_checked_obj status uri in
+      self#_loadNObj status obj
 
     method private _loadDir dir = 
       let content = Http_getter.ls ~local:false dir in
@@ -643,7 +639,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
@@ -661,17 +657,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 =
@@ -680,6 +690,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 ->
@@ -687,20 +698,6 @@ let sequentsViewer_instance =
    else
     (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