TEMPORARY: add unicode-tokens2 mechanism to test across different machines

4 files changed, 176 insertions, 0 deletions

diff --git a/generic/pg-custom.el b/generic/pg-custom.el
index 238b76b4..64d8a97a 100644
--- a/generic/pg-custom.el
+++ b/generic/pg-custom.el
@@ -56,6 +56,12 @@ look for files named x-symbol-<PA>.el.")
   :set 'proof-set-value
   :group 'proof-user-options)
 
+(defpgcustom unicode-tokens2-enable nil
+  "*Non-nil for using Unicode token input mode in Proof General."
+  :type 'boolean
+  :set 'proof-set-value
+  :group 'proof-user-options)
+
 (defpgcustom mmm-enable nil
   "*Whether to use MMM Mode in Proof General for this assistant.
 MMM Mode allows multiple modes to be used in the same buffer.
diff --git a/generic/proof-auxmodes.el b/generic/proof-auxmodes.el
index a42ca070..809630bc 100644
--- a/generic/proof-auxmodes.el
+++ b/generic/proof-auxmodes.el
@@ -76,6 +76,22 @@
 	     (proof-unicode-tokens-support-available))
 	(proof-unicode-tokens-set-global t)))
 
+;;
+;; Unicode tokens 2 (temporary!)
+;; 
+(defun proof-unicode-tokens2-support-available ()
+  "A test to see whether unicode tokens2 support is available."
+  (and
+   (or (featurep 'unicode-tokens2)
+       (proof-try-require 'unicode-tokens2))
+   ;; Requires prover-specific config in <foo>-unicode-tokens2.el
+   (proof-try-require (proof-ass-sym unicode-tokens2))))
+
+(proof-eval-when-ready-for-assistant
+    (if (and (proof-ass unicode-tokens2-enable)
+	     (proof-unicode-tokens2-support-available))
+	(proof-unicode-tokens2-set-global t)))
+
 
 (provide 'proof-auxmodes)
 
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index af7950d1..968098e0 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -279,6 +279,8 @@ without adjusting window layout."
   (proof-deftoggle-fn 
    (proof-ass-sym unicode-tokens-enable) 'proof-unicode-tokens-toggle)
   (proof-deftoggle-fn 
+   (proof-ass-sym unicode-tokens2-enable) 'proof-unicode-tokens2-toggle)
+  (proof-deftoggle-fn 
    (proof-ass-sym maths-menu-enable) 'proof-maths-menu-toggle)
   (proof-deftoggle-fn (proof-ass-sym mmm-enable) 'proof-mmm-toggle))
 
@@ -332,6 +334,16 @@ without adjusting window layout."
       :selected (and (boundp 'unicode-tokens-mode) 
 		     unicode-tokens-mode)]
 
+     ["Unicode Tokens 2" 
+      (progn
+	(unless unicode-tokens2-mode (proof-x-symbol-toggle 0))
+	(proof-unicode-tokens2-toggle (if unicode-tokens2-mode 0 1)))
+      :active (and (not (and (boundp 'x-symbol-mode) x-symbol-mode))
+		   (proof-unicode-tokens2-support-available))
+      :style toggle
+      :selected (and (boundp 'unicode-tokens2-mode) 
+		     unicode-tokens2-mode)]
+
      ["Unicode Maths Menu" (proof-maths-menu-toggle (if maths-menu-mode 0 1))
       :active (proof-maths-menu-support-available)
       :style toggle
diff --git a/generic/proof-unicode-tokens2.el b/generic/proof-unicode-tokens2.el
new file mode 100644
index 00000000..377d7d8f
--- /dev/null
+++ b/generic/proof-unicode-tokens2.el
@@ -0,0 +1,142 @@
+;; proof-unicode-tokens2.el   Support Unicode tokens package
+;;
+;; Copyright (C) 2008 David Aspinall / LFCS Edinburgh
+;; Author:    David Aspinall <David.Aspinall@ed.ac.uk>
+;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
+;;
+;; $Id$
+;;
+
+(eval-when-compile
+  (require 'proof-utils) ; for proof-ass, proof-eval-when-ready-for-assistant
+  (require 'cl))
+
+(eval-when (compile)
+  (require 'unicode-tokens2)) ; it's loaded dynamically at runtime
+
+(defvar proof-unicode-tokens2-initialised nil
+  "Flag indicating whether or not we've performed startup.")
+
+(defun proof-unicode-tokens2-init ()
+  "Initialise settings for unicode tokens from prover specific variables."
+  (mapcar
+   (lambda (var) ;; or defass?
+     (if (boundp (proof-ass-symv var))
+	 (set (intern (concat "unicode-tokens2-" (symbol-name var)))
+	      (eval `(proof-ass ,var)))))
+   '(charref-format
+     token-format
+     control-token-format
+     token-name-alist
+     glyph-list
+     token-match
+     control-token-match
+     hexcode-match
+     next-character-regexp
+     token-prefix
+     token-suffix
+     shortcut-alist))
+  (unicode-tokens2-initialise)
+  (setq proof-unicode-tokens2-initialised t))
+  
+;;;###autoload
+(defun proof-unicode-tokens2-enable ()
+  "Turn on or off Unicode tokens mode in Proof General script buffer.
+This invokes `unicode-tokens2-mode' to toggle the setting for the current
+buffer, and then sets PG's option for default to match.
+Also we arrange to have unicode tokens mode turn itself on automatically 
+in future if we have just activated it for this buffer."
+  (interactive)
+  (when (proof-unicode-tokens2-support-available) ;; loads unicode-tokens2
+    (unless proof-unicode-tokens2-initialised
+      (proof-unicode-tokens2-init))
+    (proof-unicode-tokens2-set-global (not unicode-tokens2-mode))))
+
+
+;;;###autoload
+(defun proof-unicode-tokens2-set-global (flag)
+  "Set global status of unicode tokens mode for PG buffers to be FLAG.
+Turn on/off menu in all script buffers and ensure new buffers follow suit."
+  (unless proof-unicode-tokens2-initialised 
+      (proof-unicode-tokens2-init))
+  (let ((hook (proof-ass-sym mode-hook)))
+    (if flag
+	(add-hook hook 'unicode-tokens2-mode)
+      (remove-hook hook 'unicode-tokens2-mode))
+    (proof-map-buffers 
+      (proof-buffers-in-mode proof-mode-for-script)
+      (unicode-tokens2-mode (if flag 1 0)))
+    (proof-unicode-tokens2-shell-config)))
+
+  
+;;;
+;;; Interface to custom to dynamically change tables (via proof-set-value)
+;;;
+
+(defun proof-token-name-alist ()
+  "Function called after the current token name alist has been changed.
+Switch off tokens in all buffers, recalculate maps, turn on again."
+  (when proof-unicode-tokens2-initialised ; not on startup
+    (when (proof-ass unicode-tokens2-enable)
+      (proof-map-buffers 
+       (proof-buffers-in-mode proof-mode-for-script)
+       (unicode-tokens2-mode 0)))
+    (setq unicode-tokens2-token-name-alist (proof-ass token-name-alist))
+    (unicode-tokens2-initialise)
+    (when (proof-ass unicode-tokens2-enable)
+      (proof-map-buffers 
+       (proof-buffers-in-mode proof-mode-for-script)
+       (unicode-tokens2-mode 1)))))
+  
+(defun proof-shortcut-alist ()
+  "Function called after the shortcut alist has been changed.
+Updates the input mapping for reading shortcuts."
+  (when proof-unicode-tokens2-initialised ; not on startup
+    (setq unicode-tokens2-shortcut-alist (proof-ass shortcut-alist))
+    (unicode-tokens2-initialise)))
+
+;;;
+;;; Interface to shell
+;;;
+
+
+(defun proof-unicode-tokens2-activate-prover ()
+  (when (and proof-xsym-activate-command 
+	     (proof-shell-live-buffer)
+	     (proof-shell-available-p))
+    (proof-shell-invisible-command-invisible-result
+     proof-xsym-activate-command)))
+
+(defun proof-unicode-tokens2-deactivate-prover ()
+  (when (and proof-xsym-deactivate-command 
+	     ;; NB: clash with X-symbols since use same commands in prover!
+	     (not (proof-ass x-symbol-enable))
+	     (proof-shell-live-buffer)
+	     (proof-shell-available-p))
+    (proof-shell-invisible-command-invisible-result
+     proof-xsym-deactivate-command)))
+
+;;; NB: we shouldn't bother load this if it's not enabled.
+;;;###autoload
+(defun proof-unicode-tokens2-shell-config ()
+  (when (proof-ass unicode-tokens2-enable)
+    (add-hook 'proof-shell-insert-hook
+	      'proof-unicode-tokens2-encode-shell-input)
+    (proof-unicode-tokens2-activate-prover))
+  (unless (proof-ass unicode-tokens2-enable)
+    (remove-hook 'proof-shell-insert-hook
+		 'proof-unicode-tokens2-encode-shell-input)
+    (proof-unicode-tokens2-deactivate-prover)))
+
+(defun proof-unicode-tokens2-encode-shell-input ()
+  "Encode shell input in the variable STRING.
+A value for proof-shell-insert-hook."
+  (if (proof-ass unicode-tokens2-enable)
+      (with-temp-buffer ;; TODO: better to do directly in *prover*
+	(insert string)
+	(unicode-tokens2-unicode-to-tokens)
+	(setq string (buffer-substring-no-properties
+		      (point-min) (point-max))))))
+
+(provide 'proof-unicode-tokens2)
+;; End of proof-unicode-tokens2.el