From e08dcc1bdc8f028a152fb14fbcce91c5632068bb Mon Sep 17 00:00:00 2001 From: Makarius Wenzel Date: Tue, 26 Oct 1999 17:22:38 +0000 Subject: isa-keywords-save: removed "result"; isa-keywords-commands: added "ProofGeneral.repeat_undo"; added isa-keywords-proof-commands; added isa-verbatim; --- isa/isa-syntax.el | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/isa/isa-syntax.el b/isa/isa-syntax.el index 342ba447..861b6082 100644 --- a/isa/isa-syntax.el +++ b/isa/isa-syntax.el @@ -111,7 +111,7 @@ :type '(repeat string)) (defcustom isa-keywords-save - '("qed" "qed_spec_mp" "no_qed" "result") + '("qed" "qed_spec_mp" "no_qed") ;; Related commands, but having different types, so PG ;; won't bother support them: ;; "uresult" "bind_thm" "store_thm" @@ -122,7 +122,7 @@ (defcustom isa-keywords-commands '("by" "byev" "ba" "br" "be" "bd" "brs" "bes" "bds" - "chop" "choplev" "back" "undo" + "chop" "choplev" "back" "undo" "ProofGeneral.repeat_undo" "fa" "fr" "fe" "fd" "frs" "fes" "fds" "bw" "bws" "ren" ;; batch proofs @@ -138,6 +138,10 @@ isa-keywords-defn isa-keywords-commands) "All keywords in a Isabelle script") +(defconst isa-keywords-proof-commands + (append isa-keywords-goal isa-keywords-save isa-keywords-commands) + "Actual Isabelle proof script commands") + ;; The most common Isabelle/Pure tacticals (defconst isa-tacticals '("ALLGOALS" "DETERM" "EVERY" "EVERY'" "FIRST" "FIRST'" "FIRSTGOAL" @@ -197,6 +201,18 @@ "Regexp matching goal commands in Isabelle which name a theorem") +(defconst isa-proof-command-regexp + (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 (defface isabelle-class-name-face -- cgit v1.2.3