x-symbol-isabelle-prepare-table: avoids redundancy in code, improves

  on isar version (only 1 backslash);

1 files changed, 153 insertions, 140 deletions

diff --git a/isa/x-symbol-isabelle.el b/isa/x-symbol-isabelle.el
index 857c9e57..1822b673 100644
--- a/isa/x-symbol-isabelle.el
+++ b/isa/x-symbol-isabelle.el
@@ -2,7 +2,7 @@
 ;;  Author:     David von Oheimb
 ;;  Copyright   1998 Technische Universitaet Muenchen
 ;;  token language "Isabelle Symbols" for package x-symbol
-;;  
+;;
 ;; NB: Part of Proof General distribution.
 ;;
 
@@ -23,7 +23,7 @@
 ;    ("Symbol" symbol currency mathletter setsymbol)
 ;    ("Greek Letter" greek greek1)
 ;    ("Acute, Grave" acute grave))
-;  "*If non-nil, used in isasym specific grid/menu.
+;  "*If non-nil, used in isasym specific grid/menu."
 
 (defvar x-symbol-isabelle-class-alist
   '((VALID "Isabelle Symbol" (x-symbol-info-face))
@@ -42,8 +42,8 @@
 ;(defvar x-symbol-isabelle-token-shape '(?\\ "\\\\\\<[A-Za-z][A-Za-z0-9_']*>\\a'" . "[A-Za-z]"))
 (defvar x-symbol-isabelle-token-shape nil)
 
-(defvar x-symbol-isabelle-exec-specs '(nil ("\\`\\\\<[A-Za-z][A-Za-z0-9_']*>\\'" . 
-				          "\\\\<[A-Za-z][A-Za-z0-9_']*>")))
+(defvar x-symbol-isabelle-exec-specs '(nil ("\\`\\\\<[A-Za-z][A-Za-z0-9_']*>\\'" .
+                                          "\\\\<[A-Za-z][A-Za-z0-9_']*>")))
 
 (defvar x-symbol-isabelle-input-token-ignore nil)
 (defun x-symbol-isabelle-default-token-list (tokens) tokens)
