- useless code removed

diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml
index 43a09d2a6e50cd329592086ea0eefe28a6976a12..374ada5cc7b66d4c1aaa0024773e0bb2d500a285 100644 (file)
--- a/matita/matita/matitaEngine.ml
+++ b/matita/matita/matitaEngine.ml
@@ -86,40 +86,32 @@ 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 ~include_paths ?do_heavy_checks
- ?(enforce_no_new_aliases=true) status str cb 
-=
+let eval_from_stream ~include_paths ?do_heavy_checks status str cb =
  let matita_debug = Helm_registry.get_bool "matita.debug" in
- let rec loop status statuses =
-  let stop,g,s = 
+ let rec loop status =
+  let stop,status = 
    try
      let cont =
        try Some (GrafiteParser.parse_statement status str)
        with End_of_file -> None in
      match cont with
-     | None -> true, status, statuses
+     | None -> true, status
      | Some ast ->
         cb status ast;
         let new_statuses =
           eval_ast ~include_paths ?do_heavy_checks status ("",0,ast) in
-        if enforce_no_new_aliases then
-         List.iter 
-          (fun (_,alias) ->
-            match alias with
-              None -> ()
-            | Some (k,value) ->
-               let newtxt = GrafiteAstPp.pp_alias value in
-                raise (TryingToAdd newtxt)) new_statuses;
         let status =
          match new_statuses with
-            [] -> assert false
-          | (s,_)::_ -> s
+            [s,None] -> s
+          | _::(_,Some (_,value))::_ ->
+                raise (TryingToAdd (GrafiteAstPp.pp_alias value))
+          | _ -> assert false
         in
-         false, status, (new_statuses @ statuses)
+         false, status
    with exn when not matita_debug ->
      raise (EnrichedWithStatus (exn, status))
   in
-  if stop then s else loop g s
+  if stop then status else loop status
  in
-  loop status []
+  loop status
 ;;

diff --git a/matita/matita/matitaEngine.mli b/matita/matita/matitaEngine.mli
index 9332d97223e06fa6d635ae9d999cd4ceac156021..2639f1d046e760333804964d2aea256b29cf2fa0 100644 (file)
--- a/matita/matita/matitaEngine.mli
+++ b/matita/matita/matitaEngine.mli
@@ -41,11 +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 :
-  include_paths:string list ->
-  ?do_heavy_checks:bool ->
-  ?enforce_no_new_aliases:bool -> (* default true *)
-  GrafiteTypes.status ->
-  Ulexing.lexbuf ->
-  (GrafiteTypes.status -> GrafiteAst.statement -> unit) ->
-  (GrafiteTypes.status *
-   (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) option) list
+  include_paths:string list -> ?do_heavy_checks:bool -> GrafiteTypes.status ->
+   Ulexing.lexbuf -> (GrafiteTypes.status -> GrafiteAst.statement -> unit) ->
+    GrafiteTypes.status

diff --git a/matita/matita/matitacLib.ml b/matita/matita/matitacLib.ml
index b4168ba94ca47fba77bafe84f011cbc9d998bcc2..5ae5dbf3b4a1dc8d08a7b97fbb3505dda0825392 100644 (file)
--- a/matita/matita/matitacLib.ml
+++ b/matita/matita/matitacLib.ml
@@ -29,8 +29,6 @@ open Printf
 
 open GrafiteTypes
 
-exception AttemptToInsertAnAlias of GrafiteDisambiguate.status
-
 let slash_n_RE = Pcre.regexp "\\n" ;;
 
 let pp_ast_statement grafite_status stm =
@@ -164,16 +162,7 @@ let compile atstart options fname =
       else pp_ast_statement
     in
     let grafite_status =
-     let rec aux_for_dump x grafite_status =
-      match
-       MatitaEngine.eval_from_stream ~include_paths grafite_status buf x
-      with
-      | [] -> grafite_status
-      | (g,None)::_ -> g
-      | (g,Some _)::_ ->
-         raise (AttemptToInsertAnAlias (g :> GrafiteDisambiguate.status))
-     in
-       aux_for_dump print_cb grafite_status
+     MatitaEngine.eval_from_stream ~include_paths grafite_status buf print_cb
     in
     let elapsed = Unix.time () -. time in
      (if Helm_registry.get_bool "matita.moo" then begin
@@ -198,13 +187,6 @@ let compile atstart options fname =
      true)
   with 
   (* all exceptions should be wrapped to allow lexicon-undo (LS.time_travel) *)
-  | AttemptToInsertAnAlias lexicon_status -> 
-     pp_times fname false big_bang big_bang_u big_bang_s;
-(*
-     LexiconSync.time_travel 
-       ~present:lexicon_status ~past:initial_lexicon_status;
-*)
-     clean_exit baseuri false
   | MatitaEngine.EnrichedWithStatus (exn, _grafite) as exn' ->
       (match exn with
       | Sys.Break -> HLog.error "user break!"