Added debugging option to ask for all disambiguation errors (even spurious ones)...

diff --git a/helm/software/matita/matita.ml b/helm/software/matita/matita.ml
index a326754dc40a39ac65ad30df18e795f4d64eae95..60b112d982cca6bf9e6c75ae77d935d6f3114195 100644 (file)
--- 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 6b1f24743295df187a4d625afa5822e7180b84be..99b623b0f00c037d768b7b8d8033b99ba65d788b 100644 (file)
--- 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 8c9064e1da3a49e79e4f9447b6c038e9d20732c0..388c79e1a74dd903372c72716dd7da57d191e6bb 100644 (file)
--- 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