From ceaec9b3e98da7978516f69abca33f65e10f3b03 Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Sat, 23 Jul 2016 15:58:47 +0200 Subject: Run "make magic" to update texi comments from elisp docstrings. --- doc/PG-adapting.texi | 3 +++ doc/ProofGeneral.texi | 37 +++++++++++++++++++++++++------------ 2 files changed, 28 insertions(+), 12 deletions(-) (limited to 'doc') diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 078fa93c..bd265a6a 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -1970,6 +1970,9 @@ This setting is used inside the function @samp{@code{proof-format-filename}}. @defvar proof-shell-process-connection-type The value of @samp{@code{process-connection-type}} for the proof shell.@* Set non-nil for ptys, nil for pipes. + +@var{note}: In emacs >= 24 (checked for 24 and 25.0.50.1), t is not a +good choice: input is cut after @var{4095} chars, which hangs pg. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-handle-error-or-interrupt-hook diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 05fb1b50..bd5e591f 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -4708,34 +4708,47 @@ path of @code{coqdep}. Non-standard coq library load path.@* This list specifies the LoadPath extension for coqdep, coqc and coqtop. Usually, the elements of this list are strings (for -"-I") or lists of two strings (for "-R" dir "-as" path). +"-I") or lists of two strings (for "-R" dir path and +"-Q" dir path). -The possible forms of elements of this list correspond to the 3 -forms of include options ('-I' and @code{'-R'}). An element can be +The possible forms of elements of this list correspond to the 4 +forms of include options (@samp{-I} @samp{-Q} and @samp{-R}). An element can be @lisp - - A string, specifying a directory to be mapped to the empty - logical path ('-I'). - - A list of the form '(rec dir path)' (where dir and path are + - A list of the form @samp{(}ocamlimport dir)', specifying (in 8.5) a + directory to be added to ocaml path (@samp{-I}). + - A list of the form @samp{(}rec dir path)' (where dir and path are strings) specifying a directory to be recursively mapped to the - logical path @code{'path'} ('-R dir -as path'). - - A list of the form '(nonrec dir path)', specifying a directory - to be mapped to the logical path @code{'path'} ('-I dir -as path'). + logical path @samp{path} (@samp{-R dir path}). + - A list of the form @samp{(}recnoimport dir path)' (where dir and + path are strings) specifying a directory to be recursively + mapped to the logical path @samp{path} (@samp{-Q dir path}), but not + imported (modules accessible for import with qualified names + only). Note that -Q dir "" has a special, nonrecursive meaning. + - A list of the form (8.4 only) @samp{(}nonrec dir path)', specifying a + directory to be mapped to the logical path @code{'path'} ('-I dir -as path'). @end lisp -For convenience the symbol @code{'rec'} can be omitted and entries of -the form '(dir path)' are interpreted as '(rec dir path)'. +For convenience the symbol @samp{rec} can be omitted and entries of +the form @samp{(dir path)} are interpreted as @samp{(rec dir path)}. + +A plain string maps to -Q ... "" in 8.5, and -I ... in 8.4. Under normal circumstances this list does not need to contain the coq standard library or "." for the current directory (see @samp{@code{coq-load-path-include-current}}). + +@var{warning}: if you use coq <= 8.4, the meaning of these options is +not the same (-I is for coq path). @end defvar @c TEXI DOCSTRING MAGIC: coq-load-path-include-current @defvar coq-load-path-include-current If @samp{t} let coqdep search the current directory too.@* -Should be @samp{t} for normal users. If @samp{t} pass "-I dir" to coqdep when +Should be @samp{t} for normal users. If @samp{t} pass -Q dir "" to coqdep when processing files in directory "dir" in addition to any entries in @samp{@code{coq-load-path}}. + +This setting is only relevant with Coq < 8.5. @end defvar -- cgit v1.2.3