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 ++++++---
 isar/isar.el | 5 +++--
 2 files changed, 9 insertions(+), 5 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 ===
diff --git a/isar/isar.el b/isar/isar.el
index 4d08f5b3..b3e283d7 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -240,8 +240,9 @@ See -k option for Isabelle interface script."
    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
+   pg-after-fontify-output-hook	
+   (if proof-experimental-features 
+       'isabelle-convert-idmarkup-to-subterm 'pg-remove-specials)
    pg-subterm-help-cmd			"term %s" 
 
    proof-shell-process-file
-- 
cgit v1.2.3