improved classification of keywords (see also isar-keywords.el);

improved regexps and font-lock;

1 files changed, 43 insertions, 219 deletions

diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el
index 4f891738..1f7b7c02 100644
--- a/isar/isar-syntax.el
+++ b/isar/isar-syntax.el
@@ -8,6 +8,7 @@
 ;;
 
 (require 'proof-syntax)
+(require 'isar-keywords)
 
 ;;; Proof mode customization: how should it work?
 ;;;   Presently we have a bunch of variables in proof.el which are
@@ -36,207 +37,32 @@
   "Customization of Isabelle/Isar syntax for proof mode"
   :group 'isar-settings)
 
-;MMW FIXME This stuff should be generated automatically (and made logic specific).
-;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))
+(defconst isar-keywords-theory-enclose
+  (append isar-keywords-theory-begin
+	  isar-keywords-theory-end))
 
-(defcustom isar-keywords-end-theory
-  '(
-    "end"
-    )
-  "Isabelle/Isar keywords end theory commands."
-  :group 'isar-syntax
-  :type '(repeat string))
+(defconst isar-keywords-theory
+  (append isar-keywords-theory-heading
+	  isar-keywords-theory-decl
+	  isar-keywords-theory-goal))
 
+(defconst isar-keywords-proof-enclose
+  (append isar-keywords-proof-block
+	  isar-keywords-qed))
 
