diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1998-12-18 15:07:55 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1998-12-18 15:07:55 +0000 |
| commit | 23f70bdfb7039db97f92484bbfcd00c9e6d98422 (patch) | |
| tree | 9a8cf446a64cab62abbfd1fa2a7042217b3f69ed | |
| parent | 4a2663fad7bea63d2a30c32770433d1afb87c54d (diff) | |
Elaborated on scripting language limitations Isabelle "bug"
| -rw-r--r-- | doc/ProofGeneral.texi | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index cb651429..4071275f 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -3777,10 +3777,14 @@ indentation code is somewhat broken. Since Isabelle uses ML as a top-level language for writing proof-scripts, Proof General may have difficulty understanding scripts which stray too far away from the standard functions, tactics, and -tacticals. You will usually notice when a function, or whatever, -doesn't get highlighted as you might expect. This probably has no -detrimental impact on the interface unless you use your own variants -of the @code{goal} or @code{qed} forms. +tacticals, or include nested structure with semicolons within a +top-level phrase. You will usually notice when a function, or whatever, +doesn't get highlighted as you might expect, or when only part of a +top-level phrase gets parsed as a command and Proof General gets +``stuck''. Sometimes you will be able to fix things by changing the +script. Generally this probably has no detrimental impact on the +interface unless you use your own variants of the @code{goal} or +@code{qed} forms. @strong{Workaround:} Restrict yourself to standard proof script functions, or customize some of the variables from @file{isa.el} and |