Add indirection for setting unicode tokens variables to add customize menu options

4 files changed, 94 insertions, 36 deletions

diff --git a/coq/coq-unicode-tokens.el b/coq/coq-unicode-tokens.el
index d18964a2..c0691d85 100644
--- a/coq/coq-unicode-tokens.el
+++ b/coq/coq-unicode-tokens.el
@@ -78,7 +78,7 @@ in this table.  When the file is saved, the reverse is done.
 The string mapping can be anything, but should be such that
 tokens can be uniquely recovered from a decoded text; otherwise
 results will be undefined when files are saved."
-  :type '(repeat (cons (string :tag "Token name")
+  :type '(repeat (list (string :tag "Token name")
 		       (string :tag "Unicode string")))
   :set 'proof-set-value
   :group 'coq
@@ -161,13 +161,13 @@ You can adjust this table to add more entries, or to change entries for
 glyphs that not are available in your Emacs or chosen font.
 
 These shortcuts are only used for input; no reverse conversion is
-performed.  But if tokens exist for the target of shortcuts, they
-will be used on saving the buffer."
+performed.  This means that the target strings need to have a defined 
+meaning to be useful."
   :type '(repeat (cons (string :tag "Shortcut sequence")
 		       (string :tag "Unicode string")))
   :set 'proof-set-value
   :group 'isabelle
-  :tag "Coq Unicode Token Mapping")
+  :tag "Coq Unicode Input Shortcuts")
 
   
 ;;
