syntactic components detached from basic_2 become static_2

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

diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml
index df8b5359d98b72e54a1361960f008fe03dfc656d..ea9683e188bd6232c3e2996806541fed68a2d56a 100644 (file)
--- a/matita/matita/matitaMathView.ml
+++ b/matita/matita/matitaMathView.ml
@@ -107,20 +107,19 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
       let win goal_switch =
         let w =
           GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`ALWAYS
-            ~shadow_type:`IN ~show:true ()
-        in
+            ~shadow_type:`IN ~show:true () 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
         in
         goal2win <- (goal_switch, reparent) :: goal2win;
         w#coerce
@@ -191,7 +190,24 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
           cicMathView#load_root ~root);
       (try
         cicMathView#set_selection None;
-        List.assoc goal_switch goal2win ()
+        List.assoc goal_switch goal2win ();
+        (match cicMathView#misc#parent with
+           None -> assert false
+         | Some p ->
+            (* The text widget dinamycally inserts the text in a separate
+               thread. We need to wait for it to terminate before we can
+               move the scrollbar to the end *)
+            while Glib.Main.pending()do ignore(Glib.Main.iteration false); done;
+            let w =
+             new GBin.scrolled_window
+              (Gobject.try_cast p#as_widget "GtkScrolledWindow") in
+            (* The double change upper/lower is to trigger the emission of
+               changed :-( *)
+            w#hadjustment#set_value w#hadjustment#upper;
+            w#hadjustment#set_value w#hadjustment#lower;
+            w#vadjustment#set_value w#vadjustment#lower;
+            w#vadjustment#set_value
+             (w#vadjustment#upper -. w#vadjustment#page_size));
       with Not_found -> assert false)
 
     method goto_sequent: 'status. #ApplyTransformation.status as 'status -> int -> unit
@@ -205,7 +221,6 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
       in
       notebook#goto_page page;
       self#render_page status ~page ~goal_switch
-
   end
 
 let blank_uri = BuildTimeConf.blank_uri
@@ -318,7 +333,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       HExtlib.safe_remove filename
   in
   object (self)
-    val mutable gviz_uri = NReference.reference_of_string "cic:/dummy.dec";
+    val mutable gviz_uri =
+      let uri = NUri.uri_of_string "cic:/dummy/dec.con" in
+      NReference.reference_of_spec uri NReference.Decl;
 
     val dep_contextual_menu = GMenu.menu ()
 
@@ -550,8 +567,9 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
         | _ -> self#blank ()
 
     method private _loadNReference (NReference.Ref (uri,_)) =
-      let obj = NCicEnvironment.get_checked_obj uri in
-      self#_loadNObj (get_matita_script_current ())#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
@@ -633,7 +651,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 +669,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 +702,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 +711,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