notebook#remove_all_pages ~skip_switch_page_event ;
List.iter (function (m,_,_) -> notebook#add_page m) metasenv ;
in
- if empty_notebook then
- begin
- regenerate_notebook () ;
- notebook#set_current_page
- ~may_skip_switch_page_event:false metano
- end
- else
- begin
- notebook#set_current_page
- ~may_skip_switch_page_event:true metano ;
- notebook#proofw#load_sequent metasenv currentsequent
- end
+ if empty_notebook then
+ begin
+ regenerate_notebook () ;
+ notebook#set_current_page
+ ~may_skip_switch_page_event:false metano
+ end
+ else
+ begin
+ notebook#set_current_page
+ ~may_skip_switch_page_event:true metano ;
+ notebook#proofw#load_sequent metasenv currentsequent
+ end
with
e ->
let metano =