Useless code removed.

[helm.git] / helm / software / matita / matitaScript.ml

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 65d7be828f0e0ebeb4199fd3f4dbb46e8d25180c..a5e24d3150853ce71cf11e5662c31b480ecf0f30 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -76,7 +76,6 @@ let eval_with_engine include_paths guistuff lexicon_status grafite_status user_g
 =
   let module TAPp = GrafiteAstPp in
   let module DTE = DisambiguateTypes.Environment in
-  let module DP = DisambiguatePp in
   let parsed_text_length =
     String.length skipped_txt + String.length nonskipped_txt 
   in
@@ -94,8 +93,8 @@ let eval_with_engine include_paths guistuff lexicon_status grafite_status user_g
       (fun (acc, to_prepend) (status,alias) ->
        match alias with
        | None -> (status,to_prepend ^ nonskipped_txt)::acc,""
-       | Some (k,((v,_) as value)) ->
-            let newtxt = DP.pp_environment (DTE.add k value DTE.empty) in
+       | Some (k,value) ->
+            let newtxt = LexiconAstPp.pp_alias value in
             (status,to_prepend ^ newtxt ^ "\n")::acc, "")
       ([],skipped_txt) enriched_history_fragment
   in
@@ -582,7 +581,7 @@ lexicon_status grafite_status user_goal unparsed_text skipped_txt nonskipped_txt
 script ex loc
 =
  let module TAPp = GrafiteAstPp in
- let module MD = GrafiteDisambiguator in
+ let module MD = MultiPassDisambiguator in
  let module ML = MatitaMisc in
   try
    ignore (buffer#move_mark (`NAME "beginning_of_statement")
@@ -642,9 +641,9 @@ and eval_statement include_paths (buffer : GText.buffer) guistuff lexicon_status
           HExtlib.Localized (floc, exn) ->
            HExtlib.raise_localized_exception 
              ~offset:(MatitaGtkMisc.utf8_string_length parsed_text) floc exn
-        | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
+        | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
            raise
-            (GrafiteDisambiguator.DisambiguationError
+            (MultiPassDisambiguator.DisambiguationError
               (offset+parsed_text_length, errorll))
       in
       assert (text=""); (* no macros inside comments, please! *)