From 0b79601e4c529cacbba2b64f99f3548df412f254 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 9 Jan 2006 09:39:14 +0000
Subject: [PATCH] Stupid bug of mine fixed: sometimes (Some ~-1) was used in
 place of None. Moreover the userGoal was retrieved before setting it.

---
 helm/matita/matita.ml         | 16 ++++++++--------
 helm/matita/matitaMathView.ml |  4 ++--
 helm/matita/matitaScript.ml   |  2 +-
 helm/matita/matitaScript.mli  |  2 +-
 4 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml
index 69b14b819..016d69336 100644
--- 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 794b849c4..ffbb8d7c0 100644
--- 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 d628af98d..a94d8aecf 100644
--- 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 edebcf322..8eb6d8dd9 100644
--- 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 *)
-- 
2.39.2