diff options
| author | David Aspinall | 2010-09-08 11:06:36 +0000 |
|---|---|---|
| committer | David Aspinall | 2010-09-08 11:06:36 +0000 |
| commit | 7a2d1d01bcb4b55c93ce946c31bbdd60463989c2 (patch) | |
| tree | 58ad140702649ce3c318d5827c944829281823a2 /generic/proof-shell.el | |
| parent | eaa5a8ca6bffdb4f0686f0d5684b347c0757a060 (diff) | |
Script mouse face highlighting: new faces/colours for commands and regions, reinstate comment highlighting.
Diffstat (limited to 'generic/proof-shell.el')
| -rw-r--r-- | generic/proof-shell.el | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 58ea9844..fd52670b 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -38,17 +38,17 @@ "The main queue of things to do: spans, commands and actions. The value is a list of lists of the form - (SPAN COMMANDS ACTION [FLAGS]) + (SPAN COMMANDS ACTION [DISPLAYFLAGS]) -which is the queue of things to do. Flags are set for non-scripting -commands or for when scripting should not bother the user. -They may include +which is the queue of things to do. The display flags are set +for non-scripting commands or for when scripting should not +bother the user. They may include 'no-response-display do not display messages in *response* buffer 'no-error-display do not display errors/take error action 'no-goals-display do not goals in *goals* buffer -If flags are non-empty, other interactive cues will be surpressed. +If flags are non-empty, interactive cues will be surpressed. \(E.g., printing hints). See the functions `proof-start-queue' and `proof-shell-exec-loop'.") |