Enable variable highlighting in case experimental features enabled.

1 files changed, 6 insertions, 3 deletions

diff --git a/isa/isa.el b/isa/isa.el
index 2dc4f231..45e893d0 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -217,9 +217,12 @@ and script mode."
    pg-subterm-start-char		?\372
    pg-subterm-sep-char			?\373
    pg-subterm-end-char			?\374
-   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-after-fontify-output-hook		
+   (if proof-experimental-features 
+       'isabelle-convert-idmarkup-to-subterm 'pg-remove-specials)
+   ;; FIXME: next one doesn't do the right thing, it always returns 'a
+   ;; since variables are out-of-scope.  Better would be to simply
+   ;; print the variable's kind.
    pg-subterm-help-cmd			"printyp (type_of (read \"%s\"))"
 
    ;; === MULTIPLE FILE HANDLING ===