more dead code removal

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index aa854e2dfeaacfbd153968fffd9443f48498cc98..bacc4aa26b3a8452a9cdde7baf425c82c2238d95 100644 (file)
--- 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 6297a57bc7555f3008e5859758d3807c47b4e5a2..9332d97223e06fa6d635ae9d999cd4ceac156021 100644 (file)
--- 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) ->