diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 1999-10-26 17:22:38 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 1999-10-26 17:22:38 +0000 |
| commit | e08dcc1bdc8f028a152fb14fbcce91c5632068bb (patch) | |
| tree | 7c733fa243b9ca483061ed76a280b999238a3692 /isa/isa-syntax.el | |
| parent | 5b59f4e964b5fcfa45866a1f76b312544bb6937e (diff) | |
isa-keywords-save: removed "result";
isa-keywords-commands: added "ProofGeneral.repeat_undo";
added isa-keywords-proof-commands;
added isa-verbatim;
Diffstat (limited to 'isa/isa-syntax.el')
| -rw-r--r-- | isa/isa-syntax.el | 20 |
1 files 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 |