From 95639a0a6e187e8ba8c08e71688d8065ef319408 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 7 Jun 2012 11:18:36 +0000 Subject: [PATCH] Sys.Break no longer catched --- matita/components/grafite_engine/grafiteEngine.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) 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 -- 2.39.2