Skip to content

Commit

Permalink
CoqIdE configuration file won't pollute your home anymore
Browse files Browse the repository at this point in the history
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14694 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information
pirbo authored and maximedenes committed Dec 23, 2011
1 parent 51c925a commit 2fdc8e6
Show file tree
Hide file tree
Showing 8 changed files with 42 additions and 33 deletions.
9 changes: 6 additions & 3 deletions CHANGES
Expand Up @@ -191,11 +191,14 @@ CoqIDE

- Coqide now runs coqtop as separated process, making it more robust:
coqtop subprocess can be interrupted, or even killed and relaunched
(cf button "Restart Coq", ex-"Go to Start"). For allowing such interrupts,
the Windows version of coqide now requires Windows >= XP SP1.
(cf button "Restart Coq", ex-"Go to Start"). For allowing such
interrupts, the Windows version of coqide now requires Windows >= XP
SP1.
- The Coqide parsing of sentences has be reworked and now supports
tactic delimitation via { }.
- Coqide now accepts the Abort command (wish #2357).
- Preference files have moved to $XDG_CONFIG_HOME/coq and accelerators
are not stored in a list anymore.

Tools

Expand All @@ -208,7 +211,7 @@ Tools
* More variables are given by coqtop -config, others are defined only if the
users doesn't have defined them elsewhere. Consequently, generated makefile
should work directly on any architecture.
* Packager can take advantage of $(DSTROOT) introduction
* Packagers can take advantage of $(DSTROOT) introduction

Changes from V8.2 to V8.3
=========================
Expand Down
21 changes: 9 additions & 12 deletions INSTALL.ide
Expand Up @@ -23,10 +23,10 @@ On Gentoo GNU/Linux, do:
Else, read the rest of this document to compile your own CoqIde.

REQUIREMENT:
- OCaml >= 3.10 with native threads support.
- OCaml >= 3.11 with native threads support.
- make world must succeed.
- The graphical toolkit GTK+ 2.x. See http://www.gtk.org.
The official supported version is at least 2.8.x.
The official supported version is at least 2.10.x.
You may still compile CoqIde with older versions and
use all features.
Run
Expand All @@ -42,7 +42,7 @@ REQUIREMENT:

- The OCaml bindings for GTK+ 2.x, lablgtk2.

You need at least version 2.10.0.
You need at least version 2.12.0.

Your distribution may contain precompiled packages. For
example, for Debian, run
Expand Down Expand Up @@ -104,17 +104,14 @@ INSTALLATION


NOTES
There are three configuration files located in your $(HOME) dir.
There are three configuration files located in your $(XDG_CONFIG_HOME)/coq dir.
You may need to set HOME to some sensible value under Windows.

- .coqiderc is generated by coqide itself. It may be edited by hand or
- coqiderc is generated by coqide itself. It may be edited by hand or
by using the Preference menu from coqide. It will be generated the first time
you save your the preferences in Coqide.

- .coqide-gtk2rc is a standard Gtk2 configuration file. A sample file can be
found in the coq lib "ide" subdir.

- .coqide.keys is a standard Gtk2 accelerator dump. You may edit this file
- coqide.keys is a standard Gtk2 accelerator dump. You may edit this file
to change the default shortcuts for the menus.

Read ide/FAQ for more informations.
Expand All @@ -127,8 +124,8 @@ TROUBLESHOOTING
Some users may experiment problems with unwanted automatic
templates while using Coqide. This is due to a change in the
modifiers keys available through GTK. The straightest way to get
rid of the problem is to edit by hand your .coqiderc (either
/home/<user>/.coqiderc under Linux, or
C:\Documents and Settings\<user>\.coqiderc under Windows)
rid of the problem is to edit by hand your coqiderc (either
/home/<user>/.config/coq/coqiderc under Linux, or
C:\Documents and Settings\<user>\.config\coq\coqiderc under Windows)
and replace any occurence of MOD4 by MOD1.

16 changes: 8 additions & 8 deletions doc/faq/FAQ.tex
Expand Up @@ -2347,8 +2347,8 @@ \section{\CoqIde}
\begin{itemize}

\item Insert \texttt{gtk-key-theme-name = "Emacs"}
in your \texttt{.coqide-gtk2rc} file. It may be in the current dir
or in \verb#$HOME# dir. This is done by default.
in your \texttt{coqide-gtk2rc} file. It should be in
\verb#$XDG_CONFIG_DIRS/coq# dir. This is done by default.

\item If in Gnome, run the gnome configuration editor (\texttt{gconf-editor})
and set key \texttt{gtk-key-theme} to \texttt{Emacs} in the category
Expand Down Expand Up @@ -2416,7 +2416,7 @@ \section{\CoqIde}
\verb=bind "F13" {"insert-at-cursor" ("=$\forall$\verb=")}=\\
\verb=bind "F14" {"insert-at-cursor" ("=$\exists$\verb=")}=

to your "binding "text"" section in \verb#.coqiderc-gtk2rc.#
to your "binding "text"" section in \verb#coqiderc-gtk2rc#.
The last arguments to {\tt bind} between "" are
the UTF-8 encodings for 0x2200 and 0x2203.
You can compute these encodings using the lablgtk2 toplevel with
Expand All @@ -2430,8 +2430,8 @@ \section{\CoqIde}
\Question{How to customize the shortcuts for menus?}
Two solutions are offered:
\begin{itemize}
\item Edit \$HOME/.coqide.keys by hand or
\item Add "gtk-can-change-accels = 1" in your .coqide-gtk2rc file. Then
\item Edit \$XDG_CONFIG_HOME/coq/coqide.keys (\$HOME/.config/coq/coqide.keys) by hand or
\item Add "gtk-can-change-accels = 1" in your coqide-gtk2rc file. Then
from \CoqIde, you may select a menu entry and press the desired
shortcut.
\end{itemize}
Expand All @@ -2451,9 +2451,9 @@ \section{\CoqIde}
Some users may experiment problems with unwanted automatic
templates while using Coqide. This is due to a change in the
modifiers keys available through GTK. The straightest way to get
rid of the problem is to edit by hand your .coqiderc (either
\verb|/home/<user>/.coqiderc| under Linux, or \\
\verb|C:\Documents and Settings\<user>\.coqiderc| under Windows)
rid of the problem is to edit by hand your coqiderc (either
\verb|/home/<user>/.config/coq/coqiderc| under Linux, or \\
\verb|C:\Documents and Settings\<user>\.config\coq\coqiderc| under Windows)
and replace any occurence of \texttt{MOD4} by \texttt{MOD1}.


Expand Down
10 changes: 5 additions & 5 deletions ide/FAQ
Expand Up @@ -6,8 +6,8 @@ R0: A powerfull graphical interface for Coq. See http://coq.inria.fr. for more i
Q1) How to enable Emacs keybindings?
R1: Insert
gtk-key-theme-name = "Emacs"
in your ".coqide-gtk2rc" file. It may be in the current dir
or in $HOME dir. This is done by default.
in your "coqide-gtk2rc" file. It should be in $XDG_CONFIG_DIRS/coq dir.
This is done by default.

