diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-12-01 09:59:17 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-12-01 09:59:17 +0000 |
| commit | 1bea93ee1ac9157ecd3e8ff9a0b54c71b03590bb (patch) | |
| tree | 661a09549aebe86d708598864217c1506cb9a1f3 /isar/isar-syntax.el | |
| parent | b768c1a36e66bc1124bf100bc58ec006fb77ea7e (diff) | |
isar-ids-to-regexp: regexp-opt with 'words arg (non-shy matching inside
\< \>) appears to work on Emacs 22, hopefully repairing
http://proofgeneral.inf.ed.ac.uk/trac/ticket/300.
Also replace proof-splice-separator -> mapconcat builtin.
Diffstat (limited to 'isar/isar-syntax.el')
| -rw-r--r-- | isar/isar-syntax.el | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index 5b45eb89..588af049 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -169,17 +169,17 @@ This list is in the right format for proof-easy-config.") (defun isar-ids-to-regexp (ids) "Hack list IDS of keywords IDS to make a regexp matching any of them. Note: IDS may have full-stops already regexp quoted." ; a nuisance! - (let* ((has-lbrace (member "{" ids)) - (has-rbrace (member "}" ids)) - (cleaned (remove "{" - (mapcar (lambda (s) - (replace-regexp-in-string (regexp-quote "\\.") "." s)) - ids)))) - (proof-splice-separator "\\|" - (list (if cleaned (concat "\\<" (regexp-opt cleaned) "\\>")) - (if has-rbrace "}") ; not a word constituent, so \_<}\_> fails - (if has-lbrace "\\(?:{\\(?:\\b\\|[^\\*]\\)\\)") ; ditto, & prevent {* matching - )))) + (let* ((unquoted (mapcar (lambda (s) + (replace-regexp-in-string (regexp-quote "\\.") "." s)) + ids)) + (cleaned (remove "{" (remove "}" unquoted))) + (words (if cleaned (list (regexp-opt cleaned 'words)))) + ;; } is not a word constituent, so \_<}\_> fails + (rbrace (if (member "}" ids) '("}"))) + ;; { similarly, must also prevent {* matching + (lbrace (if (member "{" ids) + '("\\(?:{\\(?:\\b\\|[^\\*]\\)\\)")))) + (mapconcat 'identity (append words lbrace rbrace) "\\|"))) ;; tests ; (isar-ids-to-regexp '("bla" "blubber")) @@ -193,9 +193,9 @@ Note: IDS may have full-stops already regexp quoted." ; a nuisance! ; (string-match (isar-ids-to-regexp '("bla" "}" "blubber" "{")) "ug{") ; 2 ; (string-match (isar-ids-to-regexp '("bla" "}" "blubber" "{")) "}ug") ; 0 ; (string-match (isar-ids-to-regexp '("bla" "}" "blubber" "{")) "}\n ug") ; 0 -; (string-match (isar-ids-to-regexp '("foo" "\\." "Foo\\.bar")) "boo.foo") ; nil +; (string-match (isar-ids-to-regexp '("foo" "\\." "Foo\\.bar")) "boo.foo") ; nil/4 ; (string-match (isar-ids-to-regexp '("foo" "\\." "Foo\\.bar")) "Foo.bar") ; 0 -; (string-match (isar-ids-to-regexp '("foo" "\\." "Foo\\.bar")) "bar . foo") ; 4 +; (string-match (isar-ids-to-regexp '("foo" "\\." "Foo\\.bar")) "bar.foo") ; 4 ; (string-match (isar-ids-to-regexp '("foo" "\\." "Foo\\.bar")) "bar. foo") ; 5 (defconst isar-any-command-regexp |