diff options
| author | Makarius Wenzel | 2000-06-03 22:17:20 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 2000-06-03 22:17:20 +0000 |
| commit | 23d43d7e9335003b2f362b6ac223b419f6714382 (patch) | |
| tree | 27b1f83b41897877571a6ef40c76933a1a9cafe4 /generic/proof-script.el | |
| parent | 70f99119285a02089b32c54c758e2d8a59680a71 (diff) | |
improved proof-segment-up-to-cmdstart: handle overlap of command
prefix and comment/string (e.g. { vs {* in Isar);
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 0b133f65..f7dabe60 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1145,7 +1145,7 @@ This version is used when `proof-script-command-start-regexp' is set." (type (if (eq (string-match commentre bufstr) 0) 'comment 'cmd)) (string (if (eq type 'comment) "" bufstr))) - (skip-chars-forward " \t\n") +; (skip-chars-forward " \t\n") ; FIXME markus: just don't do this (setq prev (point)) (goto-char tmp) ;; NB: Command string excludes whitespace, span includes it. @@ -1160,11 +1160,16 @@ This version is used when `proof-script-command-start-regexp' is set." (re-search-forward proof-script-command-start-regexp nil t) ; search for next command (setq comstart (match-beginning 0)); save command start - (or (buffer-syntactic-context) ; continue if inside comment/string + (or (save-excursion + (goto-char comstart) + (or ; continue if inside (or at start of) comment/string + (buffer-syntactic-context) + (looking-at proof-comment-start-regexp) + (looking-at proof-string-start-regexp))) (progn ; or, if found command... (setq cmdfnd (> comstart startpos)); ignore first match - (<= prev pos)))) + (<= prev pos)))) (if cmdfnd (progn (funcall add-segment-for-cmd) (setq cmdfnd nil)))) |