X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=6b1f24743295df187a4d625afa5822e7180b84be;hb=3a5b9647787e1402f6886d41824f664db290963f;hp=5bab5ab0ab4dcad44763fca84578cbe89c966ea8;hpb=b74ef6550e31214a340dfeae67ce77d055e9827c;p=helm.git diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 5bab5ab0a..6b1f24743 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -227,31 +227,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=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 = 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 +279,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 +366,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 () @@ -775,7 +712,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 () @@ -860,6 +797,7 @@ class gui () = (fun () -> MatitamakeLib.clean_development_in_bg refresh d) in ignore(clean ()))); + (* publish button hidden, use command line connect_button develList#publishButton (locker (fun () -> match get_devel_selected () with @@ -868,6 +806,8 @@ class gui () = let publish = locker (fun () -> MatitamakeLib.publish_development_in_bg refresh d) in ignore(publish ()))); + *) + develList#publishButton#misc#hide (); connect_button develList#graphButton (fun () -> match get_devel_selected () with | None -> () @@ -1144,10 +1084,13 @@ class gui () = self#updateFontSize (); (* debug menu *) main#debugMenu#misc#hide (); - (* status bar *) + (* HBUGS *) + main#hintNotebook#misc#hide (); + (* main#hintLowImage#set_file (image_path "matita-bulb-low.png"); main#hintMediumImage#set_file (image_path "matita-bulb-medium.png"); main#hintHighImage#set_file (image_path "matita-bulb-high.png"); + *) (* focus *) self#sourceView#misc#grab_focus (); (* main win dimension *) @@ -1379,11 +1322,13 @@ class gui () = end method setStar name b = - let l = main#scriptLabel in + let w = main#toplevel in + let set x = w#set_title x in + let name = "Matita - " ^ name in if b then - l#set_text (name ^ " *") + set (name ^ " *") else - l#set_text (name) + set (name) method private _enableSaveTo file = script_fname <- Some file;