no more prove in palette

[helm.git] / helm / software / matita / matitaGui.ml

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index a77800c1e05192395e141aa075a5e361dde61944..84909e95bd99d12738cec8c54f1e1fcac128ea36 100644 (file)
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -754,9 +754,48 @@ 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#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 +882,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 +1175,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 +1209,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
@@ -1232,7 +1274,8 @@ class gui () =
 
     method private updateFontSize () =
       self#sourceView#misc#modify_font_by_name
-        (sprintf "%s %d" BuildTimeConf.script_font font_size)
+        (sprintf "%s %d" BuildTimeConf.script_font font_size);
+      MatitaAutoGui.set_font_size font_size
 
     method increaseFontSize () =
       font_size <- font_size + 1;
@@ -1376,9 +1419,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 gui = instance () in
     let dialog = gui#newUriDialog () in
     dialog#uriEntryHBox#misc#hide ();
@@ -1394,13 +1438,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 ^ "<b>" ^ str2 ^ "</b>" ^ colorize stop tl
+          escape_pango_markup str1 ^ "<b>" ^ 
+          escape_pango_markup str2 ^ "</b>" ^ 
+          colorize stop tl
     in
 (*     List.iter (fun l -> let start, stop = HExtlib.loc_of_floc l in
                 Printf.eprintf "(%d,%d)" start stop) locs; *)
@@ -1419,6 +1465,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 =