1.1 --- a/etc/isar-keywords-ZF.el Wed Jan 21 23:21:44 2009 +0100
1.2 +++ b/etc/isar-keywords-ZF.el Wed Jan 21 23:25:17 2009 +0100
1.3 @@ -3,14 +3,16 @@
1.4 ;; Generated from Pure + Pure-ProofGeneral + FOL + ZF.
1.5 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
1.6 ;;
1.7 -;; $Id$
1.8 -;;
1.9
1.10 (defconst isar-keywords-major
1.11 '("\\."
1.12 "\\.\\."
1.13 "Isabelle\\.command"
1.14 + "Isar\\.begin_document"
1.15 "Isar\\.command"
1.16 + "Isar\\.define_command"
1.17 + "Isar\\.edit_document"
1.18 + "Isar\\.end_document"
1.19 "Isar\\.insert"
1.20 "Isar\\.remove"
1.21 "ML"
1.22 @@ -89,7 +91,6 @@
1.23 "instantiation"
1.24 "interpret"
1.25 "interpretation"
1.26 - "invoke"
1.27 "judgment"
1.28 "kill"
1.29 "kill_thy"
1.30 @@ -135,7 +136,6 @@
1.31 "print_drafts"
1.32 "print_facts"
1.33 "print_induct_rules"
1.34 - "print_interps"
1.35 "print_locale"
1.36 "print_locales"
1.37 "print_methods"
1.38 @@ -249,7 +249,11 @@
1.39
1.40 (defconst isar-keywords-control
1.41 '("Isabelle\\.command"
1.42 + "Isar\\.begin_document"
1.43 "Isar\\.command"
1.44 + "Isar\\.define_command"
1.45 + "Isar\\.edit_document"
1.46 + "Isar\\.end_document"
1.47 "Isar\\.insert"
1.48 "Isar\\.remove"
1.49 "ProofGeneral\\.inform_file_processed"
1.50 @@ -298,7 +302,6 @@
1.51 "print_drafts"
1.52 "print_facts"
1.53 "print_induct_rules"
1.54 - "print_interps"
1.55 "print_locale"
1.56 "print_locales"
1.57 "print_methods"
1.58 @@ -438,8 +441,7 @@
1.59 (defconst isar-keywords-proof-goal
1.60 '("have"
1.61 "hence"
1.62 - "interpret"
1.63 - "invoke"))
1.64 + "interpret"))
1.65
1.66 (defconst isar-keywords-proof-block
1.67 '("next"
2.1 --- a/etc/isar-keywords.el Wed Jan 21 23:21:44 2009 +0100
2.2 +++ b/etc/isar-keywords.el Wed Jan 21 23:25:17 2009 +0100
2.3 @@ -3,14 +3,16 @@
2.4 ;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace.
2.5 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
2.6 ;;
2.7 -;; $Id$
2.8 -;;
2.9
2.10 (defconst isar-keywords-major
2.11 '("\\."
2.12 "\\.\\."
2.13 "Isabelle\\.command"
2.14 + "Isar\\.begin_document"
2.15 "Isar\\.command"
2.16 + "Isar\\.define_command"
2.17 + "Isar\\.edit_document"
2.18 + "Isar\\.end_document"
2.19 "Isar\\.insert"
2.20 "Isar\\.remove"
2.21 "ML"
2.22 @@ -46,9 +48,6 @@
2.23 "chapter"
2.24 "class"
2.25 "class_deps"
2.26 - "class_interpret"
2.27 - "class_interpretation"
2.28 - "class_locale"
2.29 "classes"
2.30 "classrel"
2.31 "code_abort"
2.32 @@ -119,7 +118,6 @@
2.33 "instantiation"
2.34 "interpret"
2.35 "interpretation"
2.36 - "invoke"
2.37 "judgment"
2.38 "kill"
2.39 "kill_thy"
2.40 @@ -172,7 +170,6 @@
2.41 "print_drafts"
2.42 "print_facts"
2.43 "print_induct_rules"
2.44 - "print_interps"
2.45 "print_locale"
2.46 "print_locales"
2.47 "print_methods"
2.48 @@ -312,7 +309,11 @@
2.49
2.50 (defconst isar-keywords-control
2.51 '("Isabelle\\.command"
2.52 + "Isar\\.begin_document"
2.53 "Isar\\.command"
2.54 + "Isar\\.define_command"
2.55 + "Isar\\.edit_document"
2.56 + "Isar\\.end_document"
2.57 "Isar\\.insert"
2.58 "Isar\\.remove"
2.59 "ProofGeneral\\.inform_file_processed"
2.60 @@ -369,7 +370,6 @@
2.61 "print_drafts"
2.62 "print_facts"
2.63 "print_induct_rules"
2.64 - "print_interps"
2.65 "print_locale"
2.66 "print_locales"
2.67 "print_methods"
2.68 @@ -423,7 +423,6 @@
2.69 "axiomatization"
2.70 "axioms"
2.71 "class"
2.72 - "class_locale"
2.73 "classes"
2.74 "classrel"
2.75 "code_abort"
2.76 @@ -507,7 +506,6 @@
2.77
2.78 (defconst isar-keywords-theory-goal
2.79 '("ax_specification"
2.80 - "class_interpretation"
2.81 "corollary"
2.82 "cpodef"
2.83 "function"
2.84 @@ -546,11 +544,9 @@
2.85 "subsubsect"))
2.86
2.87 (defconst isar-keywords-proof-goal
2.88 - '("class_interpret"
2.89 - "have"
2.90 + '("have"
2.91 "hence"
2.92 - "interpret"
2.93 - "invoke"))
2.94 + "interpret"))
2.95
2.96 (defconst isar-keywords-proof-block
2.97 '("next"
3.1 --- a/lib/jedit/isabelle.xml Wed Jan 21 23:21:44 2009 +0100
3.2 +++ b/lib/jedit/isabelle.xml Wed Jan 21 23:25:17 2009 +0100
3.3 @@ -2,7 +2,6 @@
3.4 <!DOCTYPE MODE SYSTEM "xmode.dtd">
3.5 <!-- Generated from Pure + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace + FOL + ZF. -->
3.6 <!-- *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** -->
3.7 -<!-- $Id$ -->
3.8 <MODE>
3.9 <PROPS>
3.10 <PROPERTY NAME="commentStart" VALUE="(*"/>
3.11 @@ -36,7 +35,11 @@
3.12 <OPERATOR>.</OPERATOR>
3.13 <OPERATOR>..</OPERATOR>
3.14 <INVALID>Isabelle.command</INVALID>
3.15 + <INVALID>Isar.begin_document</INVALID>
3.16 <INVALID>Isar.command</INVALID>
3.17 + <INVALID>Isar.define_command</INVALID>
3.18 + <INVALID>Isar.edit_document</INVALID>
3.19 + <INVALID>Isar.end_document</INVALID>
3.20 <INVALID>Isar.insert</INVALID>
3.21 <INVALID>Isar.remove</INVALID>
3.22 <OPERATOR>ML</OPERATOR>
3.23 @@ -171,7 +174,6 @@
3.24 <OPERATOR>interpret</OPERATOR>
3.25 <OPERATOR>interpretation</OPERATOR>
3.26 <KEYWORD4>intros</KEYWORD4>
3.27 - <OPERATOR>invoke</OPERATOR>
3.28 <KEYWORD4>is</KEYWORD4>
3.29 <OPERATOR>judgment</OPERATOR>
3.30 <INVALID>kill</INVALID>
3.31 @@ -239,7 +241,6 @@
3.32 <LABEL>print_drafts</LABEL>
3.33 <LABEL>print_facts</LABEL>
3.34 <LABEL>print_induct_rules</LABEL>
3.35 - <LABEL>print_interps</LABEL>
3.36 <LABEL>print_locale</LABEL>
3.37 <LABEL>print_locales</LABEL>
3.38 <LABEL>print_methods</LABEL>