weight -> value

[helm.git] / helm / software / matita / matitaGui.ml

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 ()