From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 7 Jun 2012 11:18:36 +0000 (+0000)
Subject: Sys.Break no longer catched
X-Git-Tag: make_still_working~1651
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=95639a0a6e187e8ba8c08e71688d8065ef319408;p=helm.git

Sys.Break no longer catched
---

diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml
index bd0fd6cea..af0abe04a 100644
--- a/matita/components/grafite_engine/grafiteEngine.ml
+++ b/matita/components/grafite_engine/grafiteEngine.ml
@@ -654,7 +654,9 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                                     ("",0,GrafiteAst.NQed (Stdpp.dummy_loc,false))
                            | _ -> status))
                        (* XXX *)
-                      with _ -> (*HLog.warn "error in generating inversion principle"; *)
+                      with
+                         Sys.Break as exn -> raise exn
+                       | _ -> (*HLog.warn "error in generating inversion principle"; *)
                                 let status = status#set_ng_mode `CommandMode in status)
                   status
                   (NCic.Prop::
@@ -707,7 +709,9 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) =
                                     ("",0,GrafiteAst.NQed(Stdpp.dummy_loc,false))
                            | _ -> status))
                        (* XXX *)
-                      with _ -> (*HLog.warn "error in generating discrimination principle"; *)
+                      with
+                         Sys.Break as exn -> raise exn
+                       | _ -> (*HLog.warn "error in generating discrimination principle"; *)
                                 let status = status#set_ng_mode `CommandMode in
                                 status)
                   status' itl