Add unicode-tokens-enable

2 files changed, 45 insertions, 7 deletions

diff --git a/generic/pg-custom.el b/generic/pg-custom.el
index f977ae97..09bcc197 100644
--- a/generic/pg-custom.el
+++ b/generic/pg-custom.el
@@ -36,6 +36,7 @@ whether X-Symbol is installed in your Emacs."
   :set 'proof-set-value
   :group 'proof-user-options)
 
+;; todo: can remove this one now, rename isabelle-x-symbol -> isar-x-symbol
 (defpgcustom x-symbol-language proof-assistant-symbol
   "Setting for x-symbol-language for the current proof assistant.
 It defaults to proof-assistant-symbol, which makes X Symbol
@@ -47,6 +48,12 @@ look for files named x-symbol-<PA>.el.")
   :set 'proof-set-value
   :group 'proof-user-options)
 
+(defpgcustom unicode-tokens-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-menu.el b/generic/proof-menu.el
index 0d4133ec..9ce34c69 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -275,8 +275,12 @@ without adjusting window layout."
 (proof-deftoggle proof-keep-response-history)
 
 (proof-eval-when-ready-for-assistant
-  (proof-deftoggle-fn (proof-ass-sym x-symbol-enable) 'proof-x-symbol-toggle)
-  (proof-deftoggle-fn (proof-ass-sym maths-menu-enable) 'proof-maths-menu-toggle)
+  (proof-deftoggle-fn 
+   (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 maths-menu-enable) 'proof-maths-menu-toggle)
   (proof-deftoggle-fn (proof-ass-sym mmm-enable) 'proof-mmm-toggle))
 
 
@@ -310,15 +314,42 @@ without adjusting window layout."
      ["Strict Read Only" proof-strict-read-only-toggle
       :style toggle
       :selected proof-strict-read-only]
-
-     ;; X-Symbol and MM are minor modes which PG settings
-     ;; enable by default for PG buffers
-     ["X-Symbol"  (proof-x-symbol-toggle (if x-symbol-mode 0 1))
+     
+     ["X-Symbol"
+      (proof-x-symbol-toggle (if x-symbol-mode 0 1))
       :active (proof-x-symbol-support-maybe-available)
       :style toggle
       :selected (and (boundp 'x-symbol-mode) x-symbol-mode)]
 
-     ["Maths Menu" (proof-maths-menu-toggle (if maths-menu-mode 0 1))
+;; switch between X-Symbol unicode/non-unicode
+;;      ["X-Symbol"
+;; 	      (progn
+;;  		(customize-set-variable 'x-symbol-use-unicode nil)
+;; 		(proof-x-symbol-toggle (if x-symbol-mode 0 1)))
+;;       :active (and (proof-x-symbol-support-maybe-available)
+;; 		   (not (and (featurep 'x-symbol) x-symbol-use-unicode)))
+;;       :style toggle
+;;       :selected (and (boundp 'x-symbol-mode) x-symbol-mode 
+;;		     (not x-symbol-use-unicode))]
+;; too many options and not quite working anyway
+;;      ["X-Symbol Unicode"  
+;; 	      (progn
+;;  		(customize-set-variable 'x-symbol-use-unicode t)
+;; 		(proof-x-symbol-toggle (if x-symbol-mode 0 1)))
+;;       :active  (and (proof-x-symbol-support-maybe-available)
+;; 		    (not (and (featurep 'x-symbol) (not x-symbol-use-unicode))))
+;;       :style toggle
+;;       :selected (and (boundp 'x-symbol-mode) x-symbol-mode
+;; 		     x-symbol-use-unicode)]
+
+     ["Unicode Tokens" (proof-unicode-tokens-toggle 
+			(if unicode-tokens-mode 0 1))
+      :active (proof-unicode-tokens-support-available)
+      :style toggle
+      :selected (and (boundp 'unicode-tokens-mode) 
+		     unicode-tokens-mode)]
+
+     ["Unicode Maths Menu" (proof-maths-menu-toggle (if maths-menu-mode 0 1))
       :active (proof-maths-menu-support-available)
       :style toggle
       :selected (and (boundp 'maths-menu-mode) maths-menu-mode)]