X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=8bc226ed4a4bdbbbf33292d7afaa3a4f75c6f406;hb=424982ded255df68245241f56064202844ed1194;hp=9e8cfd86cd4c3163be5906acf735fd63df9d9c0f;hpb=9e1d0c4f6ddf36cd691ef0d3c95aaa7f694977f0;p=helm.git diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 9e8cfd86c..8bc226ed4 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -754,9 +754,60 @@ class gui () = ignore (adj#connect#changed (fun _ -> adj#set_value (adj#upper -. adj#page_size))); console#message (sprintf "\tMatita version %s\n" BuildTimeConf.version); - (* TO BE REMOVED *) + (* natural deduction palette *) main#tacticsButtonsHandlebox#misc#hide (); - main#tacticsBarMenuItem#misc#hide (); + MatitaGtkMisc.toggle_callback + ~callback:(fun b -> + if b then main#tacticsButtonsHandlebox#misc#show () + else main#tacticsButtonsHandlebox#misc#hide ()) + ~check:main#menuitemPalette; + connect_button main#butImpl_intro + (fun () -> source_buffer#insert "apply rule (⇒_i […] (…));\n"); + connect_button main#butAnd_intro + (fun () -> source_buffer#insert + "apply rule (∧_i (…) (…));\n\t[\n\t|\n\t]\n"); + connect_button main#butOr_intro_left + (fun () -> source_buffer#insert "apply rule (∨_i_l (…));\n"); + connect_button main#butOr_intro_right + (fun () -> source_buffer#insert "apply rule (∨_i_r (…));\n"); + connect_button main#butNot_intro + (fun () -> source_buffer#insert "apply rule (¬_i […] (…));\n"); + connect_button main#butTop_intro + (fun () -> source_buffer#insert "apply rule (⊤_i);\n"); + connect_button main#butImpl_elim + (fun () -> source_buffer#insert + "apply rule (⇒_e (…) (…));\n\t[\n\t|\n\t]\n"); + connect_button main#butAnd_elim_left + (fun () -> source_buffer#insert "apply rule (∧_e_l (…));\n"); + connect_button main#butAnd_elim_right + (fun () -> source_buffer#insert "apply rule (∧_e_r (…));\n"); + connect_button main#butOr_elim + (fun () -> source_buffer#insert + "apply rule (∨_e (…) […] (…) […] (…));\n\t[\n\t|\n\t|\n\t]\n"); + connect_button main#butNot_elim + (fun () -> source_buffer#insert + "apply rule (¬_e (…) (…));\n\t[\n\t|\n\t]\n"); + connect_button main#butBot_elim + (fun () -> source_buffer#insert "apply rule (⊥_e (…));\n"); + connect_button main#butRAA + (fun () -> source_buffer#insert "apply rule (RAA […] (…));\n"); + connect_button main#butUseLemma + (fun () -> source_buffer#insert "apply rule (lem …);\n"); + connect_button main#butDischarge + (fun () -> source_buffer#insert "apply rule (discharge […]);\n"); + + connect_button main#butForall_intro + (fun () -> source_buffer#insert "apply rule (∀_i {…} (…));\n"); + connect_button main#butForall_elim + (fun () -> source_buffer#insert "apply rule (∀_e {…} (…));\n"); + connect_button main#butExists_intro + (fun () -> source_buffer#insert "apply rule (∃_i {…} (…));\n"); + connect_button main#butExists_elim + (fun () -> source_buffer#insert + "apply rule (∃_e (…) {…} […] (…));\n\t[\n\t|\n\t]\n"); + + + (* TO BE REMOVED *) main#scriptNotebook#remove_page 1; main#scriptNotebook#set_show_tabs false; (* / TO BE REMOVED *) @@ -843,6 +894,8 @@ class gui () = source_view#source_buffer#begin_not_undoable_action (); script#loadFromFile f; source_view#source_buffer#end_not_undoable_action (); + source_view#buffer#move_mark `INSERT source_view#buffer#start_iter; + source_view#buffer#place_cursor source_view#buffer#start_iter; console#message ("'"^f^"' loaded.\n"); self#_enableSaveTo f | None -> () @@ -1134,6 +1187,8 @@ class gui () = source_view#source_buffer#begin_not_undoable_action (); script#loadFromFile content; source_view#source_buffer#end_not_undoable_action (); + source_view#buffer#move_mark `INSERT source_view#buffer#start_iter; + source_view#buffer#place_cursor source_view#buffer#start_iter; console#message ("'"^file^"' loaded."); self#_enableSaveTo file @@ -1166,7 +1221,6 @@ class gui () = self#check_widgets (); let combo_widget = combo#coerce in uriHBox#pack ~from:`END ~fill:true ~expand:true combo_widget; - self#toplevel#set_transient_for main#toplevel#as_window; combo#misc#grab_focus () method browserUri = combo end @@ -1377,14 +1431,10 @@ class interpModel = tree_store#get ~row:iter ~column:interp_no_col end + let interactive_string_choice text prefix_len ?(title = "") ?(msg = "") () ~id locs uris = - - let text = Pcre.replace ~pat:"<" ~templ:"<" text in - let text = Pcre.replace ~pat:"'" ~templ:"'" text in - let text = Pcre.replace ~pat:"\"" ~templ:""" text in - let text = Pcre.replace ~pat:">" ~templ:">" text in let gui = instance () in let dialog = gui#newUriDialog () in dialog#uriEntryHBox#misc#hide (); @@ -1400,13 +1450,15 @@ let interactive_string_choice let rec colorize acc_len = function | [] -> let floc = HExtlib.floc_of_loc (acc_len,hack_len) in - fst(MatitaGtkMisc.utf8_parsed_text text floc) + escape_pango_markup (fst(MatitaGtkMisc.utf8_parsed_text text floc)) | he::tl -> let start, stop = HExtlib.loc_of_floc he in let floc1 = HExtlib.floc_of_loc (acc_len,start) in let str1,_=MatitaGtkMisc.utf8_parsed_text text floc1 in let str2,_ = MatitaGtkMisc.utf8_parsed_text text he in - str1 ^ "" ^ str2 ^ "" ^ colorize stop tl + escape_pango_markup str1 ^ "" ^ + escape_pango_markup str2 ^ "" ^ + colorize stop tl in (* List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in Printf.eprintf "(%d,%d)" start stop) locs; *) @@ -1425,6 +1477,7 @@ let interactive_string_choice let txt,_ = MatitaGtkMisc.utf8_parsed_text txt (HExtlib.floc_of_loc (prefix_len,MatitaGtkMisc.utf8_string_length txt)) in + prerr_endline ("txt:" ^ txt); dialog#uriChoiceLabel#set_label txt; List.iter model#easy_append uris; let return v =