| 1 | Index: isar.el |
|---|
| 2 | =================================================================== |
|---|
| 3 | RCS file: /disk/cvs/proofgen/ProofGeneral/isar/isar.el,v |
|---|
| 4 | retrieving revision 9.5 |
|---|
| 5 | diff -c -r9.5 isar.el |
|---|
| 6 | *** isar.el 10 Jul 2008 18:47:49 -0000 9.5 |
|---|
| 7 | --- isar.el 10 Jul 2008 21:06:18 -0000 |
|---|
| 8 | *************** |
|---|
| 9 | *** 521,547 **** |
|---|
| 10 | ;; Configuring proof output buffer |
|---|
| 11 | ;; |
|---|
| 12 | |
|---|
| 13 | (defun isar-preprocessing () ;dynamic scoping of `string' |
|---|
| 14 | ! "Insert sync markers - acts on variable STRING by dynamic scoping." |
|---|
| 15 | (if (proof-string-match isabelle-verbatim-regexp string) |
|---|
| 16 | (setq string (match-string 1 string)) |
|---|
| 17 | (unless (proof-string-match ";[ \t]*\\'" string) |
|---|
| 18 | (setq string (concat string ";"))) |
|---|
| 19 | (setq string (concat |
|---|
| 20 | ! "\\<^sync>" |
|---|
| 21 | (isar-shell-adjust-line-width) |
|---|
| 22 | ! ;; da: this was an attempted hack to deal with ML files, |
|---|
| 23 | ! ;; unfortunately Isar complains about not seeing a theory |
|---|
| 24 | ! ;; command first: ML_setup illegal at first line |
|---|
| 25 | ! ;; Another failure is that: (* comment *) foo; |
|---|
| 26 | ! ;; ignores foo. This could be fixed by scanning for |
|---|
| 27 | ! ;; comment end in proof-script.el's function |
|---|
| 28 | ! ;; proof-segment-upto-cmdstart (which becomes even more |
|---|
| 29 | ! ;; Isar specific, then...) |
|---|
| 30 | ! ;; (if (proof-string-match "\\.ML$" (buffer-name proof-script-buffer)) |
|---|
| 31 | ! ;; (format "ML_command {* %s *};" string) |
|---|
| 32 | ! ;; string) |
|---|
| 33 | ! (proof-replace-regexp-in-string "\n" "\\\\<^newline>" string) |
|---|
| 34 | " \\<^sync>;")))) |
|---|
| 35 | |
|---|
| 36 | (defun isar-mode-config () |
|---|
| 37 | --- 521,551 ---- |
|---|
| 38 | ;; Configuring proof output buffer |
|---|
| 39 | ;; |
|---|
| 40 | |
|---|
| 41 | + (defconst isar-command-nesting-available |
|---|
| 42 | + (member "Isabelle\\.command" isar-keywords-major)) |
|---|
| 43 | + |
|---|
| 44 | + (defun isar-command-wrapping (string) |
|---|
| 45 | + (if (and isar-command-nesting-available |
|---|
| 46 | + (not (proof-string-match "^ProofGeneral\\.process_pgip" string))) |
|---|
| 47 | + (concat |
|---|
| 48 | + "Isabelle.command \"" |
|---|
| 49 | + (proof-replace-regexp-in-string |
|---|
| 50 | + "[\000-\037\"\\\\]" |
|---|
| 51 | + (lambda (str) (format "\\\\%03d" (string-to-char str))) |
|---|
| 52 | + string) |
|---|
| 53 | + "\"") |
|---|
| 54 | + (proof-replace-regexp-in-string "\n" "\\\\<^newline>" string))) |
|---|
| 55 | + |
|---|
| 56 | (defun isar-preprocessing () ;dynamic scoping of `string' |
|---|
| 57 | ! "Isabelle command wrapping - acts on variable STRING by dynamic scoping." |
|---|
| 58 | (if (proof-string-match isabelle-verbatim-regexp string) |
|---|
| 59 | (setq string (match-string 1 string)) |
|---|
| 60 | (unless (proof-string-match ";[ \t]*\\'" string) |
|---|
| 61 | (setq string (concat string ";"))) |
|---|
| 62 | (setq string (concat |
|---|
| 63 | ! " \\<^sync>; " |
|---|
| 64 | (isar-shell-adjust-line-width) |
|---|
| 65 | ! (isar-command-wrapping string) |
|---|
| 66 | " \\<^sync>;")))) |
|---|
| 67 | |
|---|
| 68 | (defun isar-mode-config () |
|---|
