Comments

3 files changed, 32 insertions, 18 deletions

diff --git a/generic/proof-config.el b/generic/proof-config.el
index bfcda272..a8900e4c 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -2283,9 +2283,14 @@ tokens (for example, editing documentation or source code files)."
   :type '(repeat symbol)
   :group 'proof-x-symbol)
 
-;; I don't really know what this setting is good for?
+;; FIXME: should perhaps be one of these per prover
+;; FIXME: actually this setting doesn't seem to be needed:
+;; instead X-Symbol uses x-symbol-<lang>-font-lock-keywords.
 (defcustom proof-xsym-font-lock-keywords nil
-  "Font lock keywords to use for the proof assistants X-Symbol token language."
+  "Font lock keywords to use for the proof assistants X-Symbol token language.
+This should be set to the additional font-lock-keywords used for the
+proof assistant when X-Symbol is enabled.  (For example, additional
+keywords used for bold or superscript text: see isa/x-symbol-isabelle.el)"
   :type 'sexp
   :group 'proof-x-symbol)
 
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 416edbce..94527602 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -353,7 +353,8 @@ font-lock-mode."
 (defun proof-fontify-region (start end &optional keepspecials)
   "Fontify and decode X-Symbols in region START...END.
 Fontifies according to the buffer's font lock defaults.
-Uses proof-x-symbol-decode to decode tokens if x-symbol is present.
+Uses `proof-x-symbol-decode-region' to decode tokens
+if X-Symbol is enabled.
 
 If `pg-use-specials-for-fontify' is set, remove characters
 with top bit set after fontifying so they don't spoil cut and paste,
@@ -403,13 +404,8 @@ Returns new END value."
     (proof-font-lock-clear-font-lock-vars)))
 
 
-(defconst pg-special-char-regexp
-  (let ((c 128) (r "\200"))
-    (while (< c 256) 
-      (setq r (concat r "\\|" (regexp-quote (char-to-string c))))
-      (incf c))
-    r)
-  "Regexp matchin any special character (top bit set).")
+(defconst pg-special-char-regexp "[\200-\377]" 
+  "Regexp matching any \"special\" character (top bit set).")
 
 
 (defun pg-remove-specials (&optional start end)
diff --git a/generic/proof-x-symbol.el b/generic/proof-x-symbol.el
index b9fc3aee..7e5718bb 100644
--- a/generic/proof-x-symbol.el
+++ b/generic/proof-x-symbol.el
@@ -16,6 +16,24 @@
 ;;
 ;; $Id$
 ;;
+;; =================================================================
+;;
+;; Notes on interacing to X-Symbol.
+;;
+;; 1. Proof script buffers.
+;; Font lock and X-Symbol minor modes are engaged as usual.
+;; Rather than using piecemeal enabling of X-Symbol
+;; or putting it onto an auto-mode list, we use
+;; proof-x-symbol-enable to cleanly turn on/off 
+;; X-Symbol in all PG buffers.
+;;
+;; 2. Output buffers (goals, response, tracing)
+;; Neither font-lock nor X-Symbol mode is engaged.
+;; Instead, we simply set `x-symbol-language', and call
+;; `x-symbol-decode' or `x-symbol-decode-region', via
+;; `proof-fontify-region' (which see).
+;;
+
 
 (defvar proof-x-symbol-initialized nil
   "Non-nil if x-symbol support has been initialized.")
@@ -112,9 +130,6 @@ The package is available at http://x-symbol.sourceforge.net/"))
 	  (set symmodelinevar symmodelinenm)
 	  (x-symbol-register-language xs-lang xs-feature-sym all-xs-modes)
 	  ;; Put the extra modes on the auto-mode-alist
-	  ;; 3.0: don't bother: rashly assume that their mode
-	  ;; functions invoke proof-x-symbol-mode.  That way we can
-	  ;; turn on/off cleanly in proof-x-symbol-mode-all-buffers.
 	  ;; (if xs-xtra-modes (push am-entry x-symbol-auto-mode-alist))
 	  ;; Okay, let's be less rash and put it on a hook list.
 	  ;; 12.1.00: Nope, there's a problem here!  
@@ -153,9 +168,6 @@ Calls proof-x-symbol-toggle-clean-buffers afterwards."
   (proof-x-symbol-mode-all-buffers)
   (proof-x-symbol-toggle-clean-buffers))
 
-;; First inclination was to put this function in a hook called by
-;; enable function.  But rather than proliferate hooks needlessly, it
-;; seems better to wait to find out whether they're really needed.
 (defun proof-x-symbol-toggle-clean-buffers ()
   "Clear the response buffer and send proof-showproof-command.
 This function is intended to clean the display after a change
@@ -182,6 +194,8 @@ Return new END value."
 	  (point-max)))
     end))
 
+;; FIXME: see whether X-Symbol's supplied hook does the right
+;; thing here.
 (defun proof-x-symbol-encode-shell-input ()
   "Encode shell input in the variable STRING.
 A value for proof-shell-insert-hook."
@@ -343,8 +357,7 @@ Assumes that the current buffer is the proof shell buffer."
     (progn
       (proof-x-symbol-initialize)
       (unless proof-x-symbol-initialized
-	;; If initialization failed, turn off
-	;; x-symbol-enable for the session.
+	;; If init failed, turn off x-symbol-enable for the session.
 	(customize-set-variable (proof-ass-sym x-symbol-enable) nil))))
 
 (provide 'proof-x-symbol)