diff options
-rw-r--r-- | isar/isar-syntax.el | 38 |
1 files changed, 6 insertions, 32 deletions
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index 9ea749a5..c6da5caf 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -31,12 +31,8 @@ ; "Customization of Isabelle/Isar's syntax recognition" ; :group 'isar-scripting) -;; ----- syntax for font-lock and other features - -(defgroup isar-syntax nil - "Customization of Isabelle/Isar syntax for proof mode" - :group 'isar-settings) +;; ----- syntax for font-lock and other features (defconst isar-keywords-theory-enclose (append isar-keywords-theory-begin @@ -84,22 +80,6 @@ (append isar-keywords-proof-block isar-keywords-qed-block)) -(defconst isar-keywords - (append isar-keywords-control - isar-keywords-diag - isar-keywords-theory-begin - isar-keywords-theory-end - isar-keywords-theory-heading - isar-keywords-theory-decl - isar-keywords-theory-goal - isar-keywords-qed - isar-keywords-qed-block - isar-keywords-proof-goal - isar-keywords-proof-block - isar-keywords-proof-chain - isar-keywords-proof-decl - isar-keywords-proof-script)) - ;; ----- regular expressions @@ -131,17 +111,11 @@ (defconst isar-save-with-hole-regexp "$^") ; n.a. -(defcustom isar-goal-command-regexp - (proof-ids-to-regexp isar-keywords-theory-goal) - "Regular expression used to match a global goal." - :type 'regexp - :group 'isabelle-isar-config) - -(defcustom isar-local-goal-command-regexp - (proof-ids-to-regexp isar-keywords-proof-goal) - "Regular expression used to match a local goal." - :type 'regexp - :group 'isabelle-isar-config) +(defconst isar-goal-command-regexp + (proof-ids-to-regexp isar-keywords-theory-goal)) + +(defconst isar-local-goal-command-regexp + (proof-ids-to-regexp isar-keywords-proof-goal)) (defconst isar-goal-with-hole-regexp (concat "\\(" (proof-ids-to-regexp isar-keywords-theory-goal) "\\)" isar-name-regexp ":") |