Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

21 files changed, 651 insertions, 333 deletions

diff --git a/ide/command_windows.ml b/ide/command_windows.ml
index 939238d3..a34e5ebe 100644
--- a/ide/command_windows.ml
+++ b/ide/command_windows.ml
@@ -13,6 +13,7 @@ class command_window coqtop current =
 		 ~position:`CENTER
 		 ~title:"CoqIde queries" ~show:false ()
   in *)
+  let views = ref [] in
   let frame = GBin.frame ~label:"Command Pane" ~shadow_type:`IN () in
   let _ = frame#misc#hide () in
   let _ = GtkData.AccelGroup.create () in
@@ -49,12 +50,17 @@ class command_window coqtop current =
       ()
   in
 
+  let remove_cb () =
+    let index = notebook#current_page in
+    let () = notebook#remove_page index in
+    views := Minilib.list_filter_i (fun i x -> i <> index) !views
+  in
   let _ =
     toolbar#insert_button
       ~tooltip:"Delete Page"
       ~text:"Delete Page"
       ~icon:(Ideutils.stock_to_widget `DELETE)
-      ~callback:(fun () -> notebook#remove_page notebook#current_page)
+      ~callback:remove_cb
       ()
   in
 object(self)
@@ -63,14 +69,14 @@ object(self)
 
   val new_page_menu = new_page_menu
   val notebook = notebook
+
   method frame = frame
   method new_command ?command ?term () =
-    let appendp x = ignore (notebook#append_page x) in
     let frame = GBin.frame
 		  ~shadow_type:`ETCHED_OUT
-		  ~packing:appendp
 		  ()
     in
+    let _ = notebook#append_page frame#coerce in
     notebook#goto_page (notebook#page_num frame#coerce);
     let vbox = GPack.vbox ~homogeneous:false ~packing:frame#add () in
     let hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in
@@ -91,7 +97,10 @@ object(self)
 	~packing:(vbox#pack ~fill:true ~expand:true) () in
     let ok_b = GButton.button ~label:"Ok" ~packing:(hbox#pack ~expand:false) () in
     let result = GText.view ~packing:r_bin#add () in
+    let () = views := !views @ [result] in
     result#misc#modify_font !current.Preferences.text_font;
+    let clr = Tags.color_of_string !current.Preferences.background_color in
+    result#misc#modify_base [`NORMAL, `COLOR clr];
     result#misc#set_can_focus true; (* false causes problems for selection *)
     result#set_editable false;
     let callback () =
@@ -134,6 +143,15 @@ object(self)
     ignore (combo#entry#connect#activate ~callback);
     self#frame#misc#show ()
 
+  method refresh_font () =
+    let iter view = view#misc#modify_font !current.Preferences.text_font in
+    List.iter iter !views
+
+  method refresh_color () =
+    let clr = Tags.color_of_string !current.Preferences.background_color in
+    let iter view = view#misc#modify_base [`NORMAL, `COLOR clr] in
+    List.iter iter !views
+
   initializer
     ignore (new_page_menu#connect#clicked ~callback:self#new_command);
    (* ignore (window#event#connect#delete (fun _ -> window#misc#hide(); true));*)
diff --git a/ide/command_windows.mli b/ide/command_windows.mli
index 8c7319aa..c34b6cf6 100644
--- a/ide/command_windows.mli
+++ b/ide/command_windows.mli
@@ -11,4 +11,6 @@ class command_window :
   object
     method new_command : ?command:string -> ?term:string -> unit -> unit
     method frame : GBin.frame
+    method refresh_font : unit -> unit
+    method refresh_color : unit -> unit
   end
diff --git a/ide/coq.ml b/ide/coq.ml
index 16a07b01..76dc5650 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -54,36 +54,106 @@ let rec read_all_lines in_chan =
     arg::(read_all_lines in_chan)
   with End_of_file -> []
 
-let filter_coq_opts args =
+let fatal_error_popup msg =
+  let popup = GWindow.message_dialog ~buttons:GWindow.Buttons.ok
+    ~message_type:`ERROR ~message:msg ()
+  in ignore (popup#run ()); exit 1
+
+let final_info_popup small msg =
+  if small then
+    let popup = GWindow.message_dialog ~buttons:GWindow.Buttons.ok
+      ~message_type:`INFO ~message:msg ()
+    in
+    let _ = popup#run () in
+    exit 0
+  else
+    let popup = GWindow.dialog () in
+    let button = GButton.button ~label:"ok" ~packing:popup#action_area#add ()
+    in
+    let scroll = GBin.scrolled_window ~hpolicy:`NEVER ~vpolicy:`AUTOMATIC
+      ~packing:popup#vbox#add ~height:500 ()
+    in
+    let _ = GMisc.label ~text:msg ~packing:scroll#add_with_viewport () in
+    let _ = popup#connect#destroy ~callback:(fun _ -> exit 0) in
+    let _ = button#connect#clicked ~callback:(fun _ -> exit 0) in
+    let _ = popup#run () in
+    exit 0
+
+let connection_error cmd lines exn =
+  fatal_error_popup
+    ("Connection with coqtop failed!\n"^
+     "Command was: "^cmd^"\n"^
+     "Answer was: "^(String.concat "\n  " lines)^"\n"^
+     "Exception was: "^Printexc.to_string exn)
+
+let display_coqtop_answer cmd lines =
+  final_info_popup (List.length lines < 30)
+    ("Coqtop exited\n"^
+     "Command was: "^cmd^"\n"^
+     "Answer was: "^(String.concat "\n  " lines))
+
+let check_remaining_opt arg =
+  if arg <> "" && arg.[0] = '-' then fatal_error_popup ("Illegal option: "^arg)
+
+let rec filter_coq_opts args =
   let argstr = String.concat " " (List.map Filename.quote args) in
-  let cmd = Filename.quote !Minilib.coqtop_path ^" -nois -filteropts " ^ argstr in
-  let oc,ic,ec = Unix.open_process_full cmd (Unix.environment ()) in
-  let filtered_args = read_all_lines oc in
-  let message = read_all_lines ec in
-  match Unix.close_process_full (oc,ic,ec) with
-    | Unix.WEXITED 0 -> true,filtered_args
-    | Unix.WEXITED 2 -> false,filtered_args
-    | _ -> false,message
-
-exception Coqtop_output of string list
+  let cmd = Filename.quote (coqtop_path ()) ^" -nois -filteropts " ^ argstr in
+  let cmd = requote cmd in
+  let filtered_args = ref [] in
+  let errlines = ref [] in
+  try
+    let oc,ic,ec = Unix.open_process_full cmd (Unix.environment ()) in
+    filtered_args := read_all_lines oc;
+    errlines := read_all_lines ec;
+    match Unix.close_process_full (oc,ic,ec) with
+      | Unix.WEXITED 0 ->
+	List.iter check_remaining_opt !filtered_args; !filtered_args
+      | Unix.WEXITED 127 -> asks_for_coqtop args
+      | _ -> display_coqtop_answer cmd (!filtered_args @ !errlines)
+  with Sys_error _ -> asks_for_coqtop args
+    | e -> connection_error cmd (!filtered_args @ !errlines) e
+
+and asks_for_coqtop args =
+  let pb_mes = GWindow.message_dialog
+    ~message:"Failed to load coqtop. Reset the preference to default ?"
+    ~message_type:`QUESTION ~buttons:GWindow.Buttons.yes_no () in
+  match pb_mes#run () with
+    | `YES ->
+      let () = !Preferences.current.Preferences.cmd_coqtop  <- None in
+      let () = custom_coqtop := None in
+      let () = pb_mes#destroy () in
+      filter_coq_opts args
+    | `DELETE_EVENT | `NO ->
+      let () = pb_mes#destroy () in
+      let cmd_sel = GWindow.file_selection
+	~title:"Coqtop to execute (edit your preference then)"
+	~filename:(coqtop_path ()) ~urgency_hint:true () in
+      match cmd_sel#run () with
+	| `OK ->
+	  let () = custom_coqtop := (Some cmd_sel#filename) in
+	  let () = cmd_sel#destroy () in
+	  filter_coq_opts args
+	| `CANCEL | `DELETE_EVENT | `HELP -> exit 0
+
+exception WrongExitStatus of string
+
+let print_status = function
+  | Unix.WEXITED n -> "WEXITED "^string_of_int n
+  | Unix.WSIGNALED n -> "WSIGNALED "^string_of_int n
+  | Unix.WSTOPPED n -> "WSTOPPED "^string_of_int n
 
 let check_connection args =
+  let lines = ref [] in
+  let argstr = String.concat " " (List.map Filename.quote args) in
+  let cmd = Filename.quote (coqtop_path ()) ^ " -batch " ^ argstr in
+  let cmd = requote cmd in
   try
-    let argstr = String.concat " " (List.map Filename.quote args) in
-    let cmd = Filename.quote !Minilib.coqtop_path ^ " -batch " ^ argstr in
     let ic = Unix.open_process_in cmd in
-    let lines = read_all_lines ic in
+    lines := read_all_lines ic;
     match Unix.close_process_in ic with
-    | Unix.WEXITED 0 -> prerr_endline "coqtop seems ok"
-    | _ -> raise (Coqtop_output lines)
-  with
-    | End_of_file ->
-      Minilib.safe_prerr_endline "Cannot start connection with coqtop";
-      exit 1
-    | Coqtop_output lines ->
-      Minilib.safe_prerr_endline "Connection with coqtop failed:";
-      List.iter Minilib.safe_prerr_endline lines;
-      exit 1
+    | Unix.WEXITED 0 -> () (* coqtop seems ok *)
+    | st -> raise (WrongExitStatus (print_status st))
+  with e -> connection_error cmd !lines e
 
 (** * The structure describing a coqtop sub-process *)
 
@@ -139,7 +209,7 @@ let open_process_pid prog args =
 let spawn_coqtop sup_args =
   Mutex.lock toplvl_ctr_mtx;
   try
-    let prog = !Minilib.coqtop_path in
+    let prog = coqtop_path () in
     let args = Array.of_list (prog :: "-ideslave" :: sup_args) in
     let (pid,ic,oc) = open_process_pid prog args in
     incr toplvl_ctr;
diff --git a/ide/coq.mli b/ide/coq.mli
index 9d64da6c..7f61521e 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -13,11 +13,15 @@
 val short_version : unit -> string
 val version : unit -> string
 
-(** * Initial checks by launching test coqtop processes *)
-
-val filter_coq_opts : string list -> bool * string list
-
-(** A mock coqtop launch, checking in particular that initial.coq is found *)
+(** * Launch a test coqtop processes, ask for a correct coqtop if it fails.
+    @return the list of arguments that coqtop did not understand
+    (the files probably ..). This command may terminate coqide in
+    case of trouble.  *)
+val filter_coq_opts : string list -> string list
+
+(** Launch a coqtop with the user args in order to be sure that it works,
+    checking in particular that initial.coq is found. This command
+    may terminate coqide in case of trouble *)
 val check_connection : string list -> unit
 
 (** * The structure describing a coqtop sub-process *)
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index b9e14145..256426d2 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -127,7 +127,6 @@ let commands = [
      "Show Script";
      "Show Tree";*)
      "Structure";
-     (* "Suspend"; *)
      "Syntactic Definition";
      "Syntax";];
   [
diff --git a/ide/coq_lex.mll b/ide/coq_lex.mll
index f0f1afb7..c9a9a826 100644
--- a/ide/coq_lex.mll
+++ b/ide/coq_lex.mll
@@ -24,7 +24,7 @@
     let one_word_commands =
       [ "Add" ; "Check"; "Eval"; "Extraction" ;
 	"Load" ; "Undo"; "Goal";
-	"Proof" ; "Print";"Save" ;
+	"Proof" ; "Print";"Save" ; "Restart";
 	"End" ; "Section"; "Chapter"; "Transparent"; "Opaque"; "Comments" ]
     in
     let one_word_declarations =
@@ -37,7 +37,8 @@
         (* Inductive *)
         "Inductive" ; "CoInductive" ; "Record" ; "Structure" ;
         (* Other *)
-	"Ltac" ; "Typeclasses"; "Instance"; "Include"; "Context"; "Class" ]
+	"Ltac" ; "Instance"; "Include"; "Context"; "Class" ;
+	 "Arguments" ]
     in
     let proof_declarations =
       [ "Theorem" ; "Lemma" ; " Fact" ; "Remark" ; "Corollary" ;
@@ -85,33 +86,28 @@ let multiword_declaration =
 | "Existing" space+ "Instance" "s"?
 | "Canonical" space+ "Structure"
 
-let locality = ("Local" space+)?
+let locality = (space+ "Local")?
 
 let multiword_command =
-  "Set" (space+ ident)*
-| "Unset" (space+ ident)*
-| "Open" space+ locality "Scope"
-| "Close" space+ locality "Scope"
-| "Bind" space+ "Scope"
-| "Arguments" space+ "Scope"
-| "Reserved" space+ "Notation" space+ locality
-| "Delimit" space+ "Scope"
+  ("Uns" | "S")" et" (space+ ident)*
+| (("Open" | "Close") locality | "Bind" | " Delimit" )
+    space+ "Scope"
+| (("Reserved" space+)? "Notation" | "Infix") locality space+
 | "Next" space+ "Obligation"
 | "Solve" space+ "Obligations"
 | "Require" space+ ("Import"|"Export")?
-| "Infix" space+ locality
-| "Notation" space+ locality
-| "Hint" space+ locality ident
+| "Hint" locality space+ ident
 | "Reset" (space+ "Initial")?
 | "Tactic" space+ "Notation"
-| "Implicit" space+ "Arguments"
-| "Implicit" space+ ("Type"|"Types")
+| "Implicit" space+ "Type" "s"?
 | "Combined" space+ "Scheme"
 | "Extraction" space+ (("Language" space+ ("Ocaml"|"Haskell"|"Scheme"|"Toplevel"))|
     ("Library"|"Inline"|"NoInline"|"Blacklist"))
 | "Recursive" space+ "Extraction" (space+ "Library")?
 | ("Print"|"Reset") space+ "Extraction" space+ ("Inline"|"Blacklist")
 | "Extract" space+ (("Inlined" space+) "Constant"| "Inductive")
+| "Typeclasses" space+ ("eauto" | "Transparent" | "Opaque")
+| ("Generalizable" space+) ("All" | "No")? "Variable" "s"?
 
 (* At least still missing: "Inline" + decl, variants of "Identity
   Coercion", variants of Print, Add, ... *)
diff --git a/ide/coqide-gtk2rc b/ide/coqide-gtk2rc
index 621d4e84..9da99551 100644
--- a/ide/coqide-gtk2rc
+++ b/ide/coqide-gtk2rc
@@ -23,16 +23,6 @@ binding "text" {
 class "GtkTextView" binding "text"
 
 
-style "views" {
-base[NORMAL] = "CornSilk"
-# bg_pixmap[NORMAL] = "background.jpg"
-}
-class "GtkTextView" style "views"
-
-widget "*.*.*.*.*.ScriptWindow" style "views"
-widget "*.*.*.*.GoalWindow" style "views"
-widget "*.*.*.*.MessageWindow" style "views"
-
 gtk-font-name = "Sans 12"
 
 style "location" {
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 009a1989..61280fd9 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -27,7 +27,6 @@ let safety_tag = function
 class type analyzed_views=
 object
   val mutable act_id : GtkSignal.id option
-  val mutable deact_id : GtkSignal.id option
   val input_buffer : GText.buffer
   val input_view : Undo.undoable_view
   val last_array : string array
@@ -65,7 +64,6 @@ object
   method backtrack_to : GText.iter -> unit
   method backtrack_to_no_lock : GText.iter -> unit
   method clear_message : unit
-  method disconnected_keypress_handler : GdkEvent.Key.t -> bool
   method find_phrase_starting_at :
     GText.iter -> (GText.iter * GText.iter) option
   method get_insert : GText.iter
@@ -84,6 +82,7 @@ object
   method reset_initial : unit
   method force_reset_initial : unit
   method set_message : string -> unit
+  method raw_coq_query : string -> unit
   method show_goals : unit
   method show_goals_full : unit
   method undo_last_step : unit
@@ -889,11 +888,32 @@ object(self)
         raise RestartCoqtop
       | e -> sync display_error (None, Printexc.to_string e); None
 
+  (* This method is intended to perform stateless commands *)
+  method raw_coq_query phrase =
+    let () = prerr_endline "raw_coq_query starting now" in
+    let display_error s =
+      if not (Glib.Utf8.validate s) then
+        flash_info "This error is so nasty that I can't even display it."
+      else begin
+        self#insert_message s;
+        message_view#misc#draw None
+      end
+    in
+    try
+      match Coq.interp !mycoqtop ~raw:true ~verbose:false phrase with
+      | Interface.Fail (_, err) -> sync display_error err
+      | Interface.Good msg -> sync self#insert_message msg
+    with
+    | End_of_file -> raise RestartCoqtop
+    | e -> sync display_error (Printexc.to_string e)
+
   method find_phrase_starting_at (start:GText.iter) =
     try
       let start = grab_sentence_start start self#get_start_of_input in
       let stop = grab_sentence_stop start in
-      if is_sentence_end stop#backward_char then Some (start,stop)
+      (* Is this phrase non-empty and complete ? *)
+      if stop#compare start > 0 && is_sentence_end stop#backward_char
+      then Some (start,stop)
       else None
     with Not_found -> None
 
@@ -1217,22 +1237,6 @@ object(self)
     let state = GdkEvent.Key.state k in
     begin
       match  state with
-        | l when List.mem `MOD1 l ->
-          let k = GdkEvent.Key.keyval k in
-          if GdkKeysyms._Return=k
-          then ignore(
-            if (input_buffer#insert_interactive "\n") then
-              begin
-                let i= self#get_insert#backward_word_start in
-                prerr_endline "active_kp_hf: Placing cursor";
-                self#process_until_iter_or_error i
-              end);
-          true
-        | l when List.mem `CONTROL l ->
-          let k = GdkEvent.Key.keyval k in
-          if GdkKeysyms._Break=k
-          then break ();
-          false
         | l ->
           if GdkEvent.Key.keyval k = GdkKeysyms._Tab then begin
             prerr_endline "active_kp_handler for Tab";
@@ -1241,18 +1245,6 @@ object(self)
           end else false
     end
 
-
-  method disconnected_keypress_handler k =
-    match GdkEvent.Key.state k with
-      | l when List.mem `CONTROL l ->
-        let k = GdkEvent.Key.keyval k in
-        if GdkKeysyms._c=k
-        then break ();
-        false
-      | l -> false
-
-
-  val mutable deact_id = None
   val mutable act_id = None
 
   method activate () = if not is_active then begin
@@ -1523,9 +1515,15 @@ let create_session file =
   script#buffer#place_cursor ~where:(script#buffer#start_iter);
   proof#misc#set_can_focus true;
   message#misc#set_can_focus true;
+  (* setting fonts *)
   script#misc#modify_font !current.text_font;
   proof#misc#modify_font !current.text_font;
   message#misc#modify_font !current.text_font;
+  (* setting colors *)
+  script#misc#modify_base [`NORMAL, `NAME !current.background_color];
+  proof#misc#modify_base [`NORMAL, `NAME !current.background_color];
+  message#misc#modify_base [`NORMAL, `NAME !current.background_color];
+
   { tab_label=basename;
     filename=begin match file with None -> "" |Some f -> f end;
     script=script;
@@ -1798,12 +1796,6 @@ let forbid_quit_to_save () =
 	else false)
 
 let main files =
-  (* Statup preferences *)
-  begin
-    try load_pref ()
-    with e ->
-      flash_info ("Could not load preferences ("^Printexc.to_string e^").");
-  end;
 
   (* Main window *)
   let w = GWindow.window
@@ -1823,9 +1815,9 @@ let main files =
   let vbox = GPack.vbox ~homogeneous:false ~packing:w#add () in
 
   let new_f _ =
-    match select_file_for_save ~title:"Create file" () with
-      | None -> ()
-      | Some f -> do_load f
+    let session = create_session None in
+    let index = session_notebook#append_term session in
+    session_notebook#goto_page index
   in
   let load_f _ =
     match select_file_for_open ~title:"Load file" () with
@@ -2181,6 +2173,7 @@ let main files =
 	     true))
   in reset_auto_save_timer (); (* to enable statup preferences timer *)
 (* end Preferences *)
+
   let do_or_activate f () =
     do_if_not_computing "do_or_activate"
       (fun current ->
@@ -2327,13 +2320,13 @@ let main files =
   in
 
   let file_actions = GAction.action_group ~name:"File" () in
-  let export_actions = GAction.action_group ~name:"Export" () in
   let edit_actions = GAction.action_group ~name:"Edit" () in
+  let view_actions = GAction.action_group ~name:"View" () in
+  let export_actions = GAction.action_group ~name:"Export" () in
   let navigation_actions = GAction.action_group ~name:"Navigation" () in
   let tactics_actions = GAction.action_group ~name:"Tactics" () in
   let templates_actions = GAction.action_group ~name:"Templates" () in
   let queries_actions = GAction.action_group ~name:"Queries" () in
-  let display_actions = GAction.action_group ~name:"Display" () in
   let compile_actions = GAction.action_group ~name:"Compile" () in
   let windows_actions = GAction.action_group ~name:"Windows" () in
   let help_actions = GAction.action_group ~name:"Help" () in
@@ -2362,10 +2355,18 @@ let main files =
     ~accel:(!current.modifier_for_tactics^sc)
     ~callback:(do_if_active (fun a -> a#insert_command
 			       ("progress "^s^".\n") (s^".\n"))) in
-  let query_shortcut s accel = GAction.add_action s ~label:("_"^s) ?accel
-    ~callback:(fun _ -> let term = get_current_word () in
-		 session_notebook#current_term.command#new_command ~command:s ~term ())
-  in let add_complex_template (name, label, text, offset, len, key) =
+  let query_callback command _ =
+    let word = get_current_word () in
+    if not (word = "") then
+      let term = session_notebook#current_term in
+      let query = command ^ " " ^ word ^ "." in
+      term.message_view#buffer#set_text "";
+      term.analyzed_view#raw_coq_query query
+  in
+  let query_shortcut s accel =
+    GAction.add_action s ~label:("_"^s) ?accel ~callback:(query_callback s)
+  in
+  let add_complex_template (name, label, text, offset, len, key) =
     (* Templates/Lemma *)
     let callback _ =
       let {script = view } = session_notebook#current_term in
@@ -2450,6 +2451,31 @@ let main files =
 	end;
 	reset_revert_timer ()) ~stock:`PREFERENCES;
       (* GAction.add_action "Save preferences" ~label:"_Save preferences" ~callback:(fun _ -> save_pref ()); *) ];
+    GAction.add_actions view_actions [
+      GAction.add_action "View" ~label:"_View";
+      GAction.add_action "Previous tab" ~label:"_Previous tab" ~accel:("<SHIFT>Left") ~stock:`GO_BACK
+        ~callback:(fun _ -> session_notebook#previous_page ());
+      GAction.add_action "Next tab" ~label:"_Next tab" ~accel:("<SHIFT>Right") ~stock:`GO_FORWARD
+        ~callback:(fun _ -> session_notebook#next_page ());
+      GAction.add_toggle_action "Show Toolbar" ~label:"Show _Toolbar"
+        ~active:(!current.show_toolbar) ~callback:
+        (fun _ -> !current.show_toolbar <- not !current.show_toolbar;
+           !refresh_toolbar_hook ());
+      GAction.add_toggle_action "Show Query Pane" ~label:"Show _Query Pane"
+        ~callback:(fun _ -> let ccw = session_notebook#current_term.command in
+                     if ccw#frame#misc#visible
+                     then ccw#frame#misc#hide ()
+                     else ccw#frame#misc#show ())
+        ~accel:"Escape";
+    ];
+    List.iter
+      (fun (opts,name,label,key,dflt) ->
+         GAction.add_toggle_action name ~active:dflt ~label
+           ~accel:(!current.modifier_for_display^key)
+          ~callback:(fun v -> do_or_activate (fun a ->
+            let () = setopts !(session_notebook#current_term.toplvl) opts v#get_active in
+            a#show_goals) ()) view_actions)
+      print_items;
     GAction.add_actions navigation_actions [
       GAction.add_action "Navigation" ~label:"_Navigation";
       GAction.add_action "Forward" ~label:"_Forward" ~stock:`GO_DOWN
@@ -2532,15 +2558,6 @@ let main files =
       query_shortcut "Locate" None;
       query_shortcut "Whelp Locate" None;
     ];
-    GAction.add_action "Display" ~label:"_Display" display_actions;
-    List.iter
-      (fun (opts,name,label,key,dflt) ->
-         GAction.add_toggle_action name ~active:dflt ~label
-	   ~accel:(!current.modifier_for_display^key)
-          ~callback:(fun v -> do_or_activate (fun a ->
-            let () = setopts !(session_notebook#current_term.toplvl) opts v#get_active in
-            a#show_goals) ()) display_actions)
-      print_items;
     GAction.add_actions compile_actions [
       GAction.add_action "Compile" ~label:"_Compile";
       GAction.add_action "Compile buffer" ~label:"_Compile buffer" ~callback:compile_f;
@@ -2551,16 +2568,6 @@ let main files =
     ];
     GAction.add_actions windows_actions [
       GAction.add_action "Windows" ~label:"_Windows";
-      GAction.add_toggle_action "Show/Hide Query Pane" ~label:"Show/Hide _Query Pane"
-	~callback:(fun _ -> let ccw = session_notebook#current_term.command in
-		     if ccw#frame#misc#visible
-		     then ccw#frame#misc#hide ()
-		     else ccw#frame#misc#show ())
-	~accel:"Escape";
-      GAction.add_toggle_action "Show/Hide Toolbar" ~label:"Show/Hide _Toolbar"
-	~active:(!current.show_toolbar) ~callback:
-	(fun _ -> !current.show_toolbar <- not !current.show_toolbar;
-	   !show_toolbar !current.show_toolbar);
       GAction.add_action "Detach View" ~label:"Detach _View"
 	~callback:(fun _ -> do_if_not_computing "detach view"
 		     (function {script=v;analyzed_view=av} ->
@@ -2608,11 +2615,11 @@ let main files =
     Coqide_ui.ui_m#insert_action_group file_actions 0;
     Coqide_ui.ui_m#insert_action_group export_actions 0;
     Coqide_ui.ui_m#insert_action_group edit_actions 0;
+    Coqide_ui.ui_m#insert_action_group view_actions 0;
     Coqide_ui.ui_m#insert_action_group navigation_actions 0;
     Coqide_ui.ui_m#insert_action_group tactics_actions 0;
     Coqide_ui.ui_m#insert_action_group templates_actions 0;
     Coqide_ui.ui_m#insert_action_group queries_actions 0;
-    Coqide_ui.ui_m#insert_action_group display_actions 0;
     Coqide_ui.ui_m#insert_action_group compile_actions 0;
     Coqide_ui.ui_m#insert_action_group windows_actions 0;
     Coqide_ui.ui_m#insert_action_group help_actions 0;
@@ -2625,9 +2632,6 @@ let main files =
     let toolbar = new GObj.widget tbar in
     vbox#pack toolbar;
 
-    show_toolbar :=
-      (fun b -> if b then toolbar#misc#show () else toolbar#misc#hide ());
-
     ignore (w#event#connect#delete ~callback:(fun _ -> quit_f (); true));
 
   (* The vertical Separator between Scripts and Goals *)
@@ -2790,17 +2794,39 @@ let main files =
   (* Progress Bar *)
   lower_hbox#pack pbar#coerce;
   pbar#set_text "CoqIde started";
-  (* XXX *)
-  change_font :=
-    (fun fd ->
-      List.iter
-	(fun {script=view; proof_view=prf_v; message_view=msg_v} ->
-          view#misc#modify_font fd;
-          prf_v#misc#modify_font fd;
-          msg_v#misc#modify_font fd
-        )
-	session_notebook#pages;
+
+  (* Initializing hooks *)
+
+  refresh_toolbar_hook :=
+    (fun () -> if !current.show_toolbar then toolbar#misc#show () else toolbar#misc#hide ());
+  refresh_font_hook :=
+    (fun () ->
+      let fd = !current.text_font in
+      let iter_page p =
+        p.script#misc#modify_font fd;
+        p.proof_view#misc#modify_font fd;
+        p.message_view#misc#modify_font fd;
+        p.command#refresh_font ()
+      in
+      List.iter iter_page session_notebook#pages;
     );
+  refresh_background_color_hook :=
+    (fun () ->
+      let clr = Tags.color_of_string !current.background_color in
+      let iter_page p =
+        p.script#misc#modify_base [`NORMAL, `COLOR clr];
+        p.proof_view#misc#modify_base [`NORMAL, `COLOR clr];
+        p.message_view#misc#modify_base [`NORMAL, `COLOR clr];
+        p.command#refresh_color ()
+      in
+      List.iter iter_page session_notebook#pages;
+    );
+  resize_window_hook := (fun () ->
+    w#resize
+      ~width:!current.window_width
+      ~height:!current.window_height);
+  refresh_tabs_hook := update_notebook_pos;
+
   let about_full_string =
     "\nCoq is developed by the Coq Development Team\
      \n(INRIA - CNRS - LIX - LRI - PPS)\
@@ -2865,10 +2891,12 @@ let main files =
   (*
 
   *)
-  resize_window := (fun () ->
-    w#resize
-      ~width:!current.window_width
-      ~height:!current.window_height);
+(* Begin Color configuration *)
+
+  Tags.set_processing_color (Tags.color_of_string !current.processing_color);
+  Tags.set_processed_color (Tags.color_of_string !current.processed_color);
+
+(* End of color configuration *)
   ignore(nb#connect#switch_page
 	   ~callback:
 	   (fun i ->
@@ -2892,7 +2920,7 @@ let main files =
       session_notebook#goto_page index;
     end;
   initial_about session_notebook#current_term.proof_view#buffer;
-  !show_toolbar !current.show_toolbar;
+  !refresh_toolbar_hook ();
   session_notebook#current_term.script#misc#grab_focus ();;
 
 (* This function check every half of second if GeoProof has send
@@ -2921,43 +2949,24 @@ let rec check_for_geoproof_input () =
     in the path. Note that the -coqtop option to coqide allows to override
     this default coqtop path *)
 
-let default_coqtop_path () =
-  let prog = Sys.executable_name in
-  try
-    let pos = String.length prog - 6 in
-    let i = Str.search_backward (Str.regexp_string "coqide") prog pos in
-    String.blit "coqtop" 0 prog i 6;
-    prog
-  with _ -> "coqtop"
-
 let read_coqide_args argv =
   let rec filter_coqtop coqtop project_files out = function
     | "-coqtop" :: prog :: args ->
-      if coqtop = "" then filter_coqtop prog project_files out args
+      if coqtop = None then filter_coqtop (Some prog) project_files out args
       else
-	(output_string stderr "Error: multiple -coqtop options"; exit 1)
+       (output_string stderr "Error: multiple -coqtop options"; exit 1)
     | "-f" :: file :: args ->
 	filter_coqtop coqtop
 	  ((Minilib.canonical_path_name (Filename.dirname file),
 	    Project_file.read_project_file file) :: project_files) out args
     | "-f" :: [] -> output_string stderr "Error: missing project file name"; exit 1
+    | "-coqtop" :: [] -> output_string stderr "Error: missing argument after -coqtop"; exit 1
+    | "-debug"::args -> Ideutils.debug := true;
+      filter_coqtop coqtop project_files ("-debug"::out) args
     | arg::args -> filter_coqtop coqtop project_files (arg::out) args
-    | [] -> ((if coqtop = "" then default_coqtop_path () else coqtop),
-	     List.rev project_files,List.rev out)
+    | [] -> (coqtop,List.rev project_files,List.rev out)
   in
-  let coqtop,project_files,argv = filter_coqtop "" [] [] argv in
-    Minilib.coqtop_path := coqtop;
+  let coqtop,project_files,argv = filter_coqtop None [] [] argv in
+    Ideutils.custom_coqtop := coqtop;
     custom_project_files := project_files;
   argv
-
-let process_argv argv =
-  try
-    let continue,filtered = Coq.filter_coq_opts (List.tl argv) in
-    if not continue then
-      (List.iter Minilib.safe_prerr_endline filtered; exit 0);
-    let opts = List.filter (fun arg -> String.get arg 0 == '-') filtered in
-    if opts <> [] then
-      (Minilib.safe_prerr_endline ("Illegal option: "^List.hd opts); exit 1);
-    filtered
-  with _ ->
-    (Minilib.safe_prerr_endline "coqtop choked on one of your option"; exit 1)
diff --git a/ide/coqide.mli b/ide/coqide.mli
index 38b0fab0..57158a6a 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.mli
@@ -16,9 +16,6 @@ val sup_args : string list ref
     Minilib.coqtop_path accordingly *)
 val read_coqide_args : string list -> string list
 
-(** Ask coqtop the remaining options it doesn't recognize *)
-val process_argv : string list -> string list
-
 (** Prepare the widgets, load the given files in tabs *)
 val main : string list -> unit
 
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
index 3fec0631..6f4b8b13 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml4
@@ -65,21 +65,21 @@ let () =
 END
 
 let () =
-  let argl = Array.to_list Sys.argv in
-  let argl = Coqide.read_coqide_args argl in
-  let files = Coqide.process_argv argl in
-  let args = List.filter (fun x -> not (List.mem x files)) (List.tl argl) in
-  Coq.check_connection args;
-  Coqide.sup_args := args;
   Coqide.ignore_break ();
+  ignore (GtkMain.Main.init ());
+  initmac () ;
   (try
      let gtkrcdir = List.find
        (fun x -> Sys.file_exists (Filename.concat x "coqide-gtk2rc"))
        Minilib.xdg_config_dirs in
      GtkMain.Rc.add_default_file (Filename.concat gtkrcdir "coqide-gtk2rc");
    with Not_found -> ());
-  ignore (GtkMain.Main.init ());
-  initmac () ;
+  (* Statup preferences *)
+  begin
+    try Preferences.load_pref ()
+    with e ->
+      Ideutils.flash_info ("Could not load preferences ("^Printexc.to_string e^").");
+  end;
 (*    GtkData.AccelGroup.set_default_mod_mask
       (Some [`CONTROL;`SHIFT;`MOD1;`MOD3;`MOD4]);*)
     ignore (
@@ -89,7 +89,13 @@ let () =
 		  if level land Glib.Message.log_level `WARNING <> 0
 		  then Printf.eprintf "Warning: %s\n" msg
 		  else failwith ("Coqide internal error: " ^ msg)));
-    Coqide.main files;
+  let argl = Array.to_list Sys.argv in
+  let argl = Coqide.read_coqide_args argl in
+  let files = Coq.filter_coq_opts (List.tl argl) in
+  let args = List.filter (fun x -> not (List.mem x files)) (List.tl argl) in
+  Coq.check_connection args;
+  Coqide.sup_args := args;
+  Coqide.main files;
     if !Coq_config.with_geoproof then ignore (Thread.create Coqide.check_for_geoproof_input ());
     macready (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar") (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Edit/Prefs")
              (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Help/Abt");
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index 0d7c67ac..eaf1e934 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -56,6 +56,22 @@ let init () =
     <separator />
     <menuitem name='Prefs' action='Preferences' />
   </menu>
+  <menu name='View' action='View'>
+    <menuitem action='Previous tab' />
+    <menuitem action='Next tab' />
+    <separator/>
+    <menuitem action='Show Toolbar' />
+    <menuitem action='Show Query Pane' />
+    <separator/>
+    <menuitem action='Display implicit arguments' />
+    <menuitem action='Display coercions' />
+    <menuitem action='Display raw matching expressions' />
+    <menuitem action='Display notations' />
+    <menuitem action='Display all basic low-level contents' />
+    <menuitem action='Display existential variable instances' />
+    <menuitem action='Display universe levels' />
+    <menuitem action='Display all low-level contents' />
+  </menu>
   <menu action='Navigation'>
     <menuitem action='Forward' />
     <menuitem action='Backward' />
@@ -100,16 +116,6 @@ let init () =
     <menuitem action='Locate' />
     <menuitem action='Whelp Locate' />
   </menu>
-  <menu action='Display'>
-    <menuitem action='Display implicit arguments' />
-    <menuitem action='Display coercions' />
-    <menuitem action='Display raw matching expressions' />
-    <menuitem action='Display notations' />
-    <menuitem action='Display all basic low-level contents' />
-    <menuitem action='Display existential variable instances' />
-    <menuitem action='Display universe levels' />
-    <menuitem action='Display all low-level contents' />
-  </menu>
   <menu action='Compile'>
     <menuitem action='Compile buffer' />
     <menuitem action='Make' />
@@ -117,8 +123,6 @@ let init () =
     <menuitem action='Make makefile' />
   </menu>
   <menu action='Windows'>
-    <menuitem action='Show/Hide Query Pane' />
-    <menuitem action='Show/Hide Toolbar' />
     <menuitem action='Detach View' />
   </menu>
   <menu name='Help' action='Help'>
diff --git a/ide/ideproof.ml b/ide/ideproof.ml
index 3c3324cb..b79d6469 100644
--- a/ide/ideproof.ml
+++ b/ide/ideproof.ml
@@ -53,7 +53,7 @@ let mode_tactic sel_cb (proof:GText.view) goals hints = match goals with
         "%d subgoal%s\n" goals_cnt (if 1 < goals_cnt then "" else "s")
       in
       let goal_str index total = Printf.sprintf
-        "\n______________________________________(%d/%d)\n" index total
+        "______________________________________(%d/%d)\n" index total
       in
       (* Insert current goal and its hypotheses *)
       let hyps_hints, goal_hints = match hints with
@@ -76,14 +76,15 @@ let mode_tactic sel_cb (proof:GText.view) goals hints = match goals with
       let () = proof#buffer#insert head_str in
       let () = insert_hyp hyps_hints hyps in
       let () =
-        let tags = if goal_hints <> [] then
+        let tags = Tags.Proof.goal :: if goal_hints <> [] then
           let tag = proof#buffer#create_tag [] in
           let () = hook_tag_cb tag goal_hints sel_cb on_hover in
           [tag]
           else []
         in
         proof#buffer#insert (goal_str 1 goals_cnt);
-        proof#buffer#insert ~tags (cur_goal ^ "\n")
+        proof#buffer#insert ~tags cur_goal;
+	proof#buffer#insert "\n"
       in
       (* Insert remaining goals (no hypotheses) *)
       let fold_goal i _ { Interface.goal_ccl = g } =
@@ -91,10 +92,11 @@ let mode_tactic sel_cb (proof:GText.view) goals hints = match goals with
         proof#buffer#insert (g ^ "\n")
       in
       let () = Minilib.list_fold_left_i fold_goal 2 () rem_goals in
-      ignore(proof#buffer#place_cursor  
-        ~where:((proof#buffer#get_iter_at_mark `INSERT)#backward_lines (3*goals_cnt - 2)));
-      ignore(proof#scroll_to_mark `INSERT)
 
+      ignore(proof#buffer#place_cursor
+               ~where:(proof#buffer#end_iter#backward_to_tag_toggle
+			 (Some Tags.Proof.goal)));
+      ignore(proof#scroll_to_mark ~use_align:true ~yalign:0.95 `INSERT)
 
 let mode_cesar (proof:GText.view) = function
   | [] -> assert false
@@ -123,7 +125,7 @@ let display mode (view:GText.view) goals hints evars =
       in
       List.iter iter evs
     | _ ->
-      view#buffer#insert "Proof Completed."
+      view#buffer#insert "No more subgoals."
     end
   | Some { Interface.fg_goals = []; Interface.bg_goals = bg } ->
     (* No foreground proofs, but still unfocused ones *)
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index fd460c4e..a208ad0e 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -63,28 +63,25 @@ let print_id id =
 let do_convert s =
   Utf8_convert.f
     (if Glib.Utf8.validate s then begin
-       prerr_endline "Input is UTF-8";s
-     end else
-       let from_loc () =
-	 let _,char_set = Glib.Convert.get_charset () in
-	 flash_info
-	   ("Converting from locale ("^char_set^")");
-	 Glib.Convert.convert_with_fallback ~to_codeset:"UTF-8" ~from_codeset:char_set s
-       in
-       let from_manual () =
-	 flash_info
-	   ("Converting from "^ !current.encoding_manual);
-	 Glib.Convert.convert s ~to_codeset:"UTF-8" ~from_codeset:!current.encoding_manual
-       in
-       if !current.encoding_use_utf8 || !current.encoding_use_locale then begin
-	 try
-	   from_loc ()
-	 with _ -> from_manual ()
-       end else begin
-	 try
-	   from_manual ()
-	 with _ -> from_loc ()
-       end)
+      prerr_endline "Input is UTF-8";s
+    end else
+	let from_loc () =
+	  let _,char_set = Glib.Convert.get_charset () in
+	  flash_info
+	    ("Converting from locale ("^char_set^")");
+	  Glib.Convert.convert_with_fallback ~to_codeset:"UTF-8" ~from_codeset:char_set s
+	in
+	let from_manual enc =
+	  flash_info
+	    ("Converting from "^ enc);
+	  Glib.Convert.convert s ~to_codeset:"UTF-8" ~from_codeset:enc
+	in
+	match !current.encoding with
+	  |Preferences.Eutf8 | Preferences.Elocale -> from_loc ()
+	  |Emanual enc ->
+	    try
+	      from_manual enc
+	    with _ -> from_loc ())
 
 let try_convert s =
   try
@@ -96,18 +93,21 @@ Please choose a correct encoding in the preference panel.*)";;
 
 let try_export file_name s =
   try let s =
-    try if !current.encoding_use_utf8 then begin
-      (prerr_endline "UTF-8 is enforced" ;s)
-    end else if !current.encoding_use_locale then begin
-      let is_unicode,char_set = Glib.Convert.get_charset () in
-      if is_unicode then
-	(prerr_endline "Locale is UTF-8" ;s)
-      else
-	(prerr_endline ("Locale is "^char_set);
-	 Glib.Convert.convert_with_fallback ~from_codeset:"UTF-8" ~to_codeset:char_set s)
-    end else
-      (prerr_endline ("Manual charset is "^ !current.encoding_manual);
-       Glib.Convert.convert_with_fallback ~from_codeset:"UTF-8" ~to_codeset:!current.encoding_manual s)
+    try match !current.encoding with
+      |Eutf8 -> begin
+	(prerr_endline "UTF-8 is enforced" ;s)
+      end
+      |Elocale -> begin
+	let is_unicode,char_set = Glib.Convert.get_charset () in
+	if is_unicode then
+	  (prerr_endline "Locale is UTF-8" ;s)
+	else
+	  (prerr_endline ("Locale is "^char_set);
+	   Glib.Convert.convert_with_fallback ~from_codeset:"UTF-8" ~to_codeset:char_set s)
+      end
+      |Emanual enc ->
+	(prerr_endline ("Manual charset is "^ enc);
+       Glib.Convert.convert_with_fallback ~from_codeset:"UTF-8" ~to_codeset:enc s)
     with e -> (prerr_endline ("Error ("^(Printexc.to_string e)^") in transcoding: falling back to UTF-8") ;s)
   in
   let oc = open_out file_name in
@@ -252,14 +252,40 @@ let stock_to_widget ?(size=`DIALOG) s =
   in img#set_stock s;
   img#coerce
 
+let custom_coqtop = ref None
+
+let coqtop_path () =
+  let file = match !custom_coqtop with
+    | Some s -> s
+    | None ->
+      match !current.cmd_coqtop with
+	| Some s -> s
+	| None ->
+	  let prog = String.copy Sys.executable_name in
+	  try
+	    let pos = String.length prog - 6 in
+	    let i = Str.search_backward (Str.regexp_string "coqide") prog pos in
+	    String.blit "coqtop" 0 prog i 6;
+	    prog
+	  with Not_found -> "coqtop"
+  in file
+
 let rec print_list print fmt = function
   | [] -> ()
   | [x] -> print fmt x
   | x :: r -> print fmt x; print_list print fmt r
 
+(* In win32, when a command-line is to be executed via cmd.exe
+   (i.e. Sys.command, Unix.open_process, ...), it cannot contain several
+   quoted "..." zones otherwise some quotes are lost. Solution: we re-quote
+   everything. Reference: http://ss64.com/nt/cmd.html *)
+
+let requote cmd = if Sys.os_type = "Win32" then "\""^cmd^"\"" else cmd
+
 (* TODO: allow to report output as soon as it comes (user-fiendlier
    for long commands like make...) *)
 let run_command f c =
+  let c = requote c in
   let result = Buffer.create 127 in
   let cin,cout,cerr = Unix.open_process_full c (Unix.environment ()) in
   let buff = String.make 127 ' ' in
@@ -279,11 +305,12 @@ let run_command f c =
 
 let browse f url =
   let com = Minilib.subst_command_placeholder !current.cmd_browse url in
-  let s = Sys.command com in
+  let _ = Unix.open_process_out com in ()
+(* This beautiful message will wait for twt ...
   if s = 127 then
     f ("Could not execute\n\""^com^
        "\"\ncheck your preferences for setting a valid browser command\n")
-
+*)
 let doc_url () =
   if !current.doc_url = use_default_doc_url || !current.doc_url = "" then
     let addr = List.fold_left Filename.concat (Coq_config.docdir) ["html";"refman";"index.html"] in
diff --git a/ide/ideutils.mli b/ide/ideutils.mli
index 1e29d323..c433d92a 100644
--- a/ide/ideutils.mli
+++ b/ide/ideutils.mli
@@ -52,6 +52,12 @@ val print_list : (formatter -> 'a -> unit) -> formatter -> 'a list -> unit
 
 val run_command : (string -> unit) -> string -> Unix.process_status*string
 
+val custom_coqtop : string option ref
+(* @return command to call coqtop
+   - custom_coqtop if set
+   - from the prefs is set
+   - try to infer it else *)
+val coqtop_path : unit -> string
 
 
 val status : GMisc.statusbar
@@ -67,3 +73,10 @@ val pbar : GRange.progress_bar
   returns an absolute filename equivalent to given filename
 *)
 val absolute_filename : string -> string
+
+(* In win32, when a command-line is to be executed via cmd.exe
+   (i.e. Sys.command, Unix.open_process, ...), it cannot contain several
+   quoted "..." zones otherwise some quotes are lost. Solution: we re-quote
+   everything. Reference: http://ss64.com/nt/cmd.html *)
+
+val requote : string -> string
diff --git a/ide/minilib.ml b/ide/minilib.ml
index cec77f3b..4ccb1ccb 100644
--- a/ide/minilib.ml
+++ b/ide/minilib.ml
@@ -64,9 +64,10 @@ let string_map f s =
 let subst_command_placeholder s t =
   Str.global_replace (Str.regexp_string "%s") t s
 
-let path_to_list p =
-  let sep = Str.regexp (if Sys.os_type = "Win32" then ";" else ":") in
-    Str.split sep p
+(* Split the content of a variable such as $PATH in a list of directories.
+   The separators are either ":" in unix or ";" in win32 *)
+
+let path_to_list = Str.split (Str.regexp "[:;]")
 
 (* On win32, the home directory is probably not in $HOME, but in
    some other environment variable *)
@@ -76,28 +77,50 @@ let home =
     try (Sys.getenv "HOMEDRIVE")^(Sys.getenv "HOMEPATH") with Not_found ->
       try Sys.getenv "USERPROFILE" with Not_found -> Filename.current_dir_name
 
+let opt2list = function None -> [] | Some x -> [x]
+
+let rec lconcat = function
+  | [] -> assert false
+  | [x] -> x
+  | x::l -> Filename.concat x (lconcat l)
+
 let xdg_config_home =
   try
     Filename.concat (Sys.getenv "XDG_CONFIG_HOME") "coq"
   with Not_found ->
-    Filename.concat home "/.config/coq"
+    lconcat [home;".config";"coq"]
+
+let static_xdg_config_dirs =
+  if Sys.os_type = "Win32" then
+    let base = Filename.dirname (Filename.dirname Sys.executable_name) in
+    [Filename.concat base "config"]
+  else ["/etc/xdg/coq"]
 
 let xdg_config_dirs =
-  xdg_config_home :: (try
-    List.map (fun dir -> Filename.concat dir "coq") (path_to_list (Sys.getenv "XDG_CONFIG_DIRS"))
-  with Not_found -> "/etc/xdg/coq"::(match Coq_config.configdir with |None -> [] |Some d -> [d]))
+  xdg_config_home ::
+    try
+      List.map (fun dir -> Filename.concat dir "coq")
+	(path_to_list (Sys.getenv "XDG_CONFIG_DIRS"))
+    with Not_found -> static_xdg_config_dirs @ opt2list Coq_config.configdir
 
 let xdg_data_home =
   try
     Filename.concat (Sys.getenv "XDG_DATA_HOME") "coq"
   with Not_found ->
-    Filename.concat home "/.local/share/coq"
+    lconcat [home;".local";"share";"coq"]
+
+let static_xdg_data_dirs =
+  if Sys.os_type = "Win32" then
+    let base = Filename.dirname (Filename.dirname Sys.executable_name) in
+    [Filename.concat base "share"]
+  else ["/usr/local/share/coq";"/usr/share/coq"]
 
 let xdg_data_dirs =
-  xdg_data_home :: (try
-    List.map (fun dir -> Filename.concat dir "coq") (path_to_list (Sys.getenv "XDG_DATA_DIRS"))
-  with Not_found ->
-    "/usr/local/share/coq"::"/usr/share/coq"::(match Coq_config.datadir with |None -> [] |Some d -> [d]))
+  xdg_data_home ::
+    try
+      List.map (fun dir -> Filename.concat dir "coq")
+	(path_to_list (Sys.getenv "XDG_DATA_DIRS"))
+    with Not_found -> static_xdg_data_dirs @ opt2list Coq_config.datadir
 
 let coqtop_path = ref ""
 
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 02673098..d320ddda 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -10,9 +10,22 @@ open Configwin
 open Printf
 
 let pref_file = Filename.concat Minilib.xdg_config_home "coqiderc"
-
 let accel_file = Filename.concat Minilib.xdg_config_home "coqide.keys"
 
+let get_config_file name =
+  let find_config dir = Sys.file_exists (Filename.concat dir name) in
+  let config_dir = List.find find_config Minilib.xdg_config_dirs in
+  Filename.concat config_dir name
+
+(* Small hack to handle v8.3 to v8.4 change in configuration file *)
+let loaded_pref_file =
+  try get_config_file "coqiderc"
+  with Not_found -> Filename.concat Minilib.home ".coqiderc"
+
+let loaded_accel_file =
+  try get_config_file "coqide.keys"
+  with Not_found -> Filename.concat Minilib.home ".coqide.keys"
+
 let mod_to_str (m:Gdk.Tags.modifier) =
   match m with
     | `MOD1 -> "<Alt>"
@@ -40,8 +53,32 @@ let project_behavior_of_string s =
   else if s = "appended to arguments" then Append_args
   else Ignore_args
 
+type inputenc = Elocale | Eutf8 | Emanual of string
+
+let string_of_inputenc = function
+  |Elocale -> "LOCALE"
+  |Eutf8 -> "UTF-8"
+  |Emanual s -> s
+
+let inputenc_of_string s =
+      (if s = "UTF-8" then Eutf8
+       else if s = "LOCALE" then Elocale
+       else Emanual s)
+
+
+(** Hooks *)
+
+let refresh_font_hook = ref (fun () -> ())
+let refresh_background_color_hook = ref (fun () -> ())
+let refresh_toolbar_hook = ref (fun () -> ())
+let auto_complete_hook = ref (fun x -> ())
+let contextual_menus_on_goal_hook = ref (fun x -> ())
+let resize_window_hook = ref (fun () -> ())
+let refresh_tabs_hook = ref (fun () -> ())
+
 type pref =
     {
+      mutable cmd_coqtop : string option;
       mutable cmd_coqc : string;
       mutable cmd_make : string;
       mutable cmd_coqmakefile : string;
@@ -57,9 +94,7 @@ type pref =
       mutable read_project : project_behavior;
       mutable project_file_name : string;
 
-      mutable encoding_use_locale : bool;
-      mutable encoding_use_utf8 : bool;
-      mutable encoding_manual : string;
+      mutable encoding : inputenc;
 
       mutable automatic_tactics : string list;
       mutable cmd_print : string;
@@ -89,15 +124,20 @@ type pref =
 *)
       mutable auto_complete : bool;
       mutable stop_before : bool;
-      mutable lax_syntax : bool;
       mutable vertical_tabs : bool;
       mutable opposite_tabs : bool;
+
+      mutable background_color : string;
+      mutable processing_color : string;
+      mutable processed_color : string;
+
 }
 
 let use_default_doc_url = "(automatic)"
 
 let (current:pref ref) =
   ref {
+    cmd_coqtop = None;
     cmd_coqc = "coqc";
     cmd_make = "make";
     cmd_coqmakefile = "coq_makefile -o makefile *.v";
@@ -114,9 +154,7 @@ let (current:pref ref) =
     read_project = Ignore_args;
     project_file_name = "_CoqProject";
 
-    encoding_use_locale = true;
-    encoding_use_utf8 = false;
-    encoding_manual = "ISO_8859-1";
+    encoding = if Sys.os_type = "Win32" then Eutf8 else Elocale;
 
     automatic_tactics = ["trivial"; "tauto"; "auto"; "omega";
 			 "auto with *"; "intuition" ];
@@ -150,32 +188,25 @@ let (current:pref ref) =
 *)
     auto_complete = false;
     stop_before = true;
-    lax_syntax = true;
     vertical_tabs = false;
     opposite_tabs = false;
-  }
-
-
-let change_font = ref (fun f -> ())
 
-let show_toolbar = ref (fun x -> ())
+    background_color = "cornsilk";
+    processed_color = "light green";
+    processing_color = "light blue";
 
-let auto_complete = ref (fun x -> ())
-
-let contextual_menus_on_goal = ref (fun x -> ())
-
-let resize_window = ref (fun () -> ())
+  }
 
 let save_pref () =
   if not (Sys.file_exists Minilib.xdg_config_home)
   then Unix.mkdir Minilib.xdg_config_home 0o700;
-  (try GtkData.AccelMap.save accel_file
-  with _ -> ());
+  let () = try GtkData.AccelMap.save accel_file with _ -> () in
   let p = !current in
 
     let add = Minilib.Stringmap.add in
     let (++) x f = f x in
     Minilib.Stringmap.empty ++
+    add "cmd_coqtop" (match p.cmd_coqtop with | None -> [] | Some v-> [v]) ++
     add "cmd_coqc" [p.cmd_coqc] ++
     add "cmd_make" [p.cmd_make] ++
     add "cmd_coqmakefile" [p.cmd_coqmakefile] ++
@@ -190,9 +221,7 @@ let save_pref () =
     add "project_options" [string_of_project_behavior p.read_project] ++
     add "project_file_name" [p.project_file_name] ++
 
-    add "encoding_use_locale" [string_of_bool p.encoding_use_locale] ++
-    add "encoding_use_utf8" [string_of_bool p.encoding_use_utf8] ++
-    add "encoding_manual" [p.encoding_manual] ++
+    add "encoding" [string_of_inputenc p.encoding] ++
 
     add "automatic_tactics" p.automatic_tactics ++
     add "cmd_print" [p.cmd_print] ++
@@ -217,19 +246,18 @@ let save_pref () =
     add "query_window_width" [string_of_int p.query_window_width] ++
     add "auto_complete" [string_of_bool p.auto_complete] ++
     add "stop_before" [string_of_bool p.stop_before] ++
-    add "lax_syntax" [string_of_bool p.lax_syntax] ++
     add "vertical_tabs" [string_of_bool p.vertical_tabs] ++
     add "opposite_tabs" [string_of_bool p.opposite_tabs] ++
+    add "background_color" [p.background_color] ++
+    add "processing_color" [p.processing_color] ++
+    add "processed_color" [p.processed_color] ++
     Config_lexer.print_file pref_file
 
 let load_pref () =
-  let accel_dir = List.find
-    (fun x -> Sys.file_exists (Filename.concat x "coqide.keys"))
-    Minilib.xdg_config_dirs in
-  GtkData.AccelMap.load (Filename.concat accel_dir "coqide.keys");
+  let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in
   let p = !current in
 
-    let m = Config_lexer.load_file pref_file in
+    let m = Config_lexer.load_file loaded_pref_file in
     let np = { p with cmd_coqc = p.cmd_coqc } in
     let set k f = try let v = Minilib.Stringmap.find k m in f v with _ -> () in
     let set_hd k f = set k (fun v -> f (List.hd v)) in
@@ -239,6 +267,8 @@ let load_pref () =
     let set_command_with_pair_compat k f =
       set k (function [v1;v2] -> f (v1^"%s"^v2) | [v] -> f v | _ -> raise Exit)
     in
+    let set_option k f = set k (fun v -> f (match v with |[] -> None |h::_ ->  Some h)) in
+    set_option "cmd_coqtop" (fun v -> np.cmd_coqtop <- v);
     set_hd "cmd_coqc" (fun v -> np.cmd_coqc <- v);
     set_hd "cmd_make" (fun v -> np.cmd_make <- v);
     set_hd "cmd_coqmakefile" (fun v -> np.cmd_coqmakefile <- v);
@@ -249,9 +279,7 @@ let load_pref () =
     set_bool "auto_save" (fun v -> np.auto_save <- v);
     set_int "auto_save_delay" (fun v -> np.auto_save_delay <- v);
     set_pair "auto_save_name" (fun v1 v2 -> np.auto_save_name <- (v1,v2));
-    set_bool "encoding_use_locale" (fun v -> np.encoding_use_locale <- v);
-    set_bool "encoding_use_utf8" (fun v -> np.encoding_use_utf8 <- v);
-    set_hd "encoding_manual" (fun v -> np.encoding_manual <- v);
+    set_hd "encoding_manual" (fun v -> np.encoding <- (inputenc_of_string v));
     set_hd "project_options"
       (fun v -> np.read_project <- (project_behavior_of_string v));
     set_hd "project_file_name" (fun v -> np.project_file_name <- v);
@@ -290,15 +318,21 @@ let load_pref () =
     set_int "query_window_height" (fun v -> np.query_window_height <- v);
     set_bool "auto_complete" (fun v -> np.auto_complete <- v);
     set_bool "stop_before" (fun v -> np.stop_before <- v);
-    set_bool "lax_syntax" (fun v -> np.lax_syntax <- v);
     set_bool "vertical_tabs" (fun v -> np.vertical_tabs <- v);
     set_bool "opposite_tabs" (fun v -> np.opposite_tabs <- v);
+    set_hd "background_color" (fun v -> np.background_color <- v);
+    set_hd "processing_color" (fun v -> np.processing_color <- v);
+    set_hd "processed_color" (fun v -> np.processed_color <- v);
     current := np
 (*
     Format.printf "in load_pref: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
 *)
 
 let configure ?(apply=(fun () -> ())) () =
+  let cmd_coqtop =
+    string
+      ~f:(fun s -> !current.cmd_coqtop <- if s = "AUTO" then None else Some s)
+      "       coqtop" (match !current.cmd_coqtop with |None -> "AUTO" | Some x -> x) in
   let cmd_coqc =
     string
       ~f:(fun s -> !current.cmd_coqc <- s)
@@ -325,7 +359,7 @@ let configure ?(apply=(fun () -> ())) () =
     let w = GMisc.font_selection () in
     w#set_preview_text
       "Goal (∃n : nat, n ≤ 0)∧(∀x,y,z, x∈y⋃z↔x∈y∨x∈z).";
-    box#pack w#coerce;
+    box#pack ~expand:true w#coerce;
     ignore (w#misc#connect#realize
 	      ~callback:(fun () -> w#set_font_name
 			   (Pango.Font.to_string !current.text_font)));
@@ -338,9 +372,67 @@ let configure ?(apply=(fun () -> ())) () =
 (*
 	 Format.printf "in config_font: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
 *)
-	 !change_font !current.text_font)
+	 !refresh_font_hook ())
       true
   in
+
+  let config_color =
+    let box = GPack.vbox () in
+    let table = GPack.table
+      ~row_spacings:5
+      ~col_spacings:5
+      ~border_width:2
+      ~packing:(box#pack ~expand:true) ()
+    in
+    let background_label = GMisc.label
+      ~text:"Background color"
+      ~packing:(table#attach ~expand:`X ~left:0 ~top:0) ()
+    in
+    let processed_label = GMisc.label
+      ~text:"Background color of processed text"
+      ~packing:(table#attach ~expand:`X ~left:0 ~top:1) ()
+    in
+    let processing_label = GMisc.label
+      ~text:"Background color of text being processed"
+      ~packing:(table#attach ~expand:`X ~left:0 ~top:2) ()
+    in
+    let () = background_label#set_xalign 0. in
+    let () = processed_label#set_xalign 0. in
+    let () = processing_label#set_xalign 0. in
+    let background_button = GButton.color_button
+      ~color:(Tags.color_of_string (!current.background_color))
+      ~packing:(table#attach ~left:1 ~top:0) ()
+    in
+    let processed_button = GButton.color_button
+      ~color:(Tags.get_processed_color ())
+      ~packing:(table#attach ~left:1 ~top:1) ()
+    in
+    let processing_button = GButton.color_button
+      ~color:(Tags.get_processing_color ())
+      ~packing:(table#attach ~left:1 ~top:2) ()
+    in
+    let reset_button = GButton.button
+      ~label:"Reset"
+      ~packing:box#pack ()
+    in
+    let reset_cb () =
+      background_button#set_color (Tags.color_of_string "cornsilk");
+      processing_button#set_color (Tags.color_of_string "light blue");
+      processed_button#set_color (Tags.color_of_string "light green");
+    in
+    let _ = reset_button#connect#clicked ~callback:reset_cb in
+    let label = "Color configuration" in
+    let callback () =
+      !current.background_color <- Tags.string_of_color background_button#color;
+      !current.processing_color <- Tags.string_of_color processing_button#color;
+      !current.processed_color <- Tags.string_of_color processed_button#color;
+      !refresh_background_color_hook ();
+      Tags.set_processing_color processing_button#color;
+      Tags.set_processed_color processed_button#color
+    in
+    custom ~label box callback true
+  in
+
 (*
   let show_toolbar =
     bool
@@ -369,7 +461,7 @@ let configure ?(apply=(fun () -> ())) () =
     bool
       ~f:(fun s ->
 	    !current.auto_complete <- s;
-	    !auto_complete s)
+	    !auto_complete_hook s)
       "Auto Complete" !current.auto_complete
   in
 
@@ -416,44 +508,28 @@ let configure ?(apply=(fun () -> ())) () =
       "Stop interpreting before the current point" !current.stop_before
   in
 
-  let lax_syntax =
-    bool
-      ~f:(fun s -> !current.lax_syntax <- s)
-      "Relax read-only constraint at end of command" !current.lax_syntax
-  in
-
   let vertical_tabs =
     bool
-      ~f:(fun s -> !current.vertical_tabs <- s)
+      ~f:(fun s -> !current.vertical_tabs <- s; !refresh_tabs_hook ())
       "Vertical tabs" !current.vertical_tabs
   in
 
   let opposite_tabs =
     bool
-      ~f:(fun s -> !current.opposite_tabs <- s)
+      ~f:(fun s -> !current.opposite_tabs <- s; !refresh_tabs_hook ())
       "Tabs on opposite side" !current.opposite_tabs
   in
 
   let encodings =
     combo
       "File charset encoding "
-      ~f:(fun s ->
-	    match s with
-	    | "UTF-8" ->
-		!current.encoding_use_utf8 <- true;
-		!current.encoding_use_locale <- false
-	    | "LOCALE" ->
-		!current.encoding_use_utf8 <- false;
-		!current.encoding_use_locale <- true
-	    | _ ->
-		!current.encoding_use_utf8 <- false;
-		!current.encoding_use_locale <- false;
-		!current.encoding_manual <- s;
-	 )
+      ~f:(fun s -> !current.encoding <- (inputenc_of_string s))
       ~new_allowed: true
-      ["UTF-8";"LOCALE";!current.encoding_manual]
-      (if !current.encoding_use_utf8 then "UTF-8"
-       else if !current.encoding_use_locale then "LOCALE" else !current.encoding_manual)
+      ("UTF-8"::"LOCALE":: match !current.encoding with
+	|Emanual s -> [s]
+	|_ -> []
+      )
+      (string_of_inputenc !current.encoding)
   in
   let read_project =
     combo
@@ -579,11 +655,11 @@ let configure ?(apply=(fun () -> ())) () =
     bool
       ~f:(fun s ->
 	    !current.contextual_menus_on_goal <- s;
-	    !contextual_menus_on_goal s)
+	    !contextual_menus_on_goal_hook s)
       "Contextual menus on goal" !current.contextual_menus_on_goal
   in
 
-  let misc = [contextual_menus_on_goal;auto_complete;stop_before;lax_syntax;
+  let misc = [contextual_menus_on_goal;auto_complete;stop_before;
               vertical_tabs;opposite_tabs] in
 
 (* ATTENTION !!!!! L'onglet Fonts doit etre en premier pour eviter un bug !!!!
@@ -591,6 +667,7 @@ let configure ?(apply=(fun () -> ())) () =
   let cmds =
     [Section("Fonts", Some `SELECT_FONT,
 	     [config_font]);
+     Section("Colors", Some `SELECT_COLOR, [config_color]);
      Section("Files", Some `DIRECTORY,
 	     [global_auto_revert;global_auto_revert_delay;
 	      auto_save; auto_save_delay; (* auto_save_name*)
@@ -604,9 +681,8 @@ let configure ?(apply=(fun () -> ())) () =
 	     config_appearance);
 *)
      Section("Externals", None,
-	     [cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; cmd_print;
-	      cmd_editor;
-	      cmd_browse;doc_url;library_url]);
+	     [cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc;
+	      cmd_print;cmd_editor;cmd_browse;doc_url;library_url]);
      Section("Tactics Wizard", None,
 	     [automatic_tactics]);
      Section("Shortcuts", Some `PREFERENCES,
@@ -618,7 +694,7 @@ let configure ?(apply=(fun () -> ())) () =
 (*
   Format.printf "before edit: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
 *)
-  let x = edit ~apply ~width:500 "Customizations" cmds in
+  let x = edit ~apply "Customizations" cmds in
 (*
   Format.printf "after edit: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
 *)
diff --git a/ide/preferences.mli b/ide/preferences.mli
index f55088f1..b680c6f0 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -7,9 +7,11 @@
 (************************************************************************)
 
 type project_behavior = Ignore_args | Append_args | Subst_args
+type inputenc = Elocale | Eutf8 | Emanual of string
 
 type pref =
     {
+      mutable cmd_coqtop : string option;
       mutable cmd_coqc : string;
       mutable cmd_make : string;
       mutable cmd_coqmakefile : string;
@@ -25,9 +27,7 @@ type pref =
       mutable read_project : project_behavior;
       mutable project_file_name : string;
 
-      mutable encoding_use_locale : bool;
-      mutable encoding_use_utf8 : bool;
-      mutable encoding_manual : string;
+      mutable encoding : inputenc;
 
       mutable automatic_tactics : string list;
       mutable cmd_print : string;
@@ -57,9 +57,12 @@ type pref =
 *)
       mutable auto_complete : bool;
       mutable stop_before : bool;
-      mutable lax_syntax : bool;
       mutable vertical_tabs : bool;
       mutable opposite_tabs : bool;
+
+      mutable background_color : string;
+      mutable processing_color : string;
+      mutable processed_color : string;
     }
 
 val save_pref : unit -> unit
@@ -69,9 +72,11 @@ val current : pref ref
 
 val configure : ?apply:(unit -> unit) -> unit -> unit
 
-val change_font : ( Pango.font_description -> unit) ref
-val show_toolbar : (bool -> unit) ref
-val auto_complete : (bool -> unit) ref
-val resize_window : (unit -> unit) ref
+(* Hooks *)
+val refresh_font_hook : (unit -> unit) ref
+val refresh_background_color_hook : (unit -> unit) ref
+val refresh_toolbar_hook : (unit -> unit) ref
+val resize_window_hook : (unit -> unit) ref
+val refresh_tabs_hook : (unit -> unit) ref
 
 val use_default_doc_url : string
diff --git a/ide/tags.ml b/ide/tags.ml
index 52ba54dc..eeace465 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -13,6 +13,9 @@ let make_tag (tt:GText.tag_table) ~name prop =
   tt#add new_tag#as_tag;
   new_tag
 
+let processed_color = ref "light green"
+let processing_color = ref "light blue"
+
 module Script =
 struct
   let table = GText.tag_table ()
@@ -23,8 +26,8 @@ struct
   let comment = make_tag table ~name:"comment" [`FOREGROUND "brown"]
   let reserved = make_tag table ~name:"reserved" [`FOREGROUND "dark red"]
   let error = make_tag table ~name:"error" [`UNDERLINE `DOUBLE ; `FOREGROUND "red"]
-  let to_process = make_tag table ~name:"to_process" [`BACKGROUND "light blue" ;`EDITABLE false]
-  let processed = make_tag table ~name:"processed" [`BACKGROUND "light green" ;`EDITABLE false]
+  let to_process = make_tag table ~name:"to_process" [`BACKGROUND !processing_color ;`EDITABLE false]
+  let processed = make_tag table ~name:"processed" [`BACKGROUND !processed_color;`EDITABLE false]
   let unjustified = make_tag table ~name:"unjustified" [`UNDERLINE `SINGLE; `FOREGROUND "red"; `BACKGROUND "gold";`EDITABLE false]
   let found = make_tag table ~name:"found" [`BACKGROUND "blue"; `FOREGROUND "white"]
   let hidden = make_tag table ~name:"hidden" [`INVISIBLE true; `EDITABLE false]
@@ -35,7 +38,7 @@ end
 module Proof =
 struct
   let table = GText.tag_table ()
-  let highlight = make_tag table ~name:"highlight" [`BACKGROUND "light green"]
+  let highlight = make_tag table ~name:"highlight" [`BACKGROUND !processed_color]
   let hypothesis = make_tag table ~name:"hypothesis" []
   let goal = make_tag table ~name:"goal" []
 end
@@ -45,3 +48,27 @@ struct
   let error = make_tag table ~name:"error" [`FOREGROUND "red"]
 end
 
+let string_of_color clr =
+  let r = Gdk.Color.red clr in
+  let g = Gdk.Color.green clr in
+  let b = Gdk.Color.blue clr in
+  Printf.sprintf "#%04X%04X%04X" r g b
+
+let color_of_string s =
+  let colormap = Gdk.Color.get_system_colormap () in
+  Gdk.Color.alloc ~colormap (`NAME s)
+
+let get_processed_color () = color_of_string !processed_color
+
+let set_processed_color clr =
+  let s = string_of_color clr in
+  processed_color := s;
+  Script.processed#set_property (`BACKGROUND s);
+  Proof.highlight#set_property (`BACKGROUND s)
+
+let get_processing_color () = color_of_string !processing_color
+
+let set_processing_color clr =
+  let s = string_of_color clr in
+  processing_color := s;
+  Script.to_process#set_property (`BACKGROUND s)
diff --git a/ide/tags.mli b/ide/tags.mli
new file mode 100644
index 00000000..53a8c493
--- /dev/null
+++ b/ide/tags.mli
@@ -0,0 +1,50 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+module Script :
+sig
+  val table : GText.tag_table
+  val kwd : GText.tag
+  val qed : GText.tag
+  val decl : GText.tag
+  val proof_decl : GText.tag
+  val comment : GText.tag
+  val reserved : GText.tag
+  val error : GText.tag
+  val to_process : GText.tag
+  val processed : GText.tag
+  val unjustified : GText.tag
+  val found : GText.tag
+  val hidden : GText.tag
+  val folded : GText.tag
+  val paren : GText.tag
+  val sentence : GText.tag
+end
+
+module Proof :
+sig
+  val table : GText.tag_table
+  val highlight : GText.tag
+  val hypothesis : GText.tag
+  val goal : GText.tag
+end
+
+module Message :
+sig
+  val table : GText.tag_table
+  val error : GText.tag
+end
+
+val string_of_color : Gdk.color -> string
+val color_of_string : string -> Gdk.color
+
+val get_processed_color : unit -> Gdk.color
+val set_processed_color : Gdk.color -> unit
+
+val get_processing_color : unit -> Gdk.color
+val set_processing_color : Gdk.color -> unit
diff --git a/ide/utils/configwin.ml b/ide/utils/configwin.ml
index 3ff60799..4606ef29 100644
--- a/ide/utils/configwin.ml
+++ b/ide/utils/configwin.ml
@@ -60,9 +60,9 @@ let html = Configwin_ihm.html
 
 let edit
     ?(apply=(fun () -> ()))
-    title ?(width=400) ?(height=400)
+    title ?width ?height
     conf_struct_list =
-  Configwin_ihm.edit ~with_apply: true ~apply title ~width ~height conf_struct_list
+  Configwin_ihm.edit ~with_apply: true ~apply title ?width ?height conf_struct_list
 
 let get = Configwin_ihm.edit ~with_apply: false ~apply: (fun () -> ())
 
diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index 9ddc90ef..7dbd0452 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -1022,7 +1022,7 @@ class configuration_box (tt : GData.tooltips) conf_struct =
 
   let rec make_tree iter conf_struct =
     (* box is not shown at first *)
-    let box = GPack.vbox ~packing:menu_box#add ~show:false () in
+    let box = GPack.vbox ~packing:(menu_box#pack ~expand:true) ~show:false () in
     let new_iter = match iter with
     | None -> tree#append ()
     | Some parent -> tree#append ~parent ()
@@ -1136,12 +1136,12 @@ let tabbed_box conf_struct_list buttons tooltips =
    to configure the various parameters. *)
 let edit ?(with_apply=true)
     ?(apply=(fun () -> ()))
-    title ?(width=400) ?(height=400)
+    title ?width ?height
     conf_struct =
   let dialog = GWindow.dialog
     ~position:`CENTER
     ~modal: true ~title: title
-    ~height ~width
+    ?height ?width
     ()
   in
   let tooltips = GData.tooltips () in