From 04b447005f0428ac68ef5bf7dd1d6d3349bc1567 Mon Sep 17 00:00:00 2001
From: corbinea
Date: Thu, 26 Feb 2004 15:36:51 +0000
Subject: added breakpoints to help ide

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5387 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/refiner.ml    | 15 +++++++++------
 tactics/tacinterp.ml |  3 ++-
 2 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 575c27fbd5..4e70d8435d 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -332,6 +332,7 @@ let unpackage glsig = (ref (glsig.sigma)),glsig.it
 let repackage r v = {it=v;sigma = !r}
 
 let apply_sig_tac r tac g =
+  check_for_interrupt (); (* Breakpoint *) 
   let glsigma,v = tac (repackage r g) in 
   r := glsigma.sigma;
   (glsigma.it,v)
@@ -517,9 +518,10 @@ let tclNOTSAMEGOAL (tac : tactic) goal =
 let tclORELSE0 t1 t2 g =
   try 
     t1 g
-  with
-  | e when catchable_exception e -> t2 g
-  | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_)) -> t2 g
+  with (* Breakpoint *)
+  | e when catchable_exception e -> check_for_interrupt (); t2 g
+  | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_)) ->
+      check_for_interrupt (); t2 g
   | FailError (lvl,s) -> raise (FailError (lvl - 1, s))
   | Stdpp.Exc_located (s,FailError (lvl,s')) ->
       raise (Stdpp.Exc_located (s,FailError (lvl - 1, s')))
@@ -551,10 +553,11 @@ let ite_gen tcal tac_if continue tac_else gl=
       tac_else gl in
     try 
       tcal tac_if0 continue gl
-    with
-      | e when catchable_exception e -> tac_else0 e gl
+    with (* Breakpoint *)
+      | e when catchable_exception e ->
+	  check_for_interrupt (); tac_else0 e gl
       | (FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_))) as e ->
-	  tac_else0 e gl
+	  check_for_interrupt (); tac_else0 e gl
       | FailError (lvl,s) -> raise (FailError (lvl - 1, s))
       | Stdpp.Exc_located (s,FailError (lvl,s')) ->
 	  raise (Stdpp.Exc_located (s,FailError (lvl - 1, s')))
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index bc9a21ff32..fe96fa44d3 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1297,7 +1297,8 @@ let rec val_interp ist gl (tac:glob_tactic_expr) =
   (* Delayed evaluation *)
   | t -> VTactic (dummy_loc,eval_tactic ist t)
 
-  in match ist.debug with
+  in check_for_interrupt (); 
+    match ist.debug with
     | DebugOn lev ->
 	debug_prompt lev gl tac (fun v -> value_interp {ist with debug=v})
     | _ -> value_interp ist
-- 
cgit v1.2.3