From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 26 Nov 2007 10:22:36 +0000 (+0000)
Subject: Patch to automatically generate filename.error.md5.ma scripts every time a
X-Git-Tag: make_still_working~5782
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=816ee790efa658355907a90f0532eed4ba6244d5;p=helm.git

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 f4024c3cb..de98b49b8 100644
--- 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 ()