From c6b408de46049021e42ebabd3ce382de1257c620 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 15 May 2012 13:12:43 +0000 Subject: [PATCH] Sys.Break no longer caught during indexing --- matita/components/grafite_engine/grafiteEngine.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index ec14f4d3e..b6f5b14e6 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -62,7 +62,7 @@ let eval_unification_hint status t n = NCicLibrary.dump_obj status (inject_unification_hint (t,n)) ;; -let basic_index_obj l status = +let basic_index_obj l (status:#NCic.status) = status#set_auto_cache (List.fold_left (fun t (ks,v) -> @@ -560,6 +560,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let obj = uri,height,[],[],obj_kind in let old_status = status in let status = NCicLibrary.add_obj status obj in + (try let index_obj = index && match obj_kind with NCic.Constant (_,_,_,_,(_,`Example,_)) @@ -570,7 +571,9 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = if index_obj then let status = index_obj_for_auto status obj in (try index_eq_for_auto status uri - with _ -> status) + with + Sys.Break as exn -> raise exn + | _ -> status) else status in (* @@ -580,7 +583,6 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = in *) (* prerr_endline (status#ppobj obj); *) HLog.message ("New object: " ^ NUri.string_of_uri uri); - (try (*prerr_endline (status#ppobj obj);*) let boxml = NCicElim.mk_elims status obj in let boxml = boxml @ NCicElim.mk_projections status obj in -- 2.39.2