]> matita.cs.unibo.it Git - helm.git/commitdiff
Reindentation
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 23 Sep 2003 17:33:30 +0000 (17:33 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 23 Sep 2003 17:33:30 +0000 (17:33 +0000)
helm/gTopLevel/gTopLevel.ml

index 7ed63cb102abdbc20c0072b4812254cda01a4488..7fe26ff59c896b6abad5cd87bdf85c937b3ff94f 100644 (file)
@@ -622,18 +622,18 @@ let refresh_goals ?(empty_notebook=true) notebook =
           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 =