Every exception that used to have type string is now a string Lazy.t.

[helm.git] / helm / ocaml / tactics / continuationals.ml

diff --git a/helm/ocaml/tactics/continuationals.ml b/helm/ocaml/tactics/continuationals.ml
index 5b1bbce3daf9850c4c1a41ff284dab396d3a5b93..f4f9e34f665be5d106c4b2f68031fa18f23223fe 100644 (file)
--- a/helm/ocaml/tactics/continuationals.ml
+++ b/helm/ocaml/tactics/continuationals.ml
@@ -25,9 +25,7 @@
 
 open Printf
 
-exception Error of string 
-
-let fail msg = raise (Error msg)
+exception Error of string Lazy.t
 
 module type Engine =
 sig
@@ -157,8 +155,8 @@ struct
     match tactical, switch with
     | Tactic tac, Open n -> E.apply_tactic tac proof n
     | Skip, Closed n -> proof, [], [n]
-    | Tactic _, Closed _ -> fail "can't apply tactic to a closed goal"
-    | Skip, Open _ -> fail "can't skip an open goal"
+    | Tactic _, Closed _ -> raise (Error (lazy "can't apply tactic to a closed goal"))
+    | Skip, Open _ -> raise (Error (lazy "can't skip an open goal"))
 
   let eval continuational status =
     match continuational, status with
@@ -191,7 +189,7 @@ struct
     | Dot, (proof, (env, todo, left, tag)::tail) ->
         let env, left = 
           match List.filter is_open env, left with 
-          | [], [] -> fail "There is nothig to do for '.'"
+          | [], [] -> raise (Error (lazy "There is nothig to do for '.'"))
           | g::env,left -> [g], union (List.map goal_of env) left
           | [], g::left -> [dummy_pos, Open g], left
         in
@@ -199,7 +197,7 @@ struct
     | Branch, (proof, (g1::tl, todo, left, tag)::tail) ->
         assert (List.length tl >= 1);
         proof, ([g1], [], [], BranchTag)::(tl, todo, left, tag)::tail
-    | Branch, (_, _) -> fail "can't branch on a singleton context"
+    | Branch, (_, _) -> raise (Error (lazy "can't branch on a singleton context"))
     | Shift opt_pos, (proof, (leftopen, t, l,BranchTag)::
                              (goals, todo, left,tag)::tail) ->
         let next_goal, rem_goals =
@@ -208,19 +206,19 @@ struct
           | Some pos, _ ->
               (try
                 list_assoc_extract pos goals
-              with Not_found -> fail (sprintf "position %d not found" pos))
-          | None, [] -> fail "no more goals to shift"
+              with Not_found -> raise (Error (lazy (sprintf "position %d not found" pos))))
+          | None, [] -> raise (Error (lazy "no more goals to shift"))
         in
         let t =
           union t (union (List.map goal_of (List.filter is_open leftopen)) l)
         in
         proof, ([next_goal], t, [], BranchTag)::(rem_goals, todo,left,tag)::tail
-    | Shift _, (_, _) -> fail "no more goals to shift"
+    | Shift _, (_, _) -> raise (Error (lazy "no more goals to shift"))
     | Select gl, (proof, stack) ->
         List.iter
           (fun g ->
             if E.is_goal_closed g proof then
-              fail "you can't select a closed goal")
+              raise (Error (lazy "you can't select a closed goal")))
           gl;
         (proof, (open_all (map_dummy_pos gl),[],[],SelectTag)::stack)
     | End, (proof, stack) ->
@@ -233,7 +231,7 @@ struct
                   (union not_processed (List.filter is_open leftopen))))
             in
             proof, (env,todo,left,tag)::tail
-        | _ -> fail "can't end here")
+        | _ -> raise (Error (lazy "can't end here")))
 
   let init proof =
     proof,