From 5bc000d9a2e8e41db58d610f3221270add686888 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 25 May 2006 12:05:58 +0000 Subject: [PATCH] Added debug menu item to restrict disambiguation to the first pass only. --- .../components/grafite_parser/grafiteDisambiguator.ml | 7 ++++++- .../components/grafite_parser/grafiteDisambiguator.mli | 3 +++ helm/software/matita/matita.ml | 5 +++++ 3 files changed, 14 insertions(+), 1 deletion(-) diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.ml b/helm/software/components/grafite_parser/grafiteDisambiguator.ml index d9de808b0..05c988ac1 100644 --- 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 = (* *) + let passes = (* *) + 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 b70eb737f..52add3974 100644 --- 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 5d22f85d5..58b7de9f3 100644 --- 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" -- 2.39.2