diff options
| author | Makarius Wenzel | 2000-05-19 09:44:55 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 2000-05-19 09:44:55 +0000 |
| commit | 275adbd95f84422f92f9c556cee12b5c64a3ee81 (patch) | |
| tree | ca333b089dab5f50206ad5baf0ca6f104af9f26f | |
| parent | 30d3c247cc8c5a55c3a9a2691aea670b04612d26 (diff) | |
isar-verbatim-regexp: include \n;
| -rw-r--r-- | isar/isar-syntax.el | 2 | ||||
| -rw-r--r-- | isar/isar.el | 4 |
2 files changed, 1 insertions, 5 deletions
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index ee7bb275..98eb0f01 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -169,7 +169,7 @@ (concat "\\(" (proof-ids-to-regexp isar-keywords-theory-goal) "\\)" isar-name-regexp ":") "Regexp matching goal commands in Isabelle/Isar which name a theorem") -(defconst isar-verbatim-regexp "^\^VERBATIM: \\(.*\\)" +(defconst isar-verbatim-regexp "^\^VERBATIM: \\(\\(.\\|\n\\)*\\)$" "Regexp matching internal marker for verbatim command output") (defun isar-verbatim (str) diff --git a/isar/isar.el b/isar/isar.el index 48ac8325..870f3b45 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -278,10 +278,6 @@ proof-shell-init-cmd (concat (isar-verbatim "ProofGeneral.init true;") - ;; FIXME: markus, could you sort this? - ;; Doesn't seem to work, maybe - ;; should be done later? with verb? - ;; or before PG.init without m/u? "\n" (isabelle-set-default-cmd)) proof-shell-restart-cmd "ProofGeneral.restart;" |