diff options
Diffstat (limited to 'isa')
-rw-r--r-- | isa/isa.el | 2 | ||||
-rw-r--r-- | isa/isabelle-system.el | 9 |
2 files changed, 9 insertions, 2 deletions
@@ -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 |