From 8eb6639bd95715208cd1506072a277fa53422a95 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Sun, 10 Oct 2010 22:36:16 +0000 Subject: Update magic --- doc/PG-adapting.texi | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'doc/PG-adapting.texi') diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 1e30760b..63d3c697 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -376,7 +376,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") (hol-light "HOL Light" "ml"))}. +The default value is @code{((isar "Isabelle" "thy") (coq "Coq" "v") (phox "PhoX" "phx") (lego "LEGO" "l"))}. @end defopt @@ -2737,7 +2737,7 @@ in the @code{proof-assistants} setting. @c TEXI DOCSTRING MAGIC: proof-assistants @defopt proof-assistants Choice of proof assistants to use with Proof General.@* -A list of symbols chosen from: @code{'isar} @code{'coq} @code{'phox} @code{'lego} @code{'hol-light}. +A list of symbols chosen from: @code{'isar} @code{'coq} @code{'phox} @code{'lego}. If nil, the default will be ALL available proof assistants. Each proof assistant defines its own instance of Proof General, @@ -3015,7 +3015,8 @@ For locking files loaded by a proof assistant, we use the next function. Ensure @var{buffer} marked completely processed, completing with a single step. If buffer already contains a locked region, only the remainder of the -buffer is closed off atomically. +buffer is closed off atomically (although undo for the initial portion +is unlikely to work, the decoration may be worth retaining). This works for buffers which are not in proof scripting mode too, to allow other files loaded by proof assistants to be marked read-only. -- cgit v1.2.3