Revert to old isar-ids-to-regexp

1 files changed, 19 insertions, 13 deletions

diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el
index 849cb243..57054a57 100644
--- a/isar/isar-syntax.el
+++ b/isar/isar-syntax.el
@@ -139,27 +139,33 @@
 
 ;; tuned version of proof-ids-to-regexp --- admit single non-word char
 ;; as well (e.g. { })
-;; FIXME FIXME FIXME
+
 ;; DA: this goes wrong for { and } in fact, because plain { and } in
 ;; `proof-script-command-start-regexp' also match with {* and *}, which 
 ;; should not be considered as commands (breaks new parser).
+;; For now, we revert to old parser and old form of this function.
 
 (defun isar-ids-to-regexp (l)
   "Maps a non-empty list of tokens `l' to a regexp matching any element"
   (mapconcat
-   (lambda (s) (if (proof-string-match "^\\W$" s) 
-		   ;; was just s 
-		   (cond 
-		    ;; FIXME: what we really want here is to match { or }
-		    ;; _except_ when followed/preceded by *, but not to
-		    ;; consider * as part of match.  (Exclude punctuation??)
-		    ;; That kind of construct is only allowed for whitespace,
-		    ;; though.
-		    ((string-equal s "{")  "{[^\*]")
-		    ((string-equal s "}")  "[^\*]}") ;; FIXME wrong
-		    (t			   s)) ; what else?
-		   (concat "\\<" s "\\>")))
+   (lambda (s) (if (proof-string-match "^\\W$" s) s (concat "\\<" s "\\>")))
    l "\\|"))
+;;
+;; Alternative version with attempt to work for new parser (unfinished) 
+;  (mapconcat
+;   (lambda (s) (if (proof-string-match "^\\W$" s) 
+;		   ;; was just s 
+;		   (cond 
+;		    ;; FIXME: what we really want here is to match { or }
+;		    ;; _except_ when followed/preceded by *, but not to
+;		    ;; consider * as part of match.  (Exclude punctuation??)
+;		    ;; That kind of construct is only allowed for whitespace,
+;		    ;; though.
+;		    ((string-equal s "{")  "{[^\*]")
+;		    ((string-equal s "}")  "[^\*]}") ;; FIXME wrong
+;		    (t			   s)) ; what else?
+;		   (concat "\\<" s "\\>")))
+;   l "\\|"))
 
 (defconst isar-long-id-stuff "\\([A-Za-z0-9'_.]+\\)")