Residual interface bug fixes: no sequent page is now forced twice.

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 86baadbd5d9d1e37bf613efbba882be24e93ff5f..3b6eaff25cc00309222d5f4b6cf18df1f2460bcc 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -702,24 +702,29 @@ let refresh_sequent ?(empty_notebook=true) notebook =
        let sequent_gdome,ids_to_terms,ids_to_father_ids,ids_to_hypotheses =
         SequentPp.XmlPp.print_sequent metasenv currentsequent
        in
-        let sequent_doc =
-         Xml2Gdome.document_of_xml domImpl sequent_gdome
-        in
-         let sequent_mml =
-          applyStylesheets sequent_doc sequent_styles sequent_args
+        let regenerate_notebook () = 
+         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 ;
+        in
           if empty_notebook then
            begin
-            let skip_switch_page_event =
-             match metasenv with
-                (m,_,_)::_ when m = metano -> false
-              | _ -> true
+            regenerate_notebook () ;
+            notebook#set_current_page ~may_skip_switch_page_event:false metano
+           end
+          else
+           begin
+            let sequent_doc = Xml2Gdome.document_of_xml domImpl sequent_gdome in
+            let sequent_mml =
+             applyStylesheets sequent_doc sequent_styles sequent_args
             in
-             notebook#remove_all_pages ~skip_switch_page_event ;
-             List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
+             notebook#set_current_page ~may_skip_switch_page_event:true metano;
+             notebook#proofw#load_tree ~dom:sequent_mml
            end ;
-          notebook#set_current_page metano ;
-          notebook#proofw#load_tree ~dom:sequent_mml ;
           current_goal_infos :=
            Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
  with
@@ -2036,12 +2041,11 @@ object(self)
  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 =
+ method set_current_page ~may_skip_switch_page_event n =
   let (_,_,page) = List.find (function (m,_,_) -> m=n) !pages in
    let new_page = notebook#page_num page#content#coerce in
-    if new_page <> notebook#current_page then
+    if may_skip_switch_page_event && new_page <> notebook#current_page then
      skip_switch_page_event <- true ;
     notebook#goto_page new_page
  method set_empty_page = self#add_page (-1)