From 99d21e5c443ddbd1e773f1ef4baf2e9a6fe7b78c Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sun, 6 Sep 2009 14:02:15 +0000
Subject: Remove use-specials-for-fontify

---
 CHANGES                 | 3 ++-
 generic/proof-config.el | 9 ---------
 2 files changed, 2 insertions(+), 10 deletions(-)

diff --git a/CHANGES b/CHANGES
index 53458b4a..fc7e6c34 100644
--- a/CHANGES
+++ b/CHANGES
@@ -36,10 +36,11 @@
     proof-toolbar-use-button-enablers  (now always used)
     proof-output-fontify-enable        (now always enabled)
 
-*** Altered prover configuration settings
+*** Altered prover configuration settings (internal)
     pg-insert-output-as-comment-fn: removed
     proof-shell-wakeup-char: removed
     proof-shell-prompt-pattern: removed
+    pg-use-specials-for-fontify: removed
     proof-shell-strip-output-markup: required for cut-and-paste
     proof-electric-terminator-noterminator: allows non-insert of terminator
 
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 675615f3..277295a6 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1351,20 +1351,11 @@ data triggered by `proof-shell-retract-files-regexp'."
   :type '(choice function (const nil))
   :group 'proof-shell)
 
-(defcustom pg-use-specials-for-fontify nil
-  "Flag indicating whether to strip annotations from output or not;
-\"annotations\" consist of special characters according to
-`pg-special-char-regexp'. If annotations are left in, they are made
-invisible and can be used to do syntax highlighting with font-lock."
-  :type 'boolean
-  :group 'proof-shell)
-
 (defcustom pg-special-char-regexp "[\200-\377]"
   "Regexp matching any \"special\" character sequence."
   :type 'string
   :group 'proof-shell)
 
-
 (defcustom proof-shell-set-elisp-variable-regexp nil
   "Matches output telling Proof General to set some variable.
 This allows the proof assistant to configure Proof General directly
-- 
cgit v1.2.3