bug de preferencs/font"

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5076 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 80 insertions, 63 deletions

diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index d51521ff71..1907025817 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -9,7 +9,7 @@
 (* $Id$ *)
 
 let commands = [
-  ["Abort";
+  [(* "Abort"; *)
    "Add Abstract Ring";
    "Add Abstract Semi Ring";
    "Add Field";
@@ -30,12 +30,12 @@ let commands = [
   ["Canonical Structure";
    "Cd";
    "Chapter";
-   "Check";
+   (* "Check"; *)
    "Coercion";
    "Coercion Local";
    "CoFixpoint";
    "CoInductive";
-   "Correctness";];
+   (* "Correctness"; *)];
   ["Declare ML Module";
    "Defined";
    "Definition";
@@ -43,10 +43,10 @@ let commands = [
    "Derive Dependent Inversion_clear";
    "Derive Inversion";
    "Derive Inversion_clear";
-   "Drop";];
+   (* "Drop"; *)];
   ["End";
    "End Silent";
-   "Eval";
+   "Eval"; 
    "Explicitation of implicit arguments";
    "Extract Constant";
    "Extract Inductive";
@@ -93,7 +93,7 @@ let commands = [
   ["Notation";];
   ["Opaque";];
   ["Parameter";
-   "Print";
+   (*"Print";
    "Print All";
    "Print Classes";
    "Print Coercion Paths";
@@ -111,11 +111,11 @@ let commands = [
    "Print Proof";
    "Print Section";
    "Print Table Printing If";
-   "Print Table Printing Let";
+   "Print Table Printing Let";*)
    "Proof";
-   "Pwd";];
+   (*"Pwd";*)];
   ["Qed";
-   "Quit";];
+   (* "Quit";*)];
   ["Read Module";
    "Record";
    "Recursive Extraction";
@@ -126,15 +126,15 @@ let commands = [
    "Remove Printing Let";
    "Require";
    "Require Export";
-   "Reset";
+   (* "Reset"; *)
    "Reset Extraction Inline";
-   "Reset Initial";
-   "Restart";
+   (* "Reset Initial"; *)
+   (* "Restart"; *)
    "Restore State";
    "Resume";];
   [  "Save";
      "Scheme";
-     "Search";
+     (*"Search";
      "Search ... inside ...";
      "Search ... outside ...";
      "SearchAbout";
@@ -143,7 +143,7 @@ let commands = [
      "SearchPattern ... outside ...";
      "SearchRewrite";
      "SearchRewrite ... inside ...";
-     "SearchRewrite ... outside ...";
+     "SearchRewrite ... outside ..."; *)
      "Section";
      "Set Extraction AutoInline";
      "Set Extraction Optimize";
@@ -154,7 +154,7 @@ let commands = [
      "Set Printing Synth";
      "Set Printing Wildcard";
      "Set Undo";
-     "Show";
+     (*"Show";
      "Show Conjectures";
      "Show Implicits";
      "Show Intro";
@@ -162,9 +162,9 @@ let commands = [
      "Show Programs";
      "Show Proof";
      "Show Script";
-     "Show Tree";
+     "Show Tree";*)
      "Structure";
-     "Suspend";
+     (* "Suspend"; *)
      "Syntactic Definition";
      "Syntax";];
   ["Tactic Definition";
@@ -175,7 +175,7 @@ let commands = [
    "Theorem";
    "Time";
    "Transparent";];
-  ["Undo";
+  [(* "Undo"; *)
    "Unfocus";
    "Unset Extraction AutoInline";
    "Unset Extraction Optimize";
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 72cf9d6348..0239e2340a 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -2202,12 +2202,6 @@ let main files =
 	      ~callback
 	      ())
   in
-  add_to_menu_toolbar "_Interrupt"
-    ~tooltip:"Interrupt computations"    
-    ~key:GdkKeysyms._Break 
-    ~callback:break
-    `STOP
-  ;
   add_to_menu_toolbar 
     "_Forward" 
     ~tooltip:"Forward one command" 
@@ -2251,6 +2245,12 @@ let main files =
     ~key:GdkKeysyms._End
     ~callback:(do_or_activate (fun a -> a#process_until_end_or_error))
     `GOTO_BOTTOM;
+  add_to_menu_toolbar "_Interrupt"
+    ~tooltip:"Interrupt computations"    
+    ~key:GdkKeysyms._Break 
+    ~callback:break
+    `STOP
+  ;
 
   (* Tactics Menu *)
   let tactics_menu =  factory#add_submenu "_Try Tactics" in
@@ -2371,41 +2371,43 @@ let main files =
   add_complex_template 
     ("_Inductive __", "Inductive ident : :=\n  | : .\n",
      14, 5, Some GdkKeysyms._I);
+  add_complex_template 
+    ("_Fixpoint __", "Fixpoint ident (_ : _) {struct _} : _ :=\n.\n",
+     29, 5, Some GdkKeysyms._F);
   add_complex_template("_Scheme __",
 		       "Scheme new_scheme := Induction for _ Sort _
 with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 
   (* Template for match *)
-  let callback = (fun () -> 
-		    let w = get_current_word () in
-		    try 
-		      let cases = Coq.make_cases w
-		      in
-		      let print c = function
-			| [x] -> fprintf c "  | %s => _@\n" x
-			| x::l -> fprintf c "  | (%s%a) => _@\n" x 
-			    (print_list (fun c s -> fprintf c " %s" s)) l
-			| [] -> assert false
-		      in
-		      let b = Buffer.create 1024 in
-		      let fmt = formatter_of_buffer b in
-		      fprintf fmt "@[match var with@\n%aend@]@."
-			(print_list print) cases;
-		      let s = Buffer.contents b in
-		      prerr_endline s;
-		      let {view = view } = get_current_view () in
-		      ignore (view#buffer#delete_selection ());
-		      let m = view#buffer#create_mark 
-				(view#buffer#get_iter `INSERT)
-		      in
-		      if view#buffer#insert_interactive s then 
-			let i = view#buffer#get_iter (`MARK m) in
-			let _ = i#nocopy#forward_chars 9 in
-			view#buffer#place_cursor i;
-			view#buffer#move_mark ~where:(i#backward_chars 3)
-			  `SEL_BOUND 
-		    with Not_found -> !flash_info "Not an inductive type"
-		 )
+  let callback () = 
+    let w = get_current_word () in
+    try 
+      let cases = Coq.make_cases w
+      in
+      let print c = function
+	| [x] -> fprintf c "  | %s => _@\n" x
+	| x::l -> fprintf c "  | (%s%a) => _@\n" x 
+	      (print_list (fun c s -> fprintf c " %s" s)) l
+	| [] -> assert false
+      in
+      let b = Buffer.create 1024 in
+      let fmt = formatter_of_buffer b in
+      fprintf fmt "@[match var with@\n%aend@]@."
+	(print_list print) cases;
+      let s = Buffer.contents b in
+      prerr_endline s;
+      let {view = view } = get_current_view () in
+      ignore (view#buffer#delete_selection ());
+      let m = view#buffer#create_mark 
+		(view#buffer#get_iter `INSERT)
+      in
+      if view#buffer#insert_interactive s then 
+	let i = view#buffer#get_iter (`MARK m) in
+      let _ = i#nocopy#forward_chars 9 in
+      view#buffer#place_cursor i;
+      view#buffer#move_mark ~where:(i#backward_chars 3)
+	`SEL_BOUND 
+    with Not_found -> !flash_info "Not an inductive type"
   in
   ignore (templates_factory#add_item "match ..."
 	    ~key:GdkKeysyms._C
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 64bb9c4888..bda3569943 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -266,7 +266,10 @@ let load_pref () =
     set_int "query_window_width" (fun v -> np.query_window_width <- v);
     set_int "query_window_height" (fun v -> np.query_window_height <- v);
     set_bool "auto_complete" (fun v -> np.auto_complete <- v);
-    current := np
+    current := np;
+(*
+    Format.printf "in laod_pref: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
+*)
   with e -> 
     prerr_endline ("Could not load preferences ("^
 		   (Printexc.to_string e)^").")
@@ -300,6 +303,9 @@ let configure () =
       (fun () -> 
 	 let fd =  w#font_name in
 	 !current.text_font <- (Pango.Font.from_string fd) ; 
+(*
+	 Format.printf "in config_font: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
+*)
 	 !change_font !current.text_font)
       true
   in
@@ -473,14 +479,16 @@ let configure () =
 
   let misc = [contextual_menus_on_goal;auto_complete] in
    
+(* ATTENTION !!!!! L'onglet Fonts doit etre en premier pour eviter un bug !!!!
+   (shame on Benjamin) *)
   let cmds =
-    [Section("Files",
-	     [global_auto_revert;global_auto_revert_delay;
-	     auto_save; auto_save_delay; (* auto_save_name*)
-	     encodings;
-	     ]);
-     Section("Fonts",
+    [Section("Fonts",
 	     [config_font]);
+     Section("Files",
+	     [global_auto_revert;global_auto_revert_delay;
+	      auto_save; auto_save_delay; (* auto_save_name*)
+	      encodings;
+	     ]);     
 (*
      Section("Appearance",
 	     config_appearance);
@@ -496,7 +504,14 @@ let configure () =
      Section("Misc",
 	     misc)]
   in
-  match edit ~width:500 "Customizations" cmds
-  with 
+(*
+  Format.printf "before edit: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
+*)
+  let x = edit ~width:500 "Customizations" cmds in
+(*
+  Format.printf "after edit: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
+*)
+  match x with 
     | Return_apply | Return_ok -> save_pref ()
     | Return_cancel -> ()
+