X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=db26ba20a55d7575e54f6b9932e5c0d71aa1404e;hb=1118162fa2c7b4dc860da0c3aa434bd2a1631855;hp=9e8cfd86cd4c3163be5906acf735fd63df9d9c0f;hpb=9e1d0c4f6ddf36cd691ef0d3c95aaa7f694977f0;p=helm.git
diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 9e8cfd86c..db26ba20a 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -754,9 +754,50 @@ 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");
+
+
+ (* TO BE REMOVED *)
main#scriptNotebook#remove_page 1;
main#scriptNotebook#set_show_tabs false;
(* / TO BE REMOVED *)
@@ -843,6 +884,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 +1177,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 +1211,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 +1421,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 +1440,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 +1467,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 =