diff options
| author | David Aspinall | 1999-02-01 13:31:51 +0000 |
|---|---|---|
| committer | David Aspinall | 1999-02-01 13:31:51 +0000 |
| commit | 46d036e905134f5c49380834b28bb1f2a6301d3c (patch) | |
| tree | 962b3c7740926336564433537820caf8951632d3 /generic/proof-script.el | |
| parent | bac4f6fbe0f94b47fea79169c849ee17601eb67c (diff) | |
Used proof-string-match for matching against proof script.
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 4e6cb042..862c92bf 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -105,7 +105,7 @@ proof-script-next-entity-regexps, which see." (p (point)) disc res) (while (and (not res) (setq disc (car-safe discriminators))) - (if (string-match (car disc) entity) + (if (proof-string-match (car disc) entity) (let ((name (substring entity (match-beginning (nth 1 disc)) @@ -662,12 +662,12 @@ the ACS is marked in the current buffer. If CMD does not match any, ((eq (span-property span 'type) 'comment) (set-span-property span 'mouse-face 'highlight)) ((proof-check-atomic-sequents-lists span cmd end)) - ((string-match proof-save-command-regexp cmd) + ((proof-string-match proof-save-command-regexp cmd) ;; In coq, we have the invariant that if we've done a save and ;; there's a top-level declaration then it must be the ;; associated goal. (Notice that because it's a callback it ;; must have been approved by the theorem prover.) - (if (string-match proof-save-with-hole-regexp cmd) + (if (proof-string-match proof-save-with-hole-regexp cmd) (setq nam (match-string 2 cmd))) (setq gspan span) (while (or (eq (span-property gspan 'type) 'comment) @@ -678,7 +678,7 @@ the ACS is marked in the current buffer. If CMD does not match any, (setq gspan next)) (if (null nam) - (if (string-match proof-goal-with-hole-regexp + (if (proof-string-match proof-goal-with-hole-regexp (span-property gspan 'cmd)) (setq nam (match-string 2 (span-property gspan 'cmd))) ;; This only works for Coq, but LEGO raises an error if @@ -1778,6 +1778,9 @@ finish setup which depends on specific proof assistant configuration." (and (boundp 'font-lock-always-fontify-immediately) (setq font-lock-always-fontify-immediately t)) + ;; Assume font-lock case folding follows proof-case-fold-search + (setq font-lock-keywords-case-fold-search proof-case-fold-search) + ;; Make sure func menu is configured. (NB: Ideal place for this and ;; similar stuff would be in something evaluated at top level after ;; defining the derived mode: normally we wouldn't repeat this |