From 608b33a4b7c6b9c36b0637ba3894afe7093e9000 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 5 Nov 2010 11:18:41 +0000 Subject: [PATCH] more dead code removal --- matita/matita/matitaEngine.ml | 7 ++----- matita/matita/matitaEngine.mli | 1 - 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml index aa854e2df..bacc4aa26 100644 --- a/matita/matita/matitaEngine.ml +++ b/matita/matita/matitaEngine.ml @@ -87,7 +87,7 @@ exception TryingToAdd of string exception EnrichedWithStatus of exn * GrafiteTypes.status let eval_from_stream ~include_paths ?do_heavy_checks - ?(enforce_no_new_aliases=true) ?(watch_statuses=fun _ -> ()) status str cb + ?(enforce_no_new_aliases=true) status str cb = let matita_debug = Helm_registry.get_bool "matita.debug" in let rec loop status statuses = @@ -100,9 +100,7 @@ let eval_from_stream ~include_paths ?do_heavy_checks | None -> true, status, statuses | Some ast -> (match ast with - GrafiteParser.LNone _ -> - watch_statuses status ; - false, status, ((status,None)::statuses) + GrafiteParser.LNone _ -> false, status, ((status,None)::statuses) | GrafiteParser.LSome ast -> cb status ast; let new_statuses = @@ -120,7 +118,6 @@ let eval_from_stream ~include_paths ?do_heavy_checks [] -> assert false | (s,_)::_ -> s in - watch_statuses status ; false, status, (new_statuses @ statuses)) with exn when not matita_debug -> raise (EnrichedWithStatus (exn, status)) diff --git a/matita/matita/matitaEngine.mli b/matita/matita/matitaEngine.mli index 6297a57bc..9332d9722 100644 --- a/matita/matita/matitaEngine.mli +++ b/matita/matita/matitaEngine.mli @@ -44,7 +44,6 @@ val eval_from_stream : include_paths:string list -> ?do_heavy_checks:bool -> ?enforce_no_new_aliases:bool -> (* default true *) - ?watch_statuses:(GrafiteTypes.status -> unit) -> GrafiteTypes.status -> Ulexing.lexbuf -> (GrafiteTypes.status -> GrafiteAst.statement -> unit) -> -- 2.39.2