diff options
| -rw-r--r-- | isar/isar-syntax.el | 68 |
1 files changed, 50 insertions, 18 deletions
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index a0a54cb0..4f891738 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -2,9 +2,9 @@ ;; Copyright (C) 1994-1998 LFCS Edinburgh. ;; ;; Author: David Aspinall <da@dcs.ed.ac.uk> -;; Maintainer: Isabelle maintainer <isabelle@dcs.ed.ac.uk> +;; Maintainer: Markus Wenzel <wenzelm@in.tum.de> ;; -;; isar-syntax.el,v 2.14 1998/11/03 14:41:54 da Exp +;; $Id isar-syntax.el,v 2.14 1998/11/03 14:41:54 da Exp$ ;; (require 'proof-syntax) @@ -40,6 +40,33 @@ ;MMW FIXME Tune these categories. ;MMW FIXME Can I invent new categories? +(defcustom isar-keywords-begin-theory + '( + "update_context" + "theory" + "context" + ) + "Isabelle/Isar keywords begin theory commands." + :group 'isar-syntax + :type '(repeat string)) + +(defcustom isar-keywords-end-theory + '( + "end" + ) + "Isabelle/Isar keywords end theory commands." + :group 'isar-syntax + :type '(repeat string)) + + +(defcustom isar-keywords-diag + '() + "Isabelle/Isar keywords diagnostic commands." + :group 'isar-syntax + :type '(repeat string)) + + + (defcustom isar-keywords-decl '( "use_thy" @@ -88,7 +115,7 @@ "nonterminals" "local" "load" - "kill" + "kill_proof" "inductive" "help" "global" @@ -114,18 +141,15 @@ (defcustom isar-keywords-defn '( - "theory" "theorems" "lemmas" "defs" - "context" "axclass" ) "Isabelle/Isar keywords for definitions" :group 'isar-syntax :type '(repeat string)) -;; isar-keywords-goal is used to manage undo actions (defcustom isar-keywords-goal '( "typedef" @@ -140,6 +164,10 @@ (defcustom isar-keywords-save '( "qed_with" + "qed" + "by" + "\\.\\." + "\\." ) "Isabelle/Isar commands finish a top-level proof and store the theorem" :group 'isar-syntax @@ -167,14 +195,12 @@ (defcustom isar-keywords-proof-commands '( - "qed" +; "qed" "proof" "next" - "end" - "by" -;; FIXME -;; ".." -;; "." +; "by" +; "\\.\\." +; "\\." ) "Isabelle/Isar proof command keywords" :group 'isar-syntax @@ -195,9 +221,10 @@ "have" "from" "fix" - "begin" "back" "assume" + "{{" + "}}" ) "Isabelle/Isar command keywords" :group 'isar-syntax @@ -207,8 +234,8 @@ ;; NB: this means that any adjustments above by customize will ;; only have effect in next session. (defconst isar-keywords - (append isar-keywords-goal isar-keywords-save isar-keywords-decl - isar-keywords-defn isar-keywords-commands) + (append isar-keywords-diag isar-keywords-goal isar-keywords-save + isar-keywords-decl isar-keywords-defn isar-keywords-commands) "All keywords in a Isabelle/Isar theory") @@ -243,8 +270,13 @@ (defconst isar-save-command-regexp (concat "^" (proof-ids-to-regexp isar-keywords-save))) -(defconst isar-save-with-hole-regexp - (concat "\\(" (proof-ids-to-regexp isar-keywords-save) isar-string-regexp "\\)")) +; FIXME ? +;(defconst isar-save-with-hole-regexp +; (concat "\\(" (proof-ids-to-regexp isar-keywords-save) isar-string-regexp "\\)")) +;(defconst isar-save-with-hole-regexp +; (concat "\\(qed_with\\)\\s*:\\s*" isar-string-regexp)) + +(defconst isar-save-with-hole-regexp "^FIXME$\\(\\)") (defcustom isar-goal-command-regexp (proof-ids-to-regexp isar-keywords-goal) @@ -255,7 +287,7 @@ ;; MMW FIXME ?? (defconst isar-goal-with-hole-regexp (concat "\\(" - (proof-ids-to-regexp '("lemma" "theorem")) + (proof-ids-to-regexp isar-keywords-goal) "\\)" isar-string-regexp) "Regexp matching goal commands in Isabelle/Isar which name a theorem") |