Fixed coq x-symbols. now alphaa is not encoded, aalpha is not encoded,

but alpha_, _alpha and _alpha_ are decoded.

2 files changed, 110 insertions, 78 deletions

diff --git a/coq/x-symbol-coq.el b/coq/x-symbol-coq.el
index 13ebe052..bcd464cd 100644
--- a/coq/x-symbol-coq.el
+++ b/coq/x-symbol-coq.el
@@ -13,6 +13,16 @@
 
 ; ?? (defvar x-symbol-coq-required-fonts nil)
 
+
+;; CW: this sexpr can be deleted with X-Symbol 4.4.3
+(eval-when-compile
+  ;; Next lines should allow this file to work standalone 
+  ;; without proof-x-symbol.el.  See comments further below too.
+  (require 'cl)
+  (ignore-errors (require 'x-symbol-vars)))
+
+(defvar x-symbol-coq-required-fonts nil)
+  
 ;;;===========================================================================
 ;;;  General language accesses, see `x-symbol-language-access-alist'
 ;;;===========================================================================
@@ -25,20 +35,19 @@
 (defvar x-symbol-coq-modeline-name "coq")
 
 (defcustom x-symbol-coq-header-groups-alist nil
-   "*If non-nil, used in coqsym specific grid/menu.
+   "*If non-nil, used in isasym specific grid/menu.
 See `x-symbol-header-groups-alist'."
   :group 'x-symbol-coq
   :group 'x-symbol-input-init
   :type 'x-symbol-headers)
 
-(defcustom x-symbol-coq-electric-ignore 
-  nil
+(defcustom x-symbol-coq-electric-ignore nil
+;;  "[:'][A-Za-z]\\|<=\\|\\[\\[\\|\\]\\]\\|~="
   "*Additional Coq version of `x-symbol-electric-ignore'."
   :group 'x-symbol-coq
   :group 'x-symbol-input-control
   :type 'x-symbol-function-or-regexp)
 
-
 (defvar x-symbol-coq-required-fonts nil
   "List of features providing fonts for language `coq'.")
 
@@ -46,24 +55,23 @@ See `x-symbol-header-groups-alist'."
   "Extra menu entries for language `coq'.")
 
 
-;;three following are from x-symbol-phox.el
 (defvar x-symbol-coq-token-grammar
   ;; CW: for X-Symbol-4.4.3:
   ;; '(x-symbol-make-grammar ...)
   (if (fboundp 'x-symbol-make-grammar) ;; x-symbol >=4.3 versions
       (x-symbol-make-grammar
-       :encode-spec '(((id . "['a-zA-Z0-9]") (op . "[]><=\\/~&+-+-*%!{}:|]")) .
-                    ((id . "['a-zA-Z0-9]") (op . "[]><=\\/~&+-+-*%!{}:|]")))
+       :encode-spec '(((id . "['a-zA-Z0-9]") (op . "[]><=\\/~&+-*%!{}:-]")) .
+                    ((id . "['a-zA-Z0-9]") (op . "[]><=\\/~&+-*%!{}:-]")))
        :decode-spec nil
-       :decode-regexp "\\(['a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:|-]+\\)"
-       :token-list #'x-symbol-coq-default-token-list
-		 :input-spec nil)))
+		 ;; decode-spec seems to go with highlighting encoding??
+       :decode-regexp "\\(['a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:-]+\\)"
+       :token-list #'x-symbol-coq-default-token-list)))
 
-(defvar x-symbol-coq-input-token-grammar
-  '("\\([_'a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*-%!{}:|]+\\)"
-     ((id . "[A-Za-z_0-9]") (op . "[-<>!+*/|&]"))
-     (id . "[A-Za-z_0-9]") (op . "[-<>!+*/|&]"))
-  "Grammar of input method Token for language `coq'.")
+;(defvar x-symbol-coq-input-token-grammar
+;  '("\\([_'a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:-]+\\)"
+;     ((id . "[A-Za-z_0-9]") (op . "[<>!+-*/|&]"))
+;     (id . "[A-Za-z_0-9]") (op . "[<>!+-*/|&]"))
+;  "Grammar of input method Token for language `coq'.")
 
 (defun x-symbol-coq-default-token-list (tokens)
   (mapcar 
@@ -73,21 +81,10 @@ See `x-symbol-header-groups-alist'."
 	    ;; CW: where are the shapes `id' and `op' used?
 	    ((string-match "\\`[A-Za-z_][A-Za-z_0-9]+\\'" x)
 	     'id)
-	    ((string-match "\\`[-<>!+*/|&]+\\'" x) 
+	    ((string-match "\\`[<>!+-*/|&]+\\'" x) 
 	     'op))))
    tokens))
 
-
-;(defvar x-symbol-coq-token-grammar
-;  '(x-symbol-make-grammar
-;    :encode-spec (((t . "\\\\")))
-;    :decode-regexp "\\\\[A-Za-z]+"
-;    :input-spec nil
-;    :token-list x-symbol-coq-token-list))
-
-;(defun x-symbol-coq-token-list (tokens)
-;  (mapcar (lambda (x) (cons x t)) tokens))
-
 (defvar x-symbol-coq-user-table nil
   "User table defining Coq commands, used in `x-symbol-coq-table'.")
 
@@ -182,7 +179,6 @@ or subscript tag."
 ;(defvar x-symbol-coq-font-lock-keywords nil)
 
 (defvar x-symbol-coq-font-lock-allowed-faces t)
-
 ;;;===========================================================================
 ;;;  Charsym Info
 ;;;===========================================================================
@@ -194,7 +190,7 @@ or subscript tag."
 See `x-symbol-language-access-alist' for details."
   :group 'x-symbol-texi
   :group 'x-symbol-info-strings
-;;  :set 'x-symbol-set-cache-variable   [causes compile error]
+  :set 'x-symbol-set-cache-variable
   :type 'x-symbol-class-info)
 
 
@@ -204,10 +200,13 @@ See `x-symbol-language-access-alist' for details."
   :group 'x-symbol-coq
   :group 'x-symbol-input-init
   :group 'x-symbol-info-general
-;;  :set 'x-symbol-set-cache-variable   [causes compile error]
+  :set 'x-symbol-set-cache-variable
   :type 'x-symbol-class-faces)
 
 
+(defvar x-symbol-coq-font-lock-keywords nil)
+
+(defvar x-symbol-coq-font-lock-allowed-faces t)
 
 ;;;===========================================================================
 ;;;  The tables
@@ -262,7 +261,7 @@ See `x-symbol-language-access-alist' for details."
     (floorleft "lfloor")
     (floorright "rfloor")
     (bardash "|-")
-    (bardashdbl "Turnstile")
+    (bardashdbl "|=")
     (semanticsleft "lbrakk")
     (semanticsright "rbrakk")
     (periodcentered "cdot")
@@ -335,7 +334,7 @@ See `x-symbol-language-access-alist' for details."
     (longarrowdblright "Longrightarrow")
     (longarrowdblleft "Longleftarrow")
     (longarrowdblboth "Longleftrightarrow")
-    (brokenbar "bar")
+;    (brokenbar "bar")
     (hyphen "hyphen")
     (macron "inverse")
     (exclamdown "exclamdown")
@@ -447,40 +446,34 @@ See `x-symbol-language-access-alist' for details."
     (bigcirclemultiply "Otimes")
     (bigcircleplus "Oplus")
     (coproduct "Coprod")
-    (cedilla "cedilla")
-    (diaeresis "dieresis")
-    (acute "acute")
+;    (cedilla "cedilla")
+;    (diaeresis "dieresis")
+;    (acute "acute")
     (hungarumlaut "hungarumlaut")
     (lozenge "lozenge")
 ;    (smllozenge "struct") ;coq keyword
     (dotlessi "index")
     (euro "euro")
-    (zero1 "zero")
-    (one1 "one")
-    (two1 "two")
-    (three1 "three")
-    (four1 "four")
-    (five1 "five")
-    (six1 "six")
-    (seven1 "seven")
-    (eight1 "eight")
-    (nine1 "nine")
+;    (zero1 "zero")
+;    (one1 "one")
+;    (two1 "two")
+;    (three1 "three")
+;    (four1 "four")
+;    (five1 "five")
+;    (six1 "six")
+;    (seven1 "seven")
+;    (eight1 "eight")
+;    (nine1 "nine")
     ))
 
 
+
 (defun x-symbol-coq-prepare-table (table)
   "Builds the x-symbol coq table from `x-symbol-coq-user-table', ` x-symbol-coq-symbol-table' and `x-symbol-coq-xsymbol-table'."
-  (let*
-      ((is-isar t) ;; simplified from isabelle, is_isar is bad name...
-       (prfx1 (if is-isar "" "\\"))
-       ;(prfx2 (if is-isar "\\" ""))
-		 )
     (mapcar (lambda (entry)
               (list (car entry) nil
-		    (concat prfx1 (cadr entry)) 
-		    ;;(concat prfx1 (cadr entry))
-			 ))
-            table)))
+		    (cadr entry)))
+            table))
 
 (defvar x-symbol-coq-table
   (x-symbol-coq-prepare-table
@@ -491,11 +484,31 @@ See `x-symbol-language-access-alist' for details."
 
 
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; User-level settings for X-Symbol 
-;;
-;; this is MODE-ON CODING 8BITS UNIQUE SUBSCRIPTS IMAGE
+(provide 'x-symbol-coq)
+
+;;;===========================================================================
+;;;  Internal
+;;;===========================================================================
+;; CW: all are not needed in X-Symbol >= v4.3
+
+(defvar x-symbol-coq-menu-alist nil
+  "Internal.  Alist used for Isasym specific menu.")
+(defvar x-symbol-coq-grid-alist nil
+  "Internal.  Alist used for Isasym specific grid.")
+
+(defvar x-symbol-coq-decode-atree nil
+  "Internal.  Atree used by `x-symbol-token-input'.")
+(defvar x-symbol-coq-decode-alist nil
+  "Internal.  Alist used for decoding of Isasym macros.")
+(defvar x-symbol-coq-encode-alist nil
+  "Internal.  Alist used for encoding to Isasym macros.")
+
+;; FIXME: next two not needed for newer X-Symbol versions.
+(defvar x-symbol-coq-nomule-decode-exec nil
+  "Internal.  File name of Isasym decode executable.")
+(defvar x-symbol-coq-nomule-encode-exec nil
+  "Internal.  File name of Isasym encode executable.")
+
 (defcustom x-symbol-coq-auto-style
   '((proof-ass x-symbol-enable)	 ; MODE-ON: whether to turn on interactively
     nil   ;; x-symbol-coding
@@ -509,23 +522,5 @@ See documentation of `x-symbol-auto-style'."
   :group 'x-symbol-mode
   :type 'x-symbol-auto-style)
 
-;; FIXME da: is this needed?
-(defcustom x-symbol-coq-auto-coding-alist nil
-  "*Alist used to determine the file coding of COQ buffers.
-Used in the default value of `x-symbol-auto-mode-alist'.  See
-variable `x-symbol-auto-coding-alist' for details."
-  :group 'x-symbol-coq
-  :group 'x-symbol-mode
-  :type 'x-symbol-auto-coding)
-
-
-     
-;; from x-symbol-isa.el
-
-;(setq proof-xsym-extra-modes '(coq-mode)
-;      proof-xsym-activate-command
-;      "print_mode := ([\"xsymbols\", \"symbols\"] @ ! print_mode);"
-;      proof-xsym-deactivate-command
-;      "print_mode := (! print_mode \\\\ [\"xsymbols\", \"symbols\"]);")
-
 (provide 'x-symbol-coq)
+
diff --git a/coq/xsymbtest.coq b/coq/xsymbtest.coq
new file mode 100644
index 00000000..c3bee71e
--- /dev/null
+++ b/coq/xsymbtest.coq
@@ -0,0 +1,37 @@
+(* Grammar for symbols:
+  a symbol is encoded only if 
+   - preceded by _ or some space or some symbol
+  **and**
+   - followed by _ or some space or some symbol
+
+  Grammar for sub/superscript: 
+
+   - a double _ introduces a subscript that ends at the first space
+   - a double ^ introduces a superscript that ends at the first space
+  
+   - a _ followed by { introduces a subscript
+     expression that ends at the first }
+   - a ^ followed by { introduces a superscript
+     expression that ends at the first }
+ *)
+
+
+
+foo_alpha_1_beta_3  (* this should appear like foo_a_1_B_3 where a and B are greek *)
+delta__1 delta^^1          (* greek delta with a sub 1 and the same with super 1 *)
+x_{a+b} x^{a+b}         (* x with a+b subscripted and then superscripted *)
+philosophi   (* no greek letter should appear on this line *)
+aalpha alphaa (* no greek letter *)
+_alpha           (* _a where a is greek *)
+alpha_           (* a_ where a is greek *)
+
+
+
+Fixpoint toto (x:nat) {struct x} : nat := (* nat should appear as |N *)
+  match x with
+    | O => O        (* double arrow here *)
+    | S y => toto y (* double arrow here *)
+  end.
+
+Lemma titi : forall x:nat,x=x. (* symbolique for-all and nat *)
+ 
\ No newline at end of file