diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2004-04-16 12:30:42 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2004-04-16 12:30:42 +0000 |
| commit | a40c4b07059f754e63fa29787148cdab22359cb6 (patch) | |
| tree | e55100008e2a9615910648cede16436d21e36f7c | |
| parent | 665fcf2a7667f428ca0be6fc31ba14117ab11c68 (diff) | |
little fix for x-symbols coq.
| -rw-r--r-- | CHANGES | 13 | ||||
| -rw-r--r-- | coq/example-x-symbols.v | 2 | ||||
| -rw-r--r-- | coq/x-symbol-coq.el | 6 |
3 files changed, 11 insertions, 10 deletions
@@ -259,12 +259,13 @@ will be asked if you want to save abbrevs, answer yes. *** X-symbols are much improved (more symbols, cleaner grammar) -Symbols are encoded only if between spaces or _'s. Sub/superscripts -are now introduced by '__' and '^^' respectively, and the rest of the -word is sub/superscripted. To put spaces inside sub/superscripts, use -_{...} or ^{...}. Notice that this last syntax is not understood by -Coq and you will need to defined it with the "Notation" command of -Coq. +Much more symbols are supported now (C-= C-= for the symbol table). +Symbols are encoded only if between spaces, ' or _. Sub/superscripts +are now introduced by '__' and '^^' respectively, and then the word is +sub/superscripted until its end. To put spaces or symbols inside +sub/superscripts, use _{...} or ^{...}. Notice that this last syntax +and the ^^ symbol are not understood by Coq and you will need to +defined it with the "Notation" command of Coq. ** Additional instances of Proof General diff --git a/coq/example-x-symbols.v b/coq/example-x-symbols.v index c3bee71e..21d94b93 100644 --- a/coq/example-x-symbols.v +++ b/coq/example-x-symbols.v @@ -17,7 +17,7 @@ -foo_alpha_1_beta_3 (* this should appear like foo_a_1_B_3 where a and B are greek *) +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 *) diff --git a/coq/x-symbol-coq.el b/coq/x-symbol-coq.el index d37d859a..a800e8bd 100644 --- a/coq/x-symbol-coq.el +++ b/coq/x-symbol-coq.el @@ -47,11 +47,11 @@ See `x-symbol-header-groups-alist'." (defvar x-symbol-coq-token-grammar (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-spec seems to go with highlighting encoding?? - :decode-regexp "\\(['a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:-]+\\)" + :decode-regexp "\\([a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:-]+\\)" :token-list #'x-symbol-coq-default-token-list)) ;(defvar x-symbol-coq-input-token-grammar |