diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-09-08 11:06:36 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-09-08 11:06:36 +0000 |
| commit | 7a2d1d01bcb4b55c93ce946c31bbdd60463989c2 (patch) | |
| tree | 58ad140702649ce3c318d5827c944829281823a2 /generic | |
| parent | eaa5a8ca6bffdb4f0686f0d5684b347c0757a060 (diff) | |
Script mouse face highlighting: new faces/colours for commands and regions, reinstate comment highlighting.
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-faces.el | 18 | ||||
| -rw-r--r-- | generic/proof-shell.el | 10 |
2 files changed, 23 insertions, 5 deletions
diff --git a/generic/proof-faces.el b/generic/proof-faces.el index 9cc01e83..671e1596 100644 --- a/generic/proof-faces.el +++ b/generic/proof-faces.el @@ -155,6 +155,22 @@ Warning messages can come from proof assistant or from Proof General itself." "*General mouse highlighting face used in script buffer." :group 'proof-faces) +(defface proof-command-mouse-highlight-face + (proof-face-specs + (:background "gold1") + (:background "gold4") + (:italic t)) + "*Mouse highlighting face for atomic regions (usually commands) in script buffer." + :group 'proof-faces) + +(defface proof-region-mouse-highlight-face + (proof-face-specs + (:background "yellow2") + (:background "yellow3") + (:italic t)) + "*Mouse highlighting face for compound regions (usually proofs) in script buffer." + :group 'proof-faces) + (defface proof-highlight-dependent-face (proof-face-specs (:background "orange") @@ -213,6 +229,8 @@ Warning messages can come from proof assistant or from Proof General itself." (defconst proof-debug-message-face 'proof-debug-message-face proof-face-compat-doc) (defconst proof-boring-face 'proof-boring-face proof-face-compat-doc) (defconst proof-mouse-highlight-face 'proof-mouse-highlight-face proof-face-compat-doc) +(defconst proof-command-mouse-highlight-face 'proof-command-mouse-highlight-face proof-face-compat-doc) +(defconst proof-region-mouse-highlight-face 'proof-region-mouse-highlight-face proof-face-compat-doc) (defconst proof-highlight-dependent-face 'proof-highlight-dependent-face proof-face-compat-doc) (defconst proof-highlight-dependency-face 'proof-highlight-dependency-face proof-face-compat-doc) (defconst proof-active-area-face 'proof-active-area-face proof-face-compat-doc) 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'.") |