@@ -51,144 +51,157 @@
 
 (defvar x-symbol-isabelle-token-list 'x-symbol-isabelle-default-token-list)
 
-(defvar x-symbol-isabelle-symbol-table '(;;symbols (isabelle14 font)
-    (visiblespace () "\\\\<spacespace>" "\\<spacespace>")
-    (Gamma  () "\\\\<Gamma>" "\\<Gamma>")
-    (Delta  () "\\\\<Delta>" "\\<Delta>")
-    (Theta  () "\\\\<Theta>" "\\<Theta>")
-    (Lambda () "\\\\<Lambda>" "\\<Lambda>")
-    (Pi     () "\\\\<Pi>" "\\<Pi>")
-    (Sigma  () "\\\\<Sigma>" "\\<Sigma>")
-    (Phi    () "\\\\<Phi>" "\\<Phi>")
-    (Psi    () "\\\\<Psi>" "\\<Psi>")
-    (Omega  () "\\\\<Omega>" "\\<Omega>")
-    (alpha  () "\\\\<alpha>" "\\<alpha>")
-    (beta   () "\\\\<beta>" "\\<beta>")
-    (gamma  () "\\\\<gamma>" "\\<gamma>")
-    (delta  () "\\\\<delta>" "\\<delta>")
-    (epsilon1 () "\\\\<epsilon>" "\\<epsilon>")
-    (zeta   () "\\\\<zeta>" "\\<zeta>")
-    (eta    () "\\\\<eta>" "\\<eta>")
-    (theta1 () "\\\\<theta>" "\\<theta>")
-    (kappa1 () "\\\\<kappa>" "\\<kappa>")
-    (lambda () "\\\\<lambda>" "\\<lambda>")
-    (mu     () "\\\\<mu>" "\\<mu>")
-    (nu     () "\\\\<nu>" "\\<nu>")
-    (xi     () "\\\\<xi>" "\\<xi>")
-    (pi     () "\\\\<pi>" "\\<pi>")
-    (rho    () "\\\\<rho>" "\\<rho>")
-    (sigma  () "\\\\<sigma>" "\\<sigma>")
-    (tau    () "\\\\<tau>" "\\<tau>")
-    (phi1   () "\\\\<phi>" "\\<phi>")
-    (chi    () "\\\\<chi>" "\\<chi>")
-    (psi    () "\\\\<psi>" "\\<psi>")
-    (omega  () "\\\\<omega>" "\\<omega>")
-    (notsign       () "\\\\<not>" "\\<not>")
-    (logicaland    () "\\\\<and>" "\\<and>")
-    (logicalor     () "\\\\<or>" "\\<or>")
-    (universal1    () "\\\\<forall>" "\\<forall>")
-    (existential1  () "\\\\<exists>" "\\<exists>")
-    (biglogicaland () "\\\\<And>" "\\<And>")
-    (ceilingleft   () "\\\\<lceil>" "\\<lceil>")
-    (ceilingright  () "\\\\<rceil>" "\\<rceil>")
-    (floorleft     () "\\\\<lfloor>" "\\<lfloor>")
-    (floorright    () "\\\\<rfloor>" "\\<rfloor>")
-    (bardash       () "\\\\<turnstile>" "\\<turnstile>")
-    (bardashdbl    () "\\\\<Turnstile>" "\\<Turnstile>")
-    (semanticsleft () "\\\\<lbrakk>" "\\<lbrakk>")
-    (semanticsright () "\\\\<rbrakk>" "\\<rbrakk>")
-    (periodcentered () "\\\\<cdot>" "\\<cdot>")
-    (element      () "\\\\<in>" "\\<in>")
-    (reflexsubset () "\\\\<subseteq>" "\\<subseteq>")
-    (intersection () "\\\\<inter>" "\\<inter>")
-    (union        () "\\\\<union>" "\\<union>")
-    (bigintersection   () "\\\\<Inter>" "\\<Inter>")
-    (bigunion          () "\\\\<Union>" "\\<Union>")
-    (sqintersection    () "\\\\<sqinter>" "\\<sqinter>")
-    (squnion           () "\\\\<squnion>" "\\<squnion>")
-    (bigsqintersection () "\\\\<Sqinter>" "\\<Sqinter>")
-    (bigsqunion        () "\\\\<Squnion>" "\\<Squnion>")
-    (perpendicular     () "\\\\<bottom>" "\\<bottom>")
-    (dotequal    () "\\\\<doteq>" "\\<doteq>")
-    (equivalence () "\\\\<equiv>" "\\<equiv>")
-    (notequal    () "\\\\<noteq>" "\\<noteq>")
-    (propersqsubset () "\\\\<sqsubset>" "\\<sqsubset>")
-    (reflexsqsubset () "\\\\<sqsubseteq>" "\\<sqsubseteq>")
-    (properprec  () "\\\\<prec>" "\\<prec>")
-    (reflexprec  () "\\\\<preceq>" "\\<preceq>")
-    (propersucc  () "\\\\<succ>" "\\<succ>")
-    (approxequal () "\\\\<approx>" "\\<approx>")
-    (similar     () "\\\\<sim>" "\\<sim>")
-    (simequal    () "\\\\<simeq>" "\\<simeq>")
-    (lessequal   () "\\\\<le>" "\\<le>")
-    (coloncolon  () "\\\\<Colon>" "\\<Colon>")
-    (arrowleft   () "\\\\<leftarrow>" "\\<leftarrow>")
-    (endash      () "\\\\<midarrow>" "\\<midarrow>")
-    (arrowright  () "\\\\<rightarrow>" "\\<rightarrow>")
-    (arrowdblleft () "\\\\<Leftarrow>" "\\<Leftarrow>")
-;   (rightleftharpoons () "\\\\<Midarrow>" "\\<Midarrow>") ;missing symbol (but not necessary)
-    (arrowdblright () "\\\\<Rightarrow>" "\\<Rightarrow>")
-    (frown () "\\\\<bow>" "\\<bow>")
-    (mapsto () "\\\\<mapsto>" "\\<mapsto>")
-    (leadsto () "\\\\<leadsto>" "\\<leadsto>")
-    (arrowup () "\\\\<up>" "\\<up>")
-    (arrowdown () "\\\\<down>" "\\<down>")
-    (notelement () "\\\\<notin>" "\\<notin>")
-    (multiply () "\\\\<times>" "\\<times>")
-    (circleplus () "\\\\<oplus>" "\\<oplus>")
-    (circleminus () "\\\\<ominus>" "\\<ominus>")
-    (circlemultiply () "\\\\<otimes>" "\\<otimes>")
-    (circleslash () "\\\\<oslash>" "\\<oslash>")
-    (propersubset () "\\\\<subset>" "\\<subset>")
-    (infinity () "\\\\<infinity>" "\\<infinity>")
-    (box () "\\\\<box>" "\\<box>")
-    (lozenge1 () "\\\\<diamond>" "\\<diamond>")
-    (circ () "\\\\<circ>" "\\<circ>")
-    (bullet () "\\\\<bullet>" "\\<bullet>")
-    (bardbl () "\\\\<parallel>" "\\<parallel>")
-    (radical () "\\\\<surd>" "\\<surd>")
-    (copyright () "\\\\<copyright>" "\\<copyright>")
-  ))
-(defvar x-symbol-isabelle-xsymbol-table '(;;xsymbols
-    (plusminus () "\\\\<plusminus>" "\\<plusminus>")
-    (division () "\\\\<div>" "\\<div>")
-    (longarrowright () "\\\\<longrightarrow>" "\\<longrightarrow>")
-    (longarrowleft  () "\\\\<longleftarrow>" "\\<longleftarrow>")
-    (longarrowboth  () "\\\\<longleftrightarrow>" "\\<longleftrightarrow>")
-    (longarrowdblright () "\\\\<Longrightarrow>" "\\<Longrightarrow>")
-    (longarrowdblleft  () "\\\\<Longleftarrow>" "\\<Longleftarrow>")
-    (longarrowdblboth  () "\\\\<Longleftrightarrow>" "\\<Longleftrightarrow>")
-    (brokenbar () "\\\\<brokenbar>" "\\<brokenbar>")
-    (hyphen () "\\\\<hyphen>" "\\<hyphen>")
-    (macron () "\\\\<macron>" "\\<macron>")
-    (exclamdown () "\\\\<exclamdown>" "\\<exclamdown>")
-    (questiondown () "\\\\<questiondown>" "\\<questiondown>")
-    (guillemotleft () "\\\\<guillemotleft>" "\\<guillemotleft>")
-    (guillemotright () "\\\\<guillemotright>" "\\<guillemotright>")
-    (degree () "\\\\<degree>" "\\<degree>")
-    (onesuperior () "\\\\<onesuperior>" "\\<onesuperior>")
-    (onequarter () "\\\\<onequarter>" "\\<onequarter>")
-    (twosuperior () "\\\\<twosuperior>" "\\<twosuperior>")
-    (onehalf () "\\\\<onehalf>" "\\<onehalf>")
-    (threesuperior () "\\\\<threesuperior>" "\\<threesuperior>")
-    (threequarters () "\\\\<threequarters>" "\\<threequarters>")
-    (paragraph () "\\\\<paragraph>" "\\<paragraph>")
-    (registered () "\\\\<registered>" "\\<registered>")
-    (ordfeminine () "\\\\<ordfeminine>" "\\<ordfeminine>")
-    (ordmasculine () "\\\\<ordmasculine>" "\\<ordmasculine>")
-    (section () "\\\\<section>" "\\<section>")
-    (pounds () "\\\\<pounds>" "\\<pounds>")
-    (yen () "\\\\<yen>" "\\<yen>")
-    (cent () "\\\\<cent>" "\\<cent>")
-    (currency () "\\\\<currency>" "\\<currency>")
-    (braceleft2 () "\\\\<lbrace>" "\\<lbrace>")
-    (braceright2 () "\\\\<rbrace>" "\\<rbrace>")
-    (top () "\\\\<top>" "\\<top>")
-  ))
+(defvar x-symbol-isabelle-symbol-table      ; symbols (isabelle font)
+  '((visiblespace "\\<spacespace>")
+    (Gamma "\\<Gamma>")
+    (Delta "\\<Delta>")
+    (Theta "\\<Theta>")
+    (Lambda "\\<Lambda>")
+    (Pi "\\<Pi>")
+    (Sigma "\\<Sigma>")
+    (Phi "\\<Phi>")
+    (Psi "\\<Psi>")
+    (Omega "\\<Omega>")
+    (alpha "\\<alpha>")
+    (beta "\\<beta>")
+    (gamma "\\<gamma>")
+    (delta "\\<delta>")
+    (epsilon1 "\\<epsilon>")
+    (zeta "\\<zeta>")
+    (eta "\\<eta>")
+    (theta1 "\\<theta>")
+    (kappa1 "\\<kappa>")
+    (lambda "\\<lambda>")
+    (mu "\\<mu>")
+    (nu "\\<nu>")
+    (xi "\\<xi>")
+    (pi "\\<pi>")
+    (rho "\\<rho>")
+    (sigma "\\<sigma>")
+    (tau "\\<tau>")
+    (phi1 "\\<phi>")
+    (chi "\\<chi>")
+    (psi "\\<psi>")
+    (omega "\\<omega>")
+    (notsign "\\<not>")
+    (logicaland "\\<and>")
+    (logicalor "\\<or>")
+    (universal1 "\\<forall>")
+    (existential1 "\\<exists>")
+    (biglogicaland "\\<And>")
+    (ceilingleft "\\<lceil>")
+    (ceilingright "\\<rceil>")
+    (floorleft "\\<lfloor>")
+    (floorright "\\<rfloor>")
+    (bardash "\\<turnstile>")
+    (bardashdbl "\\<Turnstile>")
+    (semanticsleft "\\<lbrakk>")
+    (semanticsright "\\<rbrakk>")
+    (periodcentered "\\<cdot>")
+    (element "\\<in>")
+    (reflexsubset "\\<subseteq>")
+    (intersection "\\<inter>")
+    (union "\\<union>")
+    (bigintersection "\\<Inter>")
+    (bigunion "\\<Union>")
+    (sqintersection "\\<sqinter>")
+    (squnion "\\<squnion>")
+    (bigsqintersection "\\<Sqinter>")
+    (bigsqunion "\\<Squnion>")
+    (perpendicular "\\<bottom>")
+    (dotequal "\\<doteq>")
+    (equivalence "\\<equiv>")
+    (notequal "\\<noteq>")
+    (propersqsubset "\\<sqsubset>")
+    (reflexsqsubset "\\<sqsubseteq>")
+    (properprec "\\<prec>")
+    (reflexprec "\\<preceq>")
+    (propersucc "\\<succ>")
+    (approxequal "\\<approx>")
+    (similar "\\<sim>")
+    (simequal "\\<simeq>")
+    (lessequal "\\<le>")
+    (coloncolon "\\<Colon>")
+    (arrowleft "\\<leftarrow>")
+    (endash "\\<midarrow>")
+    (arrowright "\\<rightarrow>")
+    (arrowdblleft "\\<Leftarrow>")
+;   (rightleftharpoons "\\<Midarrow>") ;missing symbol (but not necessary)
+    (arrowdblright "\\<Rightarrow>")
+    (frown "\\<bow>")
+    (mapsto "\\<mapsto>")
+    (leadsto "\\<leadsto>")
+    (arrowup "\\<up>")
+    (arrowdown "\\<down>")
+    (notelement "\\<notin>")
+    (multiply "\\<times>")
+    (circleplus "\\<oplus>")
+    (circleminus "\\<ominus>")
+    (circlemultiply "\\<otimes>")
+    (circleslash "\\<oslash>")
+    (propersubset "\\<subset>")
+    (infinity "\\<infinity>")
+    (box "\\<box>")
+    (lozenge1 "\\<diamond>")
+    (circ "\\<circ>")
+    (bullet "\\<bullet>")
+    (bardbl "\\<parallel>")
+    (radical "\\<surd>")
+    (copyright "\\<copyright>")))
+
+(defvar x-symbol-isabelle-xsymbol-table    ; xsymbols
+  '((plusminus "\\<plusminus>")
+    (division "\\<div>")
+    (longarrowright "\\<longrightarrow>")
+    (longarrowleft "\\<longleftarrow>")
+    (longarrowboth "\\<longleftrightarrow>")
+    (longarrowdblright "\\<Longrightarrow>")
+    (longarrowdblleft "\\<Longleftarrow>")
+    (longarrowdblboth "\\<Longleftrightarrow>")
+    (brokenbar "\\<brokenbar>")
+    (hyphen "\\<hyphen>")
+    (macron "\\<macron>")
+    (exclamdown "\\<exclamdown>")
+    (questiondown "\\<questiondown>")
+    (guillemotleft "\\<guillemotleft>")
+    (guillemotright "\\<guillemotright>")
+    (degree "\\<degree>")
+    (onesuperior "\\<onesuperior>")
+    (onequarter "\\<onequarter>")
+    (twosuperior "\\<twosuperior>")
+    (onehalf "\\<onehalf>")
+    (threesuperior "\\<threesuperior>")
+    (threequarters "\\<threequarters>")
+    (paragraph "\\<paragraph>")
+    (registered "\\<registered>")
+    (ordfeminine "\\<ordfeminine>")
+    (ordmasculine "\\<ordmasculine>")
+    (section "\\<section>")
+    (pounds "\\<pounds>")
+    (yen "\\<yen>")
+    (cent "\\<cent>")
+    (currency "\\<currency>")
+    (braceleft2 "\\<lbrace>")
+    (braceright2 "\\<rbrace>")
+    (top "\\<top>")))
+
 (defvar x-symbol-isabelle-user-table nil)
+
+(defun x-symbol-isabelle-prepare-table (table)
+  (let*
+      ((is-isar (eq proof-assistant-symbol 'isar))
+       (prfx1 (if is-isar "" "\\"))
+       (prfx2 (if is-isar "\\" "")))
+    (mapcar (lambda (entry)
+              (list (car entry) '() (concat prfx1 (cadr entry)) (concat prfx2 (cadr entry))))
+            table)))
+
 (defvar x-symbol-isabelle-table
-  (append x-symbol-isabelle-user-table 
-	  (append x-symbol-isabelle-symbol-table x-symbol-isabelle-xsymbol-table)))
+  (x-symbol-isabelle-prepare-table
+   (append
+    x-symbol-isabelle-user-table
+    x-symbol-isabelle-symbol-table
+    x-symbol-isabelle-xsymbol-table)))
 
 ;;;===========================================================================
 ;;;  Internal