Small interface improvement: the first goal page is no more forced unless

the current goal is the first one.

Open bug: the current goal is forced again when visited a second time!

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 22bb994550a76780df5b9787e9fb091654e60447..86baadbd5d9d1e37bf613efbba882be24e93ff5f 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -687,7 +687,7 @@ let refresh_sequent ?(empty_notebook=true) notebook =
      None ->
       if empty_notebook then
        begin 
-        notebook#remove_all_pages ;
+        notebook#remove_all_pages ~skip_switch_page_event:false ;
         notebook#set_empty_page
        end
       else
@@ -710,8 +710,13 @@ let refresh_sequent ?(empty_notebook=true) notebook =
          in
           if empty_notebook then
            begin
-            notebook#remove_all_pages ;
-            List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
+            let skip_switch_page_event =
+             match metasenv with
+                (m,_,_)::_ when m = metano -> false
+              | _ -> true
+            in
+             notebook#remove_all_pages ~skip_switch_page_event ;
+             List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
            end ;
           notebook#set_current_page metano ;
           notebook#proofw#load_tree ~dom:sequent_mml ;
@@ -2028,9 +2033,11 @@ object(self)
    notebook#append_page
     ~tab_label:((GMisc.label ~text:("?" ^ string_of_int n) ())#coerce)
     new_page#content#coerce
- method remove_all_pages =
+ method remove_all_pages ~skip_switch_page_event:skip =
   List.iter (function _ -> notebook#remove_page 0) !pages ;
   pages := [] ;
+prerr_endline ("@@@ " ^ if skip_switch_page_event then "true" else "false" ^ " ===> " ^ if skip then "true" else "false") ;
+  skip_switch_page_event <- skip
  method set_current_page n =
   let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in
    let new_page = notebook#page_num page#content#coerce in