Stupid bug of mine fixed: sometimes (Some ~-1) was used in place of None.

Moreover the userGoal was retrieved before setting it.

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 69b14b8190b8ab90d076120aab94da41b4147ed6..016d69336313f372ed419b3a720b09580f54cc7d 100644 (file)
--- a/helm/matita/matita.ml
+++ b/helm/matita/matita.ml
@@ -81,15 +81,15 @@ let _ =
     match grafite_status.proof_status with
     | Incomplete_proof ({ stack = stack } as incomplete_proof) ->
         sequents_viewer#load_sequents incomplete_proof;
-        let goal =
-         match script#goal with
-            None -> assert false
-          | Some n -> n
-        in
         (try
-          script#setGoal (Continuationals.Stack.find_goal stack);
-          sequents_viewer#goto_sequent goal
-        with Failure _ -> script#setGoal ~-1);
+          script#setGoal (Some (Continuationals.Stack.find_goal stack));
+          let goal =
+           match script#goal with
+              None -> assert false
+            | Some n -> n
+          in
+           sequents_viewer#goto_sequent goal
+        with Failure _ -> script#setGoal None);
     | Proof proof -> sequents_viewer#load_logo_with_qed
     | No_proof -> sequents_viewer#load_logo
     | Intermediate _ -> assert false (* only the engine may be in this state *)

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index 794b849c4918202171780c1b2c496c0b1b7a7a2e..ffbb8d7c06c164fa8584d2698d7cf137911d628c 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -580,7 +580,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
       goal2page <- [];
       goal2win <- [];
       _metasenv <- []; 
-      self#script#setGoal ~-1;
+      self#script#setGoal None
 
     method load_sequents { proof = (_,metasenv,_,_) as proof; stack = stack } =
       _metasenv <- metasenv;
@@ -655,7 +655,7 @@ class sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) () =
           let goal_switch =
             try List.assoc page page2goal with Not_found -> assert false
           in
-          self#script#setGoal (goal_of_switch goal_switch);
+          self#script#setGoal (Some (goal_of_switch goal_switch));
           self#render_page ~page ~goal_switch))
 
     method private render_page ~page ~goal_switch =

diff --git a/helm/matita/matitaScript.ml b/helm/matita/matitaScript.ml
index d628af98dff7b237331bb4ca094087a9e41438ec..a94d8aecf90aa932f9863c59247b690560bf92e0 100644 (file)
--- a/helm/matita/matitaScript.ml
+++ b/helm/matita/matitaScript.ml
@@ -766,7 +766,7 @@ object (self)
        GrafiteTypes.get_proof_conclusion self#grafite_status n
 
   method stack = GrafiteTypes.get_stack self#grafite_status
-  method setGoal n = userGoal <- Some n
+  method setGoal n = userGoal <- n
   method goal = userGoal
 
   method eos = 

diff --git a/helm/matita/matitaScript.mli b/helm/matita/matitaScript.mli
index edebcf322204da1e9fd5d3883afd6e4b9b5bd8c3..8eb6d8dd9afc0d44596d6bde9c696a0c0249d033 100644 (file)
--- a/helm/matita/matitaScript.mli
+++ b/helm/matita/matitaScript.mli
@@ -67,7 +67,7 @@ object
   method proofConclusion: Cic.term            (** @raise Statement_error *)
   method stack: Continuationals.Stack.t       (** @raise Statement_error *)
 
-  method setGoal: int -> unit
+  method setGoal: int option -> unit
   method goal: int option
 
   (** end of script, true if the whole script has been executed *)