Isabelle/Isar keyword classification (used to be in isar-syntax.el);

1 files changed, 175 insertions, 0 deletions

diff --git a/isar/isar-keywords.el b/isar/isar-keywords.el
new file mode 100644
index 00000000..53e40c8f
--- /dev/null
+++ b/isar/isar-keywords.el
@@ -0,0 +1,175 @@
+;;
+;; Keyword classification for Isabelle/Isar.
+;; File generated by Isabelle -- DO NOT EDIT!
+;;
+;; $Id$
+;;
+
+(defconst isar-keywords-minor
+  '(
+    "and"
+    "as"
+    "binder"
+    "infixl"
+    "infixr"
+    "is"
+    "output"
+    ))
+
+(defconst isar-keywords-control
+  '(
+    "break"
+    "cd"
+    "clear_undo"
+    "exit"
+    "kill"
+    "kill_proof"
+    "prev"
+    "quit"
+    "redo"
+    "restart"
+    "top"
+    "undo"
+    "undos"
+    "up"
+    ))
+
+(defconst isar-keywords-diag
+  '(
+    "ML"
+    "commit"
+    "help"
+    "pr"
+    "print_attributes"
+    "print_binds"
+    "print_facts"
+    "print_methods"
+    "print_syntax"
+    "print_theorems"
+    "print_theory"
+    "prop"
+    "pwd"
+    "term"
+    "thm"
+    "typ"
+    "update_thy"
+    "use" 
+    "use_thy"
+    ))
+
+(defconst isar-keywords-theory-begin
+  '(
+    "context"
+    "theory"
+    "update_context"
+    ))
+
+(defconst isar-keywords-theory-end
+  '(
+    "end"
+    ))
+
+(defconst isar-keywords-theory-heading
+  '(
+    "chapter"
+    "section"
+    "subsection"
+    "subsubsection"
+    ))
+
+(defconst isar-keywords-theory-decl
+  '(
+    "arities"
+    "axclass"
+    "axioms"
+    "classes"
+    "classrel"
+    "coinductive"
+    "constdefs"
+    "consts"
+    "datatype"
+    "defaultsort"
+    "defer_recdef"
+    "defs"
+    "global"
+    "inductive"
+    "lemmas"
+    "local"
+    "nonterminals"
+    "oracle"
+    "parse_ast_translation"
+    "parse_translation"
+    "path"
+    "primrec"
+    "print_ast_translation"
+    "print_translation"
+    "recdef"
+    "record"
+    "rep_datatype"
+    "setup"
+    "syntax"
+    "text"
+    "theorems"
+    "title"
+    "token_translation"
+    "translations"
+    "typed_print_translation"
+    "typedecl"
+    "types"
+    ))
+
+(defconst isar-keywords-theory-goal
+  '(
+    "typedef"
+    "theorem"
+    "lemma"
+    "instance"
+    ))
+
+(defconst isar-keywords-qed
+  '(
+    "\\."
+    "\\.\\."
+    "by"
+    "qed"
+    "qed_with"
+    ))
+
+(defconst isar-keywords-proof-goal
+  '(
+    "have"
+    "hence"
+    "show"
+    "thus"
+    ))
+
+(defconst isar-keywords-proof-block
+  '(
+    "next"
+    "proof" 
+    "{{"
+    "}}"
+    ))
+
+(defconst isar-keywords-proof-chain
+  '(
+    "then"
+    "from"
+    ))
+
+(defconst isar-keywords-proof-decl
+  '(
+    "assume"
+    "fix"
+    "let"
+    "note"
+    ))
+
+(defconst isar-keywords-proof-script
+  '(
+    "back"
+    "refine"
+    "then_refine"
+    ))
+
+(provide 'isar-keywords)