X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=7d3985af3a56b63ef24059f16bac82e8f3a06232;hb=5333af1b6dba295b496e75b0ba864f87ebc1eb88;hp=7ed63cb102abdbc20c0072b4812254cda01a4488;hpb=969d115cf2bc8d0fba05db54ab0886042f3d9512;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 7ed63cb10..7d3985af3 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -593,6 +593,10 @@ let refresh_proof (output : TermViewer.proof_viewer) =
 prerr_endline ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[]))) ; flush stderr ;
    raise (InvokeTactics.RefreshProofException e)
 
+let set_proof_engine_goal g =
+ ProofEngine.goal := g
+;;
+
 let refresh_goals ?(empty_notebook=true) notebook =
  try
   match !ProofEngine.goal with
@@ -622,18 +626,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 =
@@ -701,14 +705,13 @@ let load_unfinished_proof () =
         match CicParser.obj_of_xml prooffiletype (Some prooffile) with
            Cic.CurrentProof (_,metasenv,bo,ty,_) ->
             typecheck_loaded_proof metasenv bo ty ;
-            ProofEngine.set_proof
-             (Some (uri, metasenv, bo, ty)) ;
-            ProofEngine.goal :=
+            ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ;
+            refresh_proof output ;
+            set_proof_engine_goal
              (match metasenv with
                  [] -> None
                | (metano,_,_)::_ -> Some metano
              ) ;
-            refresh_proof output ;
             refresh_goals notebook ;
              output_html outputhtml
               ("<h1 color=\"Green\">Current proof type loaded from " ^
@@ -1581,7 +1584,7 @@ prerr_endline ("######################## " ^ xxx) ;
     let _  = CicTypeChecker.type_of_aux' metasenv [] expr in
      ProofEngine.set_proof
       (Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)) ;
-     ProofEngine.goal := Some 1 ;
+     set_proof_engine_goal (Some 1) ;
      refresh_goals notebook ;
      refresh_proof output ;
      !save_set_sensitive true ;
@@ -1671,9 +1674,8 @@ let open_ () =
        | Cic.Variable _
        | Cic.InductiveDefinition _ -> raise NotADefinition
      in
-      ProofEngine.set_proof
-       (Some (uri, metasenv, bo, ty)) ;
-      ProofEngine.goal := None ;
+      ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ;
+      set_proof_engine_goal None ;
       refresh_goals notebook ;
       refresh_proof output ;
       !save_set_sensitive true
@@ -2652,7 +2654,7 @@ object(self)
        if not skip then
         try
          let (metano,setgoal,page) = List.nth !pages i in
-          ProofEngine.goal := Some metano ;
+          set_proof_engine_goal (Some metano) ;
           Lazy.force (page#compute) ;
           Lazy.force setgoal;
           if notify_hbugs_on_goal_change then