From 816ee790efa658355907a90f0532eed4ba6244d5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 26 Nov 2007 10:22:36 +0000 Subject: [PATCH] Patch to automatically generate filename.error.md5.ma scripts every time a disambiguation error is faced by the user. --- helm/software/matita/matitaGui.ml | 21 +++++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) 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 () -- 2.39.2