Q2) How to enable antialiased fonts?
R2) Set the GDK_USE_XFT variable to 1. This is by default with Gtk >= 2.2.
Expand Down Expand Up @@ -41,7 +41,7 @@ R5)-First solution : type "<CONTROL><SHIFT>2200" to enter a forall in the script
and then to add
bind "F13" {"insert-at-cursor" ("∀")}
bind "F14" {"insert-at-cursor" ("∃")}
to your "binding "text"" section in .coqiderc-gtk2rc.
to your "binding "text"" section in coqiderc-gtk2rc.
The strange ("∀") argument is the UTF-8 encoding for
0x2200.
You can compute these encodings using the lablgtk2 toplevel with
Expand All @@ -51,8 +51,8 @@ R5)-First solution : type "<CONTROL><SHIFT>2200" to enter a forall in the script

Q6) How to customize the shortcuts for menus?
R6) Two solutions are offered:
- Edit $HOME/.coqide.keys by hand or
- Add "gtk-can-change-accels = 1" in your .coqide-gtk2rc file. Then
- Edit $XDG_CONFIG_HOME/coq/coqide.keys by hand or
- Add "gtk-can-change-accels = 1" in your coqide-gtk2rc file. Then
from CoqIde, you may select a menu entry and press the desired
shortcut.

Expand Down
4 changes: 2 additions & 2 deletions ide/config_lexer.mll
Expand Up @@ -25,7 +25,7 @@ rule prefs m = parse
|ignore* (ident as id) ignore* '=' { let conf = str_list [] lexbuf in
prefs (Stringmap.add id conf m) lexbuf }
| _ { let c = lexeme_start lexbuf in
eprintf ".coqiderc: invalid character (%d)\n@." c;
eprintf "coqiderc: invalid character (%d)\n@." c;
prefs m lexbuf }
| eof { m }

Expand All @@ -41,7 +41,7 @@ and string = parse
| '"' { Buffer.add_char string_buffer '"' }
| '\\' '"' | _
{ Buffer.add_string string_buffer (lexeme lexbuf); string lexbuf }
| eof { eprintf ".coqiderc: unterminated string\n@." }
| eof { eprintf "coqiderc: unterminated string\n@." }

{

Expand Down
8 changes: 7 additions & 1 deletion ide/minilib.ml
Expand Up @@ -70,7 +70,13 @@ let subst_command_placeholder s t =
let home =
try Sys.getenv "HOME" with Not_found ->
try (Sys.getenv "HOMEDRIVE")^(Sys.getenv "HOMEPATH") with Not_found ->
try Sys.getenv "USERPROFILE" with Not_found -> "."
try Sys.getenv "USERPROFILE" with Not_found -> Filename.current_dir_name

let xdg_config_home =
try
Filename.concat (Sys.getenv "XDG_CONFIG_HOME") "coq"
with Not_found ->
Filename.concat home "/.config/coq"

let coqlib = ref ""
let coqtop_path = ref ""
Expand Down
1 change: 1 addition & 0 deletions ide/minilib.mli
Expand Up @@ -22,6 +22,7 @@ val string_map : (char -> char) -> string -> string
val subst_command_placeholder : string -> string -> string

val home : string
val xdg_config_home : string

val coqlib : string ref
val coqtop_path : string ref
Expand Down
6 changes: 4 additions & 2 deletions ide/preferences.ml
Expand Up @@ -10,9 +10,9 @@
open Configwin
open Printf

let pref_file = Filename.concat Minilib.home ".coqiderc"
let pref_file = Filename.concat Minilib.xdg_config_home "coqiderc"

let accel_file = Filename.concat Minilib.home ".coqide.keys"
let accel_file = Filename.concat Minilib.xdg_config_home "coqide.keys"

let mod_to_str (m:Gdk.Tags.modifier) =
match m with
Expand Down Expand Up @@ -168,6 +168,8 @@ 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 p = !current in
Expand Down

0 comments on commit 2fdc8e6

Please sign in to comment.