From 8c6b24410a2ef8d9767bfc1f4c12c0bfa6a0605c Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 12 Aug 2002 08:31:22 +0000
Subject: Enable variable highlighting in case experimental features enabled.

---
 isa/isa.el | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'isa')

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 ===
-- 
cgit v1.2.3