From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 4 Dec 2007 17:17:04 +0000 (+0000)
Subject: Added debugging option to ask for all disambiguation errors (even spurious ones)... 
X-Git-Tag: make_still_working~5731
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=31c099c46eba26ee5ace403fb2cc0a68616bb887;p=helm.git

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

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