X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=6b1f24743295df187a4d625afa5822e7180b84be;hb=988788642009674995382eed87606faca201ac1c;hp=a9faa592e8de974b5ce3192a81eacf22f556ac0c;hpb=fa6addea4fa1f37567dca9104164710870a50392;p=helm.git diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index a9faa592e..6b1f24743 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -84,17 +84,12 @@ let ask_and_save_moo_if_needed parent fname lexicon_status grafite_status = LibraryMisc.obj_file_of_baseuri ~must_exist:false ~baseuri ~writable:true in let save () = - let metadata_fname = - LibraryMisc.metadata_file_of_baseuri - ~must_exist:false ~baseuri ~writable:true in let lexicon_fname = LibraryMisc.lexicon_file_of_baseuri ~must_exist:false ~baseuri ~writable:true in GrafiteMarshal.save_moo moo_fname grafite_status.GrafiteTypes.moo_content_rev; - LibraryNoDb.save_metadata metadata_fname - lexicon_status.LexiconEngine.metadata; LexiconMarshal.save_lexicon lexicon_fname lexicon_status.LexiconEngine.lexicon_content_rev in @@ -232,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." ; @@ -266,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]] -> @@ -434,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 () @@ -780,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 () @@ -788,7 +720,9 @@ class gui () = notify_exn exc; unlock_world () in - worker_thread := Some (Thread.create thread_main ()) in + (*thread_main ();*) + worker_thread := Some (Thread.create thread_main ()) + in let kill_worker = (* the following lines are from Xavier Leroy: http://alan.petitepomme.net/cwn/2005.11.08.html *) let interrupt = ref None in @@ -863,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 @@ -871,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 -> () @@ -894,6 +831,8 @@ class gui () = | None -> true | Some path -> let is_prefix_of d1 d2 = + let d1 = MatitamakeLib.normalize_path d1 in + let d2 = MatitamakeLib.normalize_path d2 in let len1 = String.length d1 in let len2 = String.length d2 in if len2 < len1 then @@ -965,53 +904,13 @@ class gui () = ignore (adj#connect#changed (fun _ -> adj#set_value (adj#upper -. adj#page_size))); console#message (sprintf "\tMatita version %s\n" BuildTimeConf.version); - (* toolbar *) - let module A = GrafiteAst in - let hole = CicNotationPt.UserInput in - let loc = HExtlib.dummy_floc in - let tac ast _ = - if (MatitaScript.current ())#onGoingProof () then - (MatitaScript.current ())#advance - ~statement:("\n" - ^ GrafiteAstPp.pp_tactical ~term_pp:CicNotationPp.pp_term - ~lazy_term_pp:CicNotationPp.pp_term (A.Tactic (loc, ast))) - () - in - let tac_w_term ast _ = - if (MatitaScript.current ())#onGoingProof () then - let buf = source_buffer in - buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked")) - ("\n" - ^ GrafiteAstPp.pp_tactic ~term_pp:CicNotationPp.pp_term - ~lazy_term_pp:CicNotationPp.pp_term ast) - in - let tbar = main in - connect_button tbar#introsButton (tac (A.Intros (loc, None, []))); - connect_button tbar#applyButton (tac_w_term (A.Apply (loc, hole))); - connect_button tbar#exactButton (tac_w_term (A.Exact (loc, hole))); - connect_button tbar#elimButton (tac_w_term - (A.Elim (loc, hole, None, None, []))); - connect_button tbar#elimTypeButton (tac_w_term - (A.ElimType (loc, hole, None, None, []))); - connect_button tbar#splitButton (tac (A.Split loc)); - connect_button tbar#leftButton (tac (A.Left loc)); - connect_button tbar#rightButton (tac (A.Right loc)); - connect_button tbar#existsButton (tac (A.Exists loc)); - connect_button tbar#reflexivityButton (tac (A.Reflexivity loc)); - connect_button tbar#symmetryButton (tac (A.Symmetry loc)); - connect_button tbar#transitivityButton - (tac_w_term (A.Transitivity (loc, hole))); - connect_button tbar#assumptionButton (tac (A.Assumption loc)); - connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole))); - connect_button tbar#autoButton (tac (A.Auto (loc,[]))); - MatitaGtkMisc.toggle_widget_visibility - ~widget:(main#tacticsButtonsHandlebox :> GObj.widget) - ~check:main#tacticsBarMenuItem; + (* TO BE REMOVED *) + main#tacticsButtonsHandlebox#misc#hide (); + main#tacticsBarMenuItem#misc#hide (); + main#scriptNotebook#remove_page 1; + main#scriptNotebook#set_show_tabs false; + (* / TO BE REMOVED *) let module Hr = Helm_registry in - if - not (Hr.get_opt_default Hr.bool ~default:false "matita.tactics_bar") - then - main#tacticsBarMenuItem#set_active false; MatitaGtkMisc.toggle_callback ~check:main#fullscreenMenuItem ~callback:(function | true -> main#toplevel#fullscreen () @@ -1029,8 +928,6 @@ class gui () = MatitaGtkMisc.toggle_callback ~check:main#unicodeAsTexMenuItem ~callback:(fun enabled -> Helm_registry.set_bool "matita.paste_unicode_as_tex" enabled); - if not (Helm_registry.has "matita.paste_unicode_as_tex") then - Helm_registry.set_bool "matita.paste_unicode_as_tex" true; main#unicodeAsTexMenuItem#set_active (Helm_registry.get_bool "matita.paste_unicode_as_tex"); (* log *) @@ -1177,14 +1074,23 @@ class gui () = connect_menu_item main#saveMenuItem saveScript; connect_menu_item main#saveAsMenuItem saveAsScript; connect_menu_item main#newMenuItem newScript; + connect_menu_item main#showCoercionsGraphMenuItem + (fun _ -> + let c = MatitaMathView.cicBrowser () in + c#load (`About `Coercions)); + connect_menu_item main#showAutoGuiMenuItem + (fun _ -> MatitaAutoGui.auto_dialog Auto.get_auto_status); (* script monospace font stuff *) 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 *) @@ -1416,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;