aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-04-22 06:50:41 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-04-22 06:50:41 +0000
commitc250c03254bda83775647b47bc35274ea0747647 (patch)
tree990a7cc521570e76777412748724b7ca986ead10
parentdf95bf41c5d60d5baa915cb3ca6080af4da968ec (diff)
Coqide: fix synchro when restarting during a single step
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14052 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--ide/coqide.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index cc36dd9de..d6ebdc307 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -946,9 +946,11 @@ object(self)
match sync get_next_phrase () with
| None -> raise Unsuccessful
| Some (loc,phrase) ->
- match self#send_to_coq ct verbosely phrase true true true with
+ try match self#send_to_coq ct verbosely phrase true true true with
| Some safe -> sync mark_processed safe loc
| None -> sync remove_tag loc; raise Unsuccessful
+ with
+ | RestartCoqtop -> sync remove_tag loc; raise RestartCoqtop
method process_next_phrase verbosely =
try self#process_one_phrase !mycoqtop verbosely true true