Added debug menu item to restrict disambiguation to the first pass only.

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.ml b/helm/software/components/grafite_parser/grafiteDisambiguator.ml
index d9de808b019ea796235e551e4c33a591453f02f1..05c988ac16c98b349fed54a0a4c7268e3bcdb2de 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguator.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguator.ml
@@ -75,6 +75,8 @@ module Disambiguator = Disambiguate.Make (Callbacks)
 
 (* implement module's API *)
 
+let only_one_pass = ref false;;
+
 let disambiguate_thing ~aliases ~universe
   ~(f:?fresh_instances:bool ->
       aliases:DisambiguateTypes.environment ->
@@ -88,7 +90,10 @@ let disambiguate_thing ~aliases ~universe
   let library = false, DisambiguateTypes.Environment.empty, None in
   let multi_aliases = false, DisambiguateTypes.Environment.empty, universe in
   let mono_aliases = true, aliases, Some DisambiguateTypes.Environment.empty in
-  let passes =  (* <fresh_instances?, aliases, coercions?> *)
+  let passes = (* <fresh_instances?, aliases, coercions?> *)
+   if !only_one_pass then
+    [ (false, mono_aliases, false) ]
+   else
     [ (false, mono_aliases, false);
       (false, multi_aliases, false);
       (true, mono_aliases, false);

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.mli b/helm/software/components/grafite_parser/grafiteDisambiguator.mli
index b70eb737fba41df132a08aabb51f4076a747ed15..52add3974c8304f567f774b6a64c23834e6a3a99 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguator.mli
+++ b/helm/software/components/grafite_parser/grafiteDisambiguator.mli
@@ -30,6 +30,9 @@ exception Ambiguous_input
 exception DisambiguationError of
  int * (Token.flocation option * string Lazy.t) list list
 
+(** initially false; for debugging only (???) *)
+val only_one_pass: bool ref
+
 type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list
 type choose_interp_callback = 
   string -> int -> (Token.flocation list * string * string) list list -> 

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index 5d22f85d579f8aa9f15b2e1e27a7ab061f1e8f5c..58b7de9f34c2a9f02d94b39cc0ac589e5d0ecc8d 100644 (file)
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -170,6 +170,11 @@ let _ =
         CicNotation.set_active_notations
           (List.map fst (CicNotation.get_all_notations ())));
     addDebugSeparator ();
+    addDebugItem "enable multiple disambiguation passes (default)"
+      (fun _ -> GrafiteDisambiguator.only_one_pass := false);
+    addDebugItem "enable only one disambiguation pass"
+      (fun _ -> GrafiteDisambiguator.only_one_pass := true);
+    addDebugSeparator ();
     addDebugItem "enable coercions hiding"
       (fun _ -> TermAcicContent.hide_coercions := true);
     addDebugItem "disable coercions hiding"