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 *)
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 -> ()
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
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