diff options
| -rw-r--r-- | isa/isabelle-system.el | 4 | ||||
| -rw-r--r-- | isar/isar-syntax.el | 2 | ||||
| -rw-r--r-- | isar/isar.el | 8 |
3 files changed, 7 insertions, 7 deletions
diff --git a/isa/isabelle-system.el b/isa/isabelle-system.el index d3cc2596..2d90192c 100644 --- a/isa/isabelle-system.el +++ b/isa/isabelle-system.el @@ -185,7 +185,7 @@ passed to isa-tool-doc-command, DOCNAME will be viewed." (function (lambda (docdes) (list (substring docdes - (string-match "\\(\\S-+\\)[ \t]+" docdes) + (proof-string-match "\\(\\S-+\\)[ \t]+" docdes) (match-end 1)) (substring docdes (match-end 0))))) (split-string docs "\n")))))) @@ -207,7 +207,7 @@ Called with one argument: t to save database, nil otherwise." ;;; Set proof-shell-pre-interrupt-hook for PolyML 3. (if (and (not proof-shell-pre-interrupt-hook) - (string-match "\\`polyml-3" (isa-getenv "ML_SYSTEM"))) + (proof-string-match "\\`polyml-3" (isa-getenv "ML_SYSTEM"))) (add-hook 'proof-shell-pre-interrupt-hook (lambda () (proof-shell-insert (isabelle-verbatim "f") nil)))) diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index 89e78b87..d79ca239 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -125,7 +125,7 @@ (defun isar-ids-to-regexp (l) "Maps a non-empty list of tokens `l' to a regexp matching any element" (mapconcat - (lambda (s) (if (string-match "^\\W$" s) s (concat "\\<" s "\\>"))) + (lambda (s) (if (proof-string-match "^\\W$" s) s (concat "\\<" s "\\>"))) l "\\|")) (defconst isar-long-id-stuff "\\([A-Za-z0-9'_.]+\\)") diff --git a/isar/isar.el b/isar/isar.el index a1356705..b76d15b4 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -404,7 +404,7 @@ proof-shell-retract-files-regexp." (defun isar-global-save-command-p (span str) "Decide whether argument really is a global save command" (or - (string-match isar-global-save-command-regexp str) + (proof-string-match isar-global-save-command-regexp str) (let ((ans nil) (lev 0) cmd) (while (and (not ans) span (setq span (prev-span span 'type))) (setq cmd (span-property span 'cmd)) @@ -474,9 +474,9 @@ proof-shell-retract-files-regexp." (defun isar-preprocessing () ;dynamic scoping of `string' "Insert sync markers - acts on variable STRING by dynamic scoping" - (if (string-match isabelle-verbatim-regexp string) + (if (proof-string-match isabelle-verbatim-regexp string) (setq string (match-string 1 string)) - (unless (string-match ";[ \t]*\\'" string) + (unless (proof-string-match ";[ \t]*\\'" string) (setq string (concat string ";"))) (setq string (concat "\\<^sync>" @@ -489,7 +489,7 @@ proof-shell-retract-files-regexp." ;; comment end in proof-script.el's function ;; proof-segment-upto-cmdstart (which becomes even more ;; Isar specific, then...) - ;; (if (string-match "\\.ML$" (buffer-name proof-script-buffer)) + ;; (if (proof-string-match "\\.ML$" (buffer-name proof-script-buffer)) ;; (format "ML_command {* %s *};" string) ;; string) string |