diff options
| -rw-r--r-- | isa/isa-syntax.el | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/isa/isa-syntax.el b/isa/isa-syntax.el index 87f8dfaf..f83e0e5c 100644 --- a/isa/isa-syntax.el +++ b/isa/isa-syntax.el @@ -181,13 +181,6 @@ (proof-ids-to-regexp isa-keywords-proof-commands) "Regexp to match proof commands, with no extra output (apart from proof state)") -(defconst isa-verbatim-regexp "^\^VERBATIM: \\(.*\\)" - "Regexp matching internal marker for verbatim command output") - -(defun isa-verbatim (str) - "Mark internal command for verbatim output" - (concat "\^VERBATIM: " str)) - ;; ----- Isabelle inner syntax hilite |