Patch to automatically generate filename.error.md5.ma scripts every time a

disambiguation error is faced by the user.

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index f4024c3cbad5a72cece6c125a721184efe3e17fc..de98b49b8526b0a9ce3de21eb2e86489c0e255b4 100644 (file)
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -227,8 +227,21 @@ class interpErrorModel =
     end
 
 
-let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.source_buffer) notify_exn offset errorll
+let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.source_buffer) notify_exn offset errorll script_fname
 = 
+  (* hook to save a script for each disambiguation error *)
+  if false then
+   (let text =
+     source_buffer#get_text ~start:source_buffer#start_iter
+      ~stop:source_buffer#end_iter () in
+    let md5 = Digest.to_hex (Digest.string text) in
+    let filename = match script_fname with Some s -> s | None -> "unnamed.ma" in
+    let filename =
+     Filename.chop_extension filename ^ ".error." ^ md5 ^ ".ma"  in
+    let ch = open_out filename in
+     output_string ch text;
+    close_out ch
+   );
   assert (List.flatten errorll <> []);
   let errorll' =
    let remove_non_significant =
@@ -432,8 +445,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);
+          interactive_error_interp ~all_passes:true source_buffer notify_exn
+           offset errorll script_fname);
        connect_button dialog#disambiguationErrorsCancelButton fail;
        dialog#disambiguationErrors#show ();
        GtkThread.main ()
@@ -778,7 +791,7 @@ class gui () =
            | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
               (try
                 interactive_error_interp source_buffer notify_exn offset
-                 errorll
+                 errorll script_fname
                with
                 exc -> notify_exn exc);
               unlock_world ()