diff options
| -rw-r--r-- | generic/pg-goals.el | 1 | ||||
| -rw-r--r-- | generic/proof-config.el | 18 | ||||
| -rw-r--r-- | generic/proof-utils.el | 17 | ||||
| -rw-r--r-- | isa/isa.el | 2 | ||||
| -rw-r--r-- | isa/isabelle-system.el | 9 | ||||
| -rw-r--r-- | isar/isar.el | 2 |
6 files changed, 36 insertions, 13 deletions
diff --git a/generic/pg-goals.el b/generic/pg-goals.el index e73eca3b..6869bab9 100644 --- a/generic/pg-goals.el +++ b/generic/pg-goals.el @@ -101,7 +101,6 @@ and properly fontifies STRING using proof-fontify-region." ;; but keep specials in case also used for subterm markup. (proof-fontify-region (point-min) (point-max) 'keepspecials)) - (run-hooks 'pg-before-subterm-markup-hook) (pg-goals-analyse-structure (point-min) (point-max)) (unless pg-use-specials-for-fontify diff --git a/generic/proof-config.el b/generic/proof-config.el index cbe5e434..bfcda272 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -30,7 +30,7 @@ ;; 6. Goals buffer configuration ;; [ 7. Splash screen settings -- moved to proof-splash.el now ] ;; 8. X-Symbol support -;; 9. Prover specific settings [NEW in 3.2 -- using new mechanism] +;; 9. Prover specific settings ;; 10. Global constants ;; ;; The user options don't need to be set on a per-prover basis, @@ -1014,6 +1014,9 @@ match the entire command" (defcustom proof-non-undoables-regexp nil "Regular expression matching commands which are *not* undoable. +These are commands which should not appear in proof scripts, +for example, undo commands themselves (if the proof assistant +cannot \"redo\" an \"undo\"). Used in default functions `proof-generic-state-preserving-p' and `proof-generic-count-undos'. If you don't use those, may be left as nil." @@ -2155,7 +2158,9 @@ requested on an assumption." :group 'proof-goals) (defcustom pg-subterm-help-cmd nil - "Command to display help about a subterm." + "Command to display mouse help about a subterm. +This command is sent to the proof assistant, replacing %s by the +subterm that the mouse is over." :type '(choice nil string) :group 'proof-goals) @@ -2244,13 +2249,16 @@ See also proof-{script,shell,resp}-font-lock-keywords." :group 'proof-goals) (defcustom pg-before-fontify-output-hook nil - "This hook is called before fonfitying a region in an output buffer. + "This hook is called before fontifying a region in an output buffer. +A function on this hook can alter the region of the buffer within +the current restriction, and must return the final value of (point-max). [This hook is presently only used by phox-sym-lock]." :type '(repeat function) :group 'proof-goals) -(defcustom pg-before-subterm-markup-hook nil - "This hook is called before analysiing a region for subterm markup." +(defcustom pg-after-fontify-output-hook nil + "This hook is called before fonfitying a region in an output buffer. +[This hook is presently only used by Isabelle]." :type '(repeat function) :group 'proof-goals) diff --git a/generic/proof-utils.el b/generic/proof-utils.el index e0502010..416edbce 100644 --- a/generic/proof-utils.el +++ b/generic/proof-utils.el @@ -363,7 +363,9 @@ Returns new END value." ;; We fontify first because X-sym decoding changes char positions. ;; It's okay because x-symbol-decode works even without font lock. ;; Possible disadvantage is that font lock patterns can't refer - ;; to X-Symbol characters. + ;; to X-Symbol characters. + ;; NB: perhaps we can narrow within the whole function, but there + ;; was an earlier problem with doing that. (if proof-output-fontify-enable (progn ;; Temporarily set font-lock defaults @@ -379,11 +381,18 @@ Returns new END value." (progn (setq font-lock-cache-position (make-marker)) (set-marker font-lock-cache-position 0))) - - (run-hooks 'pg-before-fontify-output-hook) + + (save-restriction + (narrow-to-region start end) + (run-hooks 'pg-before-fontify-output-hook) + (setq end (point-max))) (font-lock-default-fontify-region start end nil) - ;; after-fontify hook might do this ugly zap commas thing. + ;; FIXME: after-fontify hook might do this ugly zap commas thing. (proof-zap-commas-region start end)))) + (save-restriction + (narrow-to-region start end) + (run-hooks 'pg-after-fontify-output-hook) + (setq end (point-max))) (if (and pg-use-specials-for-fontify (not keepspecials)) (progn (pg-remove-specials start end) @@ -219,7 +219,7 @@ and script mode." pg-subterm-start-char ?\372 pg-subterm-sep-char ?\373 pg-subterm-end-char ?\374 - pg-before-subterm-markup-hook 'isabelle-convert-idmarkup-to-subterm + pg-after-fontify-output-hook 'isabelle-convert-idmarkup-to-subterm ;'pg-remove-specials ;; FIXME: next one doesn't do quite the right thing, always returns 'a? pg-subterm-help-cmd "printyp (type_of (read \"%s\"))" diff --git a/isa/isabelle-system.el b/isa/isabelle-system.el index f6c32da8..5faf6928 100644 --- a/isa/isabelle-system.el +++ b/isa/isabelle-system.el @@ -411,9 +411,15 @@ until Proof General is restarted." (defun isabelle-convert-idmarkup-to-subterm () "Convert identifier markup to subterm markup. -This is a hook setting for `pg-before-subterm-markup-hook' to +This is a hook setting for `pg-after-fontify-output-hook' to enable identifiers to be highlighted. (To disable that behaviour, the function `pg-remove-specials' can be used instead)." + ;; NB: the order of doing this is crucial: it must happen after + ;; fontifying (since replaces chars used for fontifying), but before + ;; X-Sym decoding (since some chars used for fontifying may clash + ;; with X-Sym character codes: luckily those codes don't seem to + ;; cause problems for subterm markup). + ;; Future version of this should use PGML output in Isabelle2002. (goto-char (point-min)) (while (re-search-forward "\351\\|\352\\|\353\\|\354\\|\355\\|\356\\|\357" nil t) @@ -423,5 +429,6 @@ the function `pg-remove-specials' can be used instead)." (replace-match "\374" nil t))) + (provide 'isabelle-system) ;; End of isabelle-system.el diff --git a/isar/isar.el b/isar/isar.el index 5f38ef12..89832473 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -243,7 +243,7 @@ See -k option for Isabelle interface script." pg-subterm-start-char ?\372 pg-subterm-sep-char ?\373 pg-subterm-end-char ?\374 - pg-before-subterm-markup-hook 'isabelle-convert-idmarkup-to-subterm + pg-after-fontify-output-hook 'isabelle-convert-idmarkup-to-subterm ;'pg-remove-specials pg-subterm-help-cmd "term %s" |