From c02d503febfeba8abfffa66385b296d92862ab3e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 15 Nov 2002 13:14:41 +0000 Subject: [PATCH] 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! --- helm/gTopLevel/gTopLevel.ml | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 22bb99455..86baadbd5 100644 --- 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 -- 2.39.2