From 31c099c46eba26ee5ace403fb2cc0a68616bb887 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 4 Dec 2007 17:17:04 +0000
Subject: [PATCH] Added debugging option to ask for all disambiguation errors
 (even spurious ones) in all passes.

---
 helm/software/matita/matita.ml     |  4 ++++
 helm/software/matita/matitaGui.ml  | 12 +++++++-----
 helm/software/matita/matitaGui.mli |  3 +++
 3 files changed, 14 insertions(+), 5 deletions(-)

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index a326754dc..60b112d98 100644
--- a/helm/software/matita/matita.ml
+++ b/helm/software/matita/matita.ml
@@ -233,6 +233,10 @@ let _ =
       (fun _ -> GrafiteDisambiguator.only_one_pass := false);
     addDebugItem "enable only one disambiguation pass"
       (fun _ -> GrafiteDisambiguator.only_one_pass := true);
+    addDebugItem "always show all disambiguation errors"
+      (fun _ -> MatitaGui.all_disambiguation_passes := true);
+    addDebugItem "prune disambiguation errors"
+      (fun _ -> MatitaGui.all_disambiguation_passes := false);
     addDebugSeparator ();
 (* ZACK moved to the View menu
     addDebugItem "enable coercions hiding"
diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 6b1f24743..99b623b0f 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -33,6 +33,8 @@ open MatitaMisc
 
 exception Found of int
 
+let all_disambiguation_passes = ref false
+
 let gui_instance = ref None
 
 class type browserWin =
@@ -227,7 +229,7 @@ class interpErrorModel =
     end
 
 
-let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.source_buffer) notify_exn offset errorll script_fname
+let rec interactive_error_interp ~all_passes (source_buffer:GSourceView.source_buffer) notify_exn offset errorll script_fname
 = 
   (* hook to save a script for each disambiguation error *)
   if false then
@@ -366,8 +368,8 @@ let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.
         );
        connect_button dialog#disambiguationErrorsMoreErrors
         (fun _ -> return () ;
-          interactive_error_interp ~all_passes:true source_buffer notify_exn
-           offset errorll script_fname);
+          interactive_error_interp ~all_passes:true source_buffer
+           notify_exn offset errorll script_fname);
        connect_button dialog#disambiguationErrorsCancelButton fail;
        dialog#disambiguationErrors#show ();
        GtkThread.main ()
@@ -711,8 +713,8 @@ class gui () =
           with
            | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
               (try
-                interactive_error_interp source_buffer notify_exn offset
-                 errorll script_fname
+                interactive_error_interp ~all_passes:!all_disambiguation_passes source_buffer
+                 notify_exn offset errorll script_fname
                with
                 exc -> notify_exn exc);
               unlock_world ()
diff --git a/helm/software/matita/matitaGui.mli b/helm/software/matita/matitaGui.mli
index 8c9064e1d..388c79e1a 100644
--- a/helm/software/matita/matitaGui.mli
+++ b/helm/software/matita/matitaGui.mli
@@ -23,6 +23,9 @@
  * http://helm.cs.unibo.it/
  *)
 
+  (** for debugging only *)
+val all_disambiguation_passes: bool ref
+
   (** singleton instance of the gui *)
 val instance: unit -> MatitaGuiTypes.gui
 
-- 
2.39.2