From 619955d4b9949dd99a483fcf9daf8a4429301b82 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Sat, 5 Jul 2008 15:04:13 +0000 Subject: TEMPORARY: add unicode-tokens2 mechanism to test across different machines --- generic/pg-custom.el | 6 ++ generic/proof-auxmodes.el | 16 +++++ generic/proof-menu.el | 12 ++++ generic/proof-unicode-tokens2.el | 142 +++++++++++++++++++++++++++++++++++++++ 4 files changed, 176 insertions(+) create mode 100644 generic/proof-unicode-tokens2.el (limited to 'generic') 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-.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 -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 @@ -278,6 +278,8 @@ without adjusting window layout." (proof-ass-sym x-symbol-enable) 'proof-x-symbol-toggle) (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 +;; 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 -- cgit v1.2.3