diff options
| author | David Aspinall | 2009-09-15 07:47:15 +0000 |
|---|---|---|
| committer | David Aspinall | 2009-09-15 07:47:15 +0000 |
| commit | 682b4c17840aaa694cf3c7684bb5b06bcb4108c2 (patch) | |
| tree | 4eced173d60c3a2c2d81d7c2850364a2d8d06332 /isar/isar.el | |
| parent | b8bdbab2356aa0e68164143d3f78c73ad12197c7 (diff) | |
Fix compile errors
Diffstat (limited to 'isar/isar.el')
| -rw-r--r-- | isar/isar.el | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/isar/isar.el b/isar/isar.el index 0455ec6d..719d7ce7 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -593,15 +593,16 @@ This slows down interactive processing slightly." (defun isar-preprocessing () "Insert sync markers and other hacks. Uses variables `string' and `scriptspan' passed by dynamic scoping." - (if (proof-string-match isabelle-verbatim-regexp string) - (setq string (match-string 1 string)) - (unless (string-match ";[ \t]*\\'" string) - (setq string (concat string ";"))) - (setq string (concat - "\\<^sync>; " - (isar-shell-adjust-line-width) - string - " \\<^sync>;")))) + (with-no-warnings ; dynamic scoping of string, scriptspan + (if (proof-string-match isabelle-verbatim-regexp string) + (setq string (match-string 1 string)) + (unless (string-match ";[ \t]*\\'" string) + (setq string (concat string ";"))) + (setq string (concat + "\\<^sync>; " + (isar-shell-adjust-line-width) + string + " \\<^sync>;"))))) ;; ;; Configuring proof output buffer |