The modules in proofs now use the Errors module to explain their exceptions to the toplevel

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14120 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 42 insertions, 13 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
index c70eb3ed46..9be2d028a1 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -334,6 +334,7 @@ let defs _ rdefs _ _ =
     [null], [plus], [here] and [here_list] use internal exception [UndefinedHere]
     to communicate whether or not the value is defined in the particular context. *)
 exception UndefinedHere
+(* no handler: this should never be allowed to reach toplevel *)
 let null _ _ _ _ = raise UndefinedHere
 
 let plus s1 s2 env rdefs goal info =
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index fff1a121d6..ad15ff9031 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -92,6 +92,10 @@ let set_end_tac tac =
   Proof_global.set_endline_tactic tac
 
 exception NoSuchGoal
+let _ = Errors.register_handler begin function
+  | NoSuchGoal -> Util.error "No such goal."
+  | _ -> raise Errors.Unhandled
+end
 let get_nth_V82_goal i =
   let p = Proof_global.give_me_the_proof () in
   let { it=goals ; sigma = sigma } = Proof.V82.subgoals p in
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 3feef112f6..7e5941025c 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -49,6 +49,7 @@ let new_focus_kind () =
    [check kind1 kind2 inf] returns [inf] if [kind1] and [kind2] match.
    Otherwise it raises [CheckNext] *)
 exception CheckNext
+(* no handler: confined to this module. *)
 let check kind1 kind2 inf =
   if kind1=kind2 then inf else raise CheckNext
 
@@ -130,6 +131,11 @@ let partial_proof p =
 
 exception UnfinishedProof
 exception HasUnresolvedEvar
+let _ = Errors.register_handler begin function
+  | UnfinishedProof -> Util.error "Some goals have not been solved."
+  | HasUnresolvedEvar -> Util.error "Some existential variables are uninstantiated."
+  | _ -> raise Errors.Unhandled
+end
 let return p =
   if not (is_done p) then
     raise UnfinishedProof
@@ -147,7 +153,10 @@ let push_focus cond inf context pr =
   pr.state <- { pr.state with focus_stack = (cond,inf,context)::pr.state.focus_stack }
 
 exception FullyUnfocused
-
+let _ = Errors.register_handler begin function
+  | FullyUnfocused -> Util.error "The proof is not focused"
+  | _ -> raise Errors.Unhandled
+end
 (* An auxiliary function to read the kind of the next focusing step *)
 let cond_of_focus pr =
   match pr.state.focus_stack with
@@ -171,6 +180,10 @@ let push_undo save pr =
 
 (* Auxiliary function to pop and read a [save_state] from the undo stack. *)
 exception EmptyUndoStack
+let _ = Errors.register_handler begin function
+  | EmptyUndoStack -> Util.error "Cannot undo: no more undo information"
+  | _ -> raise Errors.Unhandled
+end
 let pop_undo pr =
   match pr.transactions , pr.undo_stack with
   | [] , state::stack -> pr.undo_stack <- stack; state
@@ -242,19 +255,18 @@ let focus cond inf i pr =
    Fails if the proof is not focused. *)
 let unfocus kind pr =
   let starting_point = save_state pr in
-  try
-    let cond = cond_of_focus pr in
-    if fst cond kind pr.state.proofview then
-      (_unfocus pr;
-       push_undo starting_point pr)
-    else
-      Util.error "This proof is focused, but cannot be unfocused this way"
-  with FullyUnfocused -> 
-    Util.error "This proof is not focused"
-
+  let cond = cond_of_focus pr in
+  if fst cond kind pr.state.proofview then
+    (_unfocus pr;
+     push_undo starting_point pr)
+  else
+    Util.error "This proof is focused, but cannot be unfocused this way"
+      
 let get_at_point kind ((_,get),inf,_) = get kind inf
 exception NoSuchFocus
+(* no handler: should not be allowed to reach toplevel. *)
 exception GetDone of Obj.t
+(* no handler: confined to this module. *)
 let get_in_focus_stack kind stack =
   try
     List.iter begin fun pt ->
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index f930486673..76aa300aa1 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -92,6 +92,10 @@ let push a l = l := a::!l;
   update_proof_mode ()
 
 exception NoSuchProof
+let _ = Errors.register_handler begin function
+  | NoSuchProof -> Util.error "No such proof."
+  | _ -> raise Errors.Unhandled
+end
 let rec extract id l = 
   let rec aux = function
     | ((id',_) as np)::l when id_ord id id' = 0 -> (np,l)
@@ -104,6 +108,10 @@ let rec extract id l =
   np
 
 exception NoCurrentProof
+let _ = Errors.register_handler begin function
+  | NoCurrentProof -> Util.error "No focused proof (No proof-editing in progress)."
+  | _ -> raise Errors.Unhandled
+end
 let extract_top l =
   match !l with
   | np::l' -> l := l' ; update_proof_mode (); np
@@ -292,8 +300,7 @@ let maximal_unfocus k p =
   begin try while Proof.no_focused_goal p do
     Proof.unfocus k p
   done
-  with Util.UserError _ -> (* arnaud: attention à ça si je fini par me décider à mettre une vrai erreur pour Proof.unfocus *)
-    ()
+  with Proof.FullyUnfocused -> ()
   end
 
 
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 2802acfc1a..aa00cee829 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -70,6 +70,7 @@ let return { initial=init; solution=defs }  =
 (* [IndexOutOfRange] occurs in case of malformed indices
    with respect to list lengths. *)
 exception IndexOutOfRange
+(* no handler: should not be allowed to reach toplevel *)
 
 (* [list_goto i l] returns a pair of lists [c,t] where
    [c] has length [i] and is the reversed of the [i] first
@@ -278,6 +279,10 @@ let tclFOCUS i j t env = { go = fun sk fk step ->
     sense in the goals immediatly built by it, and would cause an anomaly
     is used otherwise. *)
 exception SizeMismatch
+let _ = Errors.register_handler begin function
+  | SizeMismatch -> Util.error "Incorrect number of goals."
+  | _ -> raise Errors.Unhandled
+end
 (* spiwack: we use an parametrised function to generate the dispatch tacticals.
     [tclDISPATCHGEN] takes a [null] argument to generate the return value
     if there are no goal under focus, and a [join] argument to explain how