From 849b0d81fce498ef52e90d3cb1710e741bcf9b97 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 10 Jul 2008 20:11:26 +0000 Subject: Extend documentation for logic setting mechanism (needs magic update) --- doc/ProofGeneral.texi | 92 +++++++++++++++++++++++++++++++-------------------- 1 file changed, 56 insertions(+), 36 deletions(-) diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 60723013..d080f027 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -3773,11 +3773,61 @@ it is very hard to let Proof General lose synchronization with the Isabelle process. @menu +* Choosing logic and starting isabelle:: * Isabelle commands:: -* Logics and Settings:: +* Isabelle settings:: * Isabelle customizations:: @end menu +@node Choosing logic and starting isabelle +@section Choosing logic and starting isabelle +@cindex Isabelle logic + +When you load an Isabelle theory file into Proof General, you may be +prompted for the path to the program @code{isatool} if it is not on the +system @code{PATH} already. This is used to generate further +information for invoking Isabelle, in particular, the list of available +logics. + +The Isabelle menu offers an easy way to select the invoked object logic. +If you look at the menu: +@lisp + Isabelle -> Logics -> +@end lisp +you should see the list of logics available to Isabelle. This menu is +generated from the output of the command @code{isatool findlogics}. +(Similarly, the documentation menu is partly generated from +@code{isatool doc}). Instead of the menu, you can use the +keyboard command @code{isabelle-chose-logic} to choose from the list. + +The logics list is refreshed dynamically so you can select any newly +built heap images in the same Emacs session. However, notice that the +choices are greyed out while Isabelle is actually runnning --- you can +only switch to a new logic if you first exit Isabelle (similarly to +Proof General, Isabelle operates with only one logic at a time). + +Another way to set the logic before Isabelle is launched is using an +Emacs local variable setting inside a comment at the top of the file, +see the documentation of @code{isabelle-chosen-logic} below. + +In case you do not have the @code{isatool} program available or want to +override its behaviour, you may set the variable +@code{isabelle-program-name-override} to define the name of the +executable used to start Isabelle. The standard options are and +logic name are still appended. +@c in fact, we also have ISABELLE_OPTIONS and PROOFGENERAL_LOGIC, +@c but lets not mention these. + + +@c TEXI DOCSTRING MAGIC: isabelle-program-name-override + +@c TEXI DOCSTRING MAGIC: isabelle-chosen-logic + +@c TEXI DOCSTRING MAGIC: isabelle-choose-logic + + + + @node Isabelle commands @section Isabelle commands @cindex Isabelle commands @@ -3809,8 +3859,6 @@ The Isabelle instance of Proof General supplies several specific help key bindings; these functions are offered within the prover help menu as well. - - @table @kbd @item C-c C-a r Invokes Isar command @code{refute} on the current subgoal. Only available in HOL @@ -3923,31 +3971,10 @@ Remove explicit Isabelle/Isar command terminators @samp{;} from the buffer. @end deffn -@node Logics and Settings -@section Logics and Settings -@cindex Isabelle logic - -The prover specific menu (the same on both Isabelle variants of Proof -General) offers a way to select the invoked object logic, and also -access to numerous settings of Isabelle. - -If you look at the menu: -@lisp - Isabelle -> Logics -> -@end lisp -you should see the list of logics available to Isabelle. This menu is -generated from the output of the command @code{isatool findlogics}, so -you should check that Proof General can find the @code{isatool} program -for it to operate correctly. (Similarly, the documentation menu is -partly generated from @code{isatool doc}). - -The logics menu is refreshed dynamically so you can select any newly -built heap images in the same Emacs session. However, notice that the -choices are greyed out while Isabelle is actually runnning --- you can -only switch to a new logic if you first exit Isabelle (similarly to -Proof General, Isabelle operates with only one logic at a time). +@node Isabelle settings +@section Isabelle settings -The prover specific menu also contains a @code{Settings} submenu, which +The Isabelle menu also contains a @code{Settings} submenu, which allows you to configure things such as the behaviour of Isabelle's term pretty printer (display of types, sorts, etc). Note that you won't see this sub-menu until Isabelle has been started, because it is @@ -3956,21 +3983,14 @@ responsible for recording any settings that are configured when you select @code{Isabelle -> Settings -> Save Settings}. They are stored along with the other Emacs customization settings. -@c TEXI DOCSTRING MAGIC: isabelle-chosen-logic -@defvar isabelle-chosen-logic -URL of web page for Isabelle. -@end defvar - - @node Isabelle customizations @section Isabelle customizations @cindex Isabelle customizations - -Here are some of the user options specific to Isabelle. You can set -these as usual with the customization mechanism. +Here are some of the other user options specific to Isabelle. You can +set these as usual with the customization mechanism. @c TEXI DOCSTRING MAGIC: isabelle-web-page @defvar isabelle-web-page -- cgit v1.2.3