From 0da47082b74d6f819641d163db443d6ba4cd6da6 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 12 May 2011 15:57:45 +0000 Subject: Update docstring magic --- doc/PG-adapting.texi | 9 ++++++--- doc/ProofGeneral.texi | 4 ++-- 2 files changed, 8 insertions(+), 5 deletions(-) (limited to 'doc') diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 9009235e..513bdbbe 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -345,12 +345,15 @@ under @samp{@code{proof-home-directory}}. Each entry is a list of the form @lisp - (@var{symbol} @var{name} @var{file-extension} [AUTOMODE-REGEXP]) + (@var{symbol} @var{name} @var{file-extension} [AUTOMODE-REGEXP] [IGNORED-EXTENSIONS-LIST]) @end lisp The @var{name} is a string, naming the proof assistant. The @var{symbol} is used to form the name of the mode for the assistant, @samp{SYMBOL-mode}, run when files with @var{automode-regexp} -(or with extension @var{file-extension}) are visited. +(or with extension @var{file-extension}) are visited. If present, +@var{ignored-extensions-list} is a list of file-name extensions to be +ignored when doing file-name completion (@var{ignored-extensions-list} +is added to @code{completion-ignored-extensions}). @var{symbol} is also used to form the name of the directory and elisp file for the mode, which will be @@ -360,7 +363,7 @@ file for the mode, which will be where @var{proof-home-directory} is the value of the variable @samp{@code{proof-home-directory}}. -The default value is @code{((isar "Isabelle" "thy") (coq "Coq" "v") (phox "PhoX" "phx") (lego "LEGO" "l"))}. +The default value is @code{((isar "Isabelle" "thy") (coq "Coq" "v" nil (".vo" ".glob")) (phox "PhoX" "phx") (lego "LEGO" "l"))}. @end defopt diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 1ff6d542..b6cb3531 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -4207,9 +4207,9 @@ command the following keys are substituted as follows: @lisp %p the (physical) directory containing the source of the required module - %o the coq object file in the physical directory that will + %o the Coq object file in the physical directory that will be loaded - %s the coq source file in the physical directory whose + %s the Coq source file in the physical directory whose object will be loaded %q the qualified id of the "Require" command %r the source file containing the "Require" -- cgit v1.2.3