Source of parsing problem discovered and explained.

1 files changed, 16 insertions, 1 deletions

diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el
index 5102bf0f..849cb243 100644
--- a/isar/isar-syntax.el
+++ b/isar/isar-syntax.el
@@ -139,11 +139,26 @@
 
 ;; 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).
 
 (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) s (concat "\\<" s "\\>")))
+   (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'_.]+\\)")