From: Andrea Asperti Date: Fri, 5 Nov 2010 11:16:18 +0000 (+0000) Subject: dead code removed X-Git-Tag: make_still_working~2717 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1009a1048c267f007cc1a265fafaeacfe5af740c;p=helm.git dead code removed --- diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml index 429f75cd3..aa854e2df 100644 --- a/matita/matita/matitaEngine.ml +++ b/matita/matita/matitaEngine.ml @@ -86,16 +86,11 @@ let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) = exception TryingToAdd of string exception EnrichedWithStatus of exn * GrafiteTypes.status -let eval_from_stream ~first_statement_only ~include_paths - ?do_heavy_checks ?(enforce_no_new_aliases=true) - ?(watch_statuses=fun _ -> ()) status str cb +let eval_from_stream ~include_paths ?do_heavy_checks + ?(enforce_no_new_aliases=true) ?(watch_statuses=fun _ -> ()) status str cb = let matita_debug = Helm_registry.get_bool "matita.debug" in let rec loop status statuses = - let loop = - if first_statement_only then fun _ statuses -> statuses - else loop - in let stop,g,s = try let cont = diff --git a/matita/matita/matitaEngine.mli b/matita/matita/matitaEngine.mli index e559d5a0c..6297a57bc 100644 --- a/matita/matita/matitaEngine.mli +++ b/matita/matita/matitaEngine.mli @@ -41,7 +41,6 @@ exception EnrichedWithStatus of exn * GrafiteTypes.status (* should be used only by the compiler since it looses the * disambiguation_context (text,prefix_len,_) *) val eval_from_stream : - first_statement_only:bool -> include_paths:string list -> ?do_heavy_checks:bool -> ?enforce_no_new_aliases:bool -> (* default true *) diff --git a/matita/matita/matitacLib.ml b/matita/matita/matitacLib.ml index d1962c99d..b4168ba94 100644 --- a/matita/matita/matitacLib.ml +++ b/matita/matita/matitacLib.ml @@ -166,8 +166,7 @@ let compile atstart options fname = let grafite_status = let rec aux_for_dump x grafite_status = match - MatitaEngine.eval_from_stream ~first_statement_only:false ~include_paths - grafite_status buf x + MatitaEngine.eval_from_stream ~include_paths grafite_status buf x with | [] -> grafite_status | (g,None)::_ -> g