diff options
| author | Gerwin Klein | 2004-04-14 01:41:38 +0000 |
|---|---|---|
| committer | Gerwin Klein | 2004-04-14 01:41:38 +0000 |
| commit | 7b2adf1cc7384c096709f51c89eb9a519b38dab1 (patch) | |
| tree | 278b1a2accb7a34e4c9d830c970414c92616a06d | |
| parent | 0075ce86d00708e724255319e12f299ce05b2231 (diff) | |
fixed regexp problem with function menu
| -rw-r--r-- | isar/isar-syntax.el | 12 | ||||
| -rw-r--r-- | isar/isar.el | 2 |
2 files changed, 8 insertions, 6 deletions
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index fe50401b..46224f09 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -195,7 +195,7 @@ (defconst isar-ext-rest "\\(?:\\\\<\\^?[A-Za-z]+>\\|[A-Za-z0-9'_]\\)") (defconst isar-long-id-stuff (concat "\\(?:" isar-ext-rest "\\|\.\\)+")) -(defconst isar-id (concat "\\(?:" isar-ext-first isar-ext-rest "*\\)")) +(defconst isar-id (concat "\\(" isar-ext-first isar-ext-rest "*\\)")) (defconst isar-idx (concat isar-id "\\(?:\\.[0-9]+\\)?")) (defconst isar-string "\"\\(?:\\(?:[^\"]\\|\\\\\"\\)*\\)\"") @@ -407,18 +407,20 @@ (defconst isar-any-entity-regexp (concat "\\(?:" (isar-ids-to-regexp isar-keywords-fume) "\\)" + "\\(?:\\s-*(\\s-*in.+)\\)?" "\\(?:" isar-name-regexp "[[:=]\\)?")) (defconst isar-named-entity-regexp - (concat "\\(?:" (isar-ids-to-regexp isar-keywords-fume) "\\)" - isar-name-regexp "[[:=]")) + (concat "\\(" (isar-ids-to-regexp isar-keywords-fume) "\\)" + "\\(\\s-*(\\s-*in.+)\\)?" + isar-name-regexp "[[:=]" )) (defconst isar-unnamed-entity-regexp - (concat "\\(?:" (isar-ids-to-regexp isar-keywords-fume) "\\)")) + (concat "\\(" (isar-ids-to-regexp isar-keywords-fume) "\\)")) (defconst isar-next-entity-regexps (list isar-any-entity-regexp - (list isar-named-entity-regexp '(1 2)) + (list isar-named-entity-regexp '(1 3)) (list isar-unnamed-entity-regexp 1))) diff --git a/isar/isar.el b/isar/isar.el index 5793fc78..58e0fa7a 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -140,7 +140,7 @@ See -k option for Isabelle interface script." proof-save-command-regexp isar-save-command-regexp proof-goal-command-regexp isar-goal-command-regexp proof-goal-with-hole-regexp isar-named-entity-regexp ; da - proof-goal-with-hole-result 1 + proof-goal-with-hole-result 3 proof-save-with-hole-regexp nil proof-script-next-entity-regexps isar-next-entity-regexps |