diff --git a/generic/proof-unicode-tokens.el b/generic/proof-unicode-tokens.el
index b636eaa5..414d580c 100644
--- a/generic/proof-unicode-tokens.el
+++ b/generic/proof-unicode-tokens.el
@@ -45,12 +45,11 @@
 (defun proof-unicode-tokens-configure ()
   "Set the Unicode Tokens table from prover instances and initialise."
   (require 'unicode-tokens) ; load now, for unicode-tokens-configuration-variables
-  (mapcar
-   (lambda (var) ;; or defass?
-     (if (boundp (proof-ass-symv var))
-	 (set (intern (concat "unicode-tokens-" (symbol-name var)))
-	      (eval `(proof-ass ,var)))))
-   unicode-tokens-configuration-variables)
+  (dolist (var unicode-tokens-configuration-variables)
+    (if (boundp (proof-ass-symv var))
+	(set (intern (concat "unicode-tokens-" (symbol-name var)
+			     "-variable"))
+	     (proof-ass-symv var))))
   (unicode-tokens-initialise))
 
   
diff --git a/isar/isar-unicode-tokens.el b/isar/isar-unicode-tokens.el
index 927a9417..41a7c16b 100644
--- a/isar/isar-unicode-tokens.el
+++ b/isar/isar-unicode-tokens.el
@@ -440,15 +440,16 @@ tokens.")
   (isar-map-letters (lambda (x) (format "%c%c" x x))
 		    (lambda (x) (format "%c" x))
 		    'frakt))
-  
-(defcustom isar-token-symbol-map
-  (append
-   isar-symbols-tokens
-   isar-symbols-tokens-fallbacks
-   isar-greek-letters-tokens
-   isar-bold-nums-tokens
-   isar-script-letters-tokens
-   isar-roman-letters-tokens)
+
+;; like defcustom, but want to evaluate default
+(custom-declare-variable 'isar-token-symbol-map
+   (list 'quote (append
+       isar-symbols-tokens
+       isar-symbols-tokens-fallbacks
+       isar-greek-letters-tokens
+       isar-bold-nums-tokens
+       isar-script-letters-tokens
+       isar-roman-letters-tokens))
   "Table mapping Isabelle symbol token names to Unicode strings.
 
 You can adjust this table to add more entries, or to change entries for
@@ -458,8 +459,20 @@ The token TNAME is made into the token \\< TNAME >.
 The string mapping can be anything, but should be such that
 tokens can be uniquely recovered from a decoded text; otherwise
 results will be undefined when files are saved."
-  :type '(repeat (list (string :tag "Token name")
-		       (string :tag "Unicode string")))
+  ;; FIXME: this isn't right.
+  ;; :type '(repeat (list (string :tag "Token name")
+  ;; 		       (string :tag "Unicode string")
+  ;; 			(choice 
+  ;; 			 (const :tag "No style" nil)
+  ;; 			 (list
+  ;; 			  :inline t
+  ;; 			  ;; could generate next automatically from
+  ;; 			  ;; isar-control-regions
+  ;; 			  (const :tag "Bold" bold)
+  ;; 			  (const :tag "Italic" italic)
+  ;; 			  (const :tag "Script" script)
+  ;; 			  (const :tag "Frakt" frakt)
+  ;; 			  (const :tag "Roman" serif)))))
   :set 'proof-set-value
   :group 'isabelle
   :tag "Isabelle Unicode Token Mapping")
@@ -522,27 +535,28 @@ results will be undefined when files are saved."
     ("|}" . "\\<rbrace>")
     ("---" . "\\<emdash>")))
 
-(defcustom isar-shortcut-alist
-  (append
-   isar-symbol-shortcuts
-   ;; LaTeX-like syntax for symbol names, easier to type
-   (mapcar 
-    (lambda (tokentry)
-      (cons (concat "\\" (car tokentry))
-	    (format isar-token-format (car tokentry))))
-    (append isar-greek-letters-tokens isar-symbols-tokens)))
+;; like defcustom, but want to evaluate default
+(custom-declare-variable 'isar-shortcut-alist
+   (list 'quote (append
+      isar-symbol-shortcuts
+      ;; LaTeX-like syntax for symbol names, easier to type
+      (mapcar 
+       (lambda (tokentry)
+	 (cons (concat "\\" (car tokentry))
+	       (format isar-token-format (car tokentry))))
+       (append isar-greek-letters-tokens isar-symbols-tokens))))
   "Shortcut key sequence table for token input.
 
 You can adjust this table to add more entries, or to change entries for
 glyphs that not are available in your Emacs or chosen font.
 
-These shortcuts are only used for input; no reverse conversion is
-performed.  "
+These shortcuts are only used for input convenience; no reverse 
+conversion is performed."
   :type '(repeat (cons (string :tag "Shortcut sequence")
 		       (string :tag "Unicode string")))
   :set 'proof-set-value
   :group 'isabelle
-  :tag "Isabelle Unicode Token Mapping")
+  :tag "Isabelle Unicode Input Shortcuts")
 
   
 
diff --git a/lib/unicode-tokens.el b/lib/unicode-tokens.el
index 865f6ae8..c18a36ce 100644
--- a/lib/unicode-tokens.el
+++ b/lib/unicode-tokens.el
@@ -41,6 +41,9 @@
 
 ;;
 ;; Variables that should be set by client modes
+;; 
+;; Each variable may be set directly or indirectly; see
+;; `unicode-tokens-copy-configuration-variables' below.
 ;;
 
 (defvar unicode-tokens-token-symbol-map nil
@@ -87,7 +90,7 @@ Behaviour is much like abbrev.")
 
 
 ;;
-;; Variables that can be overridden in instances: control tokens
+;; Variables that may optionally be set in client modes
 ;;
 
 (defvar unicode-tokens-control-region-format-regexp nil
@@ -129,6 +132,43 @@ and (match-string 2) has the display control applied.")
     control-regions
     control-characters))
 
+(defun unicode-tokens-config (sym)
+  (intern (concat "unicode-tokens-" (symbol-name sym))))
+
+(defun unicode-tokens-config-var (sym)
+  (intern (concat "unicode-tokens-" (symbol-name sym) "-variable")))
+
+(dolist (sym unicode-tokens-configuration-variables)
+ (lambda (sym)
+   (eval `(defvar ,(unicode-tokens-config-var sym)
+	   nil
+	   ,(format "Name of a variable used to configure %s.\nValue should be a symbol."
+		    (symbol-name (unicode-tokens-config sym)))))))
+
+(defun unicode-tokens-copy-configuration-variables ()
+  "Initialise the configuration variables by copying from variable names.
+Each configuration variable may be set directly or indirectly by client;
+modes an indirect setting is made by this function from a variable named
+<setting>-variable, e.g., `unicode-tokens-token-symbol-map'
+will be initialised from `unicode-tokens-token-symbol-map-variable'
+if it is bound, which should be the name of a variable."
+  (dolist (sym unicode-tokens-configuration-variables)
+    (let ((var (unicode-tokens-config-var sym)))
+      (if (and (boundp var) (not (null (symbol-value var))))
+	  (set (unicode-tokens-config sym)
+	       (symbol-value (symbol-value 
+			      (unicode-tokens-config-var sym))))))))
+
+(defun unicode-tokens-customize (sym)
+  (interactive "sCustomize setting: ") ;; TODO: completing read, check if customizable
+  (customize-variable 
+   (symbol-value (unicode-tokens-config-var (intern sym)))))
+  
+
+  
+
+
+
 ;;
 ;; Variables set in the mode 
 ;;
@@ -648,6 +688,7 @@ tokenised symbols."
 
 (defun unicode-tokens-initialise ()
   (interactive)
+  (unicode-tokens-copy-configuration-variables)
   (let ((flks (unicode-tokens-font-lock-keywords)))
     (put 'unicode-tokens-font-lock-keywords major-mode flks)
     (unicode-tokens-quail-define-rules)
@@ -771,8 +812,6 @@ Commands available are:
       ["Insert token..." unicode-tokens-insert-token]
       ["Next token"      unicode-tokens-rotate-token-forward]
       ["Prev token"      unicode-tokens-rotate-token-backward]
-      ["List tokens"     unicode-tokens-list-tokens]
-      ["List shortcuts"  unicode-tokens-list-shortcuts]
        (cons "Format char"
 	     (mapcar 
  	     (lambda (fmt)
@@ -793,6 +832,12 @@ Commands available are:
   		       :active 'mark-active))
  	     unicode-tokens-control-regions))
        "---"
+      ["List tokens"     unicode-tokens-list-tokens]
+      ["List shortcuts"  unicode-tokens-list-shortcuts]
+;; typing needs fixing
+;;      ["Customize tokens"     (unicode-tokens-customize "token-symbol-map")]
+      ["Customize shortcuts"  (unicode-tokens-customize "shortcut-alist")]
+      "---"
       ["Copy as unicode" unicode-tokens-copy
        :active 'mark-active
        :help "Copy text from buffer, converting tokens to Unicode"]