-(defcustom isar-keywords-diag
-  '()
-  "Isabelle/Isar keywords diagnostic commands."
-  :group 'isar-syntax
-  :type '(repeat string))
+(defconst isar-keywords-proof
+  (append isar-keywords-proof-goal
+	  isar-keywords-proof-chain
+	  isar-keywords-proof-decl))
 
-
-
-(defcustom isar-keywords-decl
-  '(
-    "use_thy"
-    "use" 
-    "undos"
-    "undo"
-    "types"
-    "typedecl"
-    "typed_print_translation"
-    "typ"
-    "translations"
-    "top"
-    "token_translation"
-    "title"
-    "thm"
-    "text"
-    "term"
-    "syntax"
-    "subsubsection"
-    "subsection"
-    "setup"
-    "section"
-    "rep_datatype"
-    "redos"
-    "redo"
-    "record"
-    "recdef"
-    "quit"
-    "pwd"
-    "prop"
-    "print_translation"
-    "print_theory"
-    "print_theorems"
-    "print_syntax"
-    "print_methods"
-    "print_facts"
-    "print_binds"
-    "print_attributes"
-    "print_ast_translation"
-    "primrec"
-    "pr"
-    "path"
-    "parse_translation"
-    "parse_ast_translation"
-    "oracle"
-    "nonterminals"
-    "local"
-    "load"
-    "kill_proof"
-    "inductive"
-    "help"
-    "global"
-    "exit"
-    "defaultsort"
-    "datatype"
-    "consts"
-    "commit"
-    "constdefs"
-    "coinductive"
-    "classrel"
-    "classes"
-    "chapter"
-    "cd"
-    "axioms"
-    "axclass"
-    "arities"
-    "ML"
-    )
-  "Isabelle/Isar keywords for declarations."
-  :group 'isar-syntax
-  :type '(repeat string))
-
-(defcustom isar-keywords-defn
-  '(
-    "theorems"
-    "lemmas"
-    "defs"
-    "axclass"
-    )
-  "Isabelle/Isar keywords for definitions"
-  :group 'isar-syntax
-  :type '(repeat string))
-
-(defcustom isar-keywords-goal
-  '(
-    "typedef"
-    "theorem"
-    "lemma"
-    "instance"
-    )
-  "Isabelle/Isar commands to begin an interactive proof"
-  :group 'isar-syntax
-  :type '(repeat string))
-
-(defcustom isar-keywords-save
-  '(
-    "qed_with"
-    "qed"
-    "by"
-    "\\.\\."
-    "\\."
-    )
-  "Isabelle/Isar commands finish a top-level proof and store the theorem"
-  :group 'isar-syntax
-  :type '(repeat string))
-
-(defcustom isar-keywords-kill-goal
-  '("kill")
-  "Isabelle/Isar kill command keywords"
-  :group 'isar-syntax
-  :type '(repeat string))
-
-(defcustom isar-keywords-minor
-  '(
-    "and"
-    "as"
-    "binder"
-    "infixl"
-    "infixr"
-    "is"
-    "output"
-    )
-  "Isabelle/Isar minor keywords"
-  :group 'isar-syntax
-  :type '(repeat string))
-
-(defcustom isar-keywords-proof-commands
-  '(
-;    "qed"
-    "proof" 
-    "next"
-;    "by"
-;    "\\.\\."
-;    "\\."
-    )
-  "Isabelle/Isar proof command keywords"
-  :group 'isar-syntax
-  :type '(repeat string))
-
-(defcustom isar-keywords-commands
-  '(
-    "up"
-    "thus"
-    "then_refine"
-    "then"
-    "show"
-    "refine"
-    "prev"
-    "note"
-    "let"
-    "hence"
-    "have"
-    "from"
-    "fix"
-    "back"
-    "assume"
-    "{{"
-    "}}"
-    )
-  "Isabelle/Isar command keywords"
-  :group 'isar-syntax
-  :type '(repeat string))
-
-
-;; NB: this means that any adjustments above by customize will
-;; only have effect in next session.
 (defconst isar-keywords
-  (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")
+  (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-proof-goal
+	  isar-keywords-proof-block isar-keywords-proof-chain
+	  isar-keywords-proof-decl isar-keywords-proof-script))
 
 
 ;; ----- regular expressions
@@ -247,14 +73,11 @@
 (defconst isar-ids (proof-ids isar-id "[ \t]*")
   "Matches a sequence of identifiers separated by whitespace.")
 
-;;FIXME
 (defconst isar-string "\"\\(\\([^\\\"]\\|\\\\\"\\)*\\)\"")
-;;(defconst isar-string "\"\\(\\([^\\\"]\\|\\\\\"\\)*\\)\"\\|{|\\(\\([^|]\\||[^}]\\)*\\)|}")
-;;(defconst isar-string "{|\\([^|]*\\)|}")
 
-(defconst isar-string-regexp
-  (concat "\\s-*" isar-string "\\s-*")
-  "Regexp matching Isabelle/Isar strings, with contents bracketed.")
+(defconst isar-name-regexp
+  (concat "\\s-*\\(?:" isar-string "\\|" isar-id "\\)\\s-*")
+  "Regexp matching Isabelle/Isar names, with contents bracketed.")
 
 (defvar isar-font-lock-terms
   (list
@@ -268,37 +91,38 @@
   "*Font-lock table for Isabelle terms.")
 
 (defconst isar-save-command-regexp
-  (concat "^" (proof-ids-to-regexp isar-keywords-save)))
-
-; 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))
+  (concat "^" (proof-ids-to-regexp isar-keywords-qed)))
 
-(defconst isar-save-with-hole-regexp "^FIXME$\\(\\)")
+(defconst isar-save-with-hole-regexp "$^") ; n.a.
 
 (defcustom isar-goal-command-regexp
-  (proof-ids-to-regexp isar-keywords-goal)
-  "Regular expression used to match a goal."
+  (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)
 
-;; MMW FIXME ??
 (defconst isar-goal-with-hole-regexp
-  (concat "\\("
-	  (proof-ids-to-regexp isar-keywords-goal)
-	  "\\)" isar-string-regexp)
+  (concat "\\(" (proof-ids-to-regexp isar-keywords-theory-goal) "\\)" isar-name-regexp ":")
   "Regexp matching goal commands in Isabelle/Isar which name a theorem")
 
+
 (defvar isar-font-lock-keywords-1
   (append
    isar-font-lock-terms
    (list
-    (cons (proof-ids-to-regexp isar-keywords-proof-commands) 'font-lock-function-name-face)
-    (cons (proof-ids-to-regexp isar-keywords) 'font-lock-keyword-face)
     (cons (proof-ids-to-regexp isar-keywords-minor) 'font-lock-type-face)
-    (list isar-goal-with-hole-regexp 2 'font-lock-function-name-face)
-    (list isar-save-with-hole-regexp 2 'font-lock-function-name-face))))
+    (cons (proof-ids-to-regexp isar-keywords-control) 'proof-error-face)
+    (cons (proof-ids-to-regexp isar-keywords-diag) 'proof-tacticals-name-face)
+    (cons (proof-ids-to-regexp isar-keywords-theory-enclose) 'font-lock-function-name-face)
+    (cons (proof-ids-to-regexp isar-keywords-theory) 'font-lock-keyword-face)
+    (cons (proof-ids-to-regexp isar-keywords-proof-enclose) 'font-lock-function-name-face)
+    (cons (proof-ids-to-regexp isar-keywords-proof) 'font-lock-keyword-face)
+    (cons (proof-ids-to-regexp isar-keywords-proof-script) 'font-lock-reference-face))))
 
 (provide 'isar-syntax)