X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=99b623b0f00c037d768b7b8d8033b99ba65d788b;hb=e57099824bce7206a8d60c2b05ced28f4e90933a;hp=8eb54bb70c03e8e7f939b67737b30a003a04d35e;hpb=aff2feccb7a2f0dbed83c7b31874dc4694924c80;p=helm.git diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 8eb54bb70..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,31 +229,49 @@ 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 (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 = List.filter (fun (_env,_diff,_loc,_msg,significant) -> significant) in - if all_passes then errorll else + let annotated_errorll () = + List.rev + (snd + (List.fold_left (fun (pass,res) item -> pass+1,(pass+1,item)::res) (0,[]) + errorll)) in + if all_passes then annotated_errorll () else let safe_list_nth l n = try List.nth l n with Failure _ -> [] in (* We remove passes 1,2 and 5,6 *) let res = - []::[] - ::(remove_non_significant (safe_list_nth errorll 2)) - ::(remove_non_significant (safe_list_nth errorll 3)) - ::[]::[] + (1,[])::(2,[]) + ::(3,remove_non_significant (safe_list_nth errorll 2)) + ::(4,remove_non_significant (safe_list_nth errorll 3)) + ::(5,[])::(6,[])::[] in - if List.flatten res <> [] then res + if List.flatten (List.map snd res) <> [] then res else (* all errors (if any) are not significant: we keep them *) let res = - []::[] - ::(safe_list_nth errorll 2) - ::(safe_list_nth errorll 3) - ::[]::[] + (1,[])::(2,[]) + ::(3,(safe_list_nth errorll 2)) + ::(4,(safe_list_nth errorll 3)) + ::(5,[])::(6,[])::[] in - if List.flatten res <> [] then + if List.flatten (List.map snd res) <> [] then begin HLog.warn "All disambiguation errors are not significant. Showing them anyway." ; @@ -261,91 +281,10 @@ let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView. begin HLog.warn "No errors in phases 2 and 3. Showing all errors in all phases" ; - errorll + annotated_errorll () end in - let choices = - let pass = ref 0 in - List.flatten - (List.map - (fun l -> - incr pass; - List.map - (fun (env,diff,offset,msg,significant) -> - offset, [[!pass], [[!pass], env, diff], msg, significant]) l - ) errorll') in - (* Here we are doing a stable sort and list_uniq returns the latter - "equal" element. I.e. we are showing the error corresponding to the - most advanced disambiguation pass *) - let choices = - let choices_compare (o1,_) (o2,_) = compare o1 o2 in - let choices_compare_by_passes (p1,_,_,_) (p2,_,_,_) = - compare p1 p2 in - let rec uniq = - function - [] -> [] - | h::[] -> [h] - | (o1,res1)::(o2,res2)::tl when o1 = o2 -> - let merge_by_name errors = - let merge_by_env errors = - let choices_compare_by_env (_,e1,_) (_,e2,_) = compare e1 e2 in - let choices_compare_by_passes (p1,_,_) (p2,_,_) = - compare p1 p2 in - let rec uniq_by_env = - function - [] -> [] - | h::[] -> [h] - | (p1,e1,_)::(p2,e2,d2)::tl when e1 = e2 -> - uniq_by_env ((p1@p2,e2,d2) :: tl) - | h1::tl -> h1 :: uniq_by_env tl - in - List.sort choices_compare_by_passes - (uniq_by_env (List.stable_sort choices_compare_by_env errors)) - in - let choices_compare_by_msg (_,_,m1,_) (_,_,m2,_) = - compare (Lazy.force m1) (Lazy.force m2) in - let rec uniq_by_msg = - function - [] -> [] - | h::[] -> [h] - | (p1,i1,m1,s1)::(p2,i2,m2,s2)::tl - when Lazy.force m1 = Lazy.force m2 && s1 = s2 -> - uniq_by_msg ((p1@p2,merge_by_env (i1@i2),m2,s2) :: tl) - | h1::tl -> h1 :: uniq_by_msg tl - in - List.sort choices_compare_by_msg - (uniq_by_msg (List.stable_sort choices_compare_by_msg errors)) - in - let res = merge_by_name (res1@res2) in - uniq ((o1,res) :: tl) - | h1::tl -> h1 :: uniq tl - in - (* Errors in phase 3 that are not also in phase 4 are filtered out *) - let filter_phase_3 choices = - if all_passes then choices - else - let filter = - HExtlib.filter_map - (function - (loffset,messages) -> - let filtered_messages = - HExtlib.filter_map - (function - [3],_,_,_ -> None - | item -> Some item - ) messages - in - if filtered_messages = [] then - None - else - Some (loffset,filtered_messages)) - in - filter choices - in - filter_phase_3 - (List.map (fun o,l -> o,List.sort choices_compare_by_passes l) - (uniq (List.stable_sort choices_compare choices))) - in + let choices = MatitaExcPp.compact_disambiguation_errors all_passes errorll' in match choices with [] -> assert false | [loffset,[_,envs_and_diffs,msg,significant]] -> @@ -429,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); + interactive_error_interp ~all_passes:true source_buffer + notify_exn offset errorll script_fname); connect_button dialog#disambiguationErrorsCancelButton fail; dialog#disambiguationErrors#show (); GtkThread.main () @@ -774,8 +713,8 @@ class gui () = with | GrafiteDisambiguator.DisambiguationError (offset,errorll) -> (try - interactive_error_interp source_buffer notify_exn offset - errorll + interactive_error_interp ~all_passes:!all_disambiguation_passes source_buffer + notify_exn offset errorll script_fname with exc -> notify_exn exc); unlock_world ()