--- a/etc/isar-keywords-ZF.el Wed Jan 21 23:21:44 2009 +0100
+++ b/etc/isar-keywords-ZF.el Wed Jan 21 23:25:17 2009 +0100
@@ -3,14 +3,16 @@
;; Generated from Pure + Pure-ProofGeneral + FOL + ZF.
;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
;;
-;; $Id$
-;;
(defconst isar-keywords-major
'("\\."
"\\.\\."
"Isabelle\\.command"
+ "Isar\\.begin_document"
"Isar\\.command"
+ "Isar\\.define_command"
+ "Isar\\.edit_document"
+ "Isar\\.end_document"
"Isar\\.insert"
"Isar\\.remove"
"ML"
@@ -89,7 +91,6 @@
"instantiation"
"interpret"
"interpretation"
- "invoke"
"judgment"
"kill"
"kill_thy"
@@ -135,7 +136,6 @@
"print_drafts"
"print_facts"
"print_induct_rules"
- "print_interps"
"print_locale"
"print_locales"
"print_methods"
@@ -249,7 +249,11 @@
(defconst isar-keywords-control
'("Isabelle\\.command"
+ "Isar\\.begin_document"
"Isar\\.command"
+ "Isar\\.define_command"
+ "Isar\\.edit_document"
+ "Isar\\.end_document"
"Isar\\.insert"
"Isar\\.remove"
"ProofGeneral\\.inform_file_processed"
@@ -298,7 +302,6 @@
"print_drafts"
"print_facts"
"print_induct_rules"
- "print_interps"
"print_locale"
"print_locales"
"print_methods"
@@ -438,8 +441,7 @@
(defconst isar-keywords-proof-goal
'("have"
"hence"
- "interpret"
- "invoke"))
+ "interpret"))
(defconst isar-keywords-proof-block
'("next"
--- a/etc/isar-keywords.el Wed Jan 21 23:21:44 2009 +0100
+++ b/etc/isar-keywords.el Wed Jan 21 23:25:17 2009 +0100
@@ -3,14 +3,16 @@
;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace.
;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
;;
-;; $Id$
-;;
(defconst isar-keywords-major
'("\\."
"\\.\\."
"Isabelle\\.command"
+ "Isar\\.begin_document"
"Isar\\.command"
+ "Isar\\.define_command"
+ "Isar\\.edit_document"
+ "Isar\\.end_document"
"Isar\\.insert"
"Isar\\.remove"
"ML"
@@ -46,9 +48,6 @@
"chapter"
"class"
"class_deps"
- "class_interpret"
- "class_interpretation"
- "class_locale"
"classes"
"classrel"
"code_abort"
@@ -119,7 +118,6 @@
"instantiation"
"interpret"
"interpretation"
- "invoke"
"judgment"
"kill"
"kill_thy"
@@ -172,7 +170,6 @@
"print_drafts"
"print_facts"
"print_induct_rules"
- "print_interps"
"print_locale"
"print_locales"
"print_methods"
@@ -312,7 +309,11 @@
(defconst isar-keywords-control
'("Isabelle\\.command"
+ "Isar\\.begin_document"
"Isar\\.command"
+ "Isar\\.define_command"
+ "Isar\\.edit_document"
+ "Isar\\.end_document"
"Isar\\.insert"
"Isar\\.remove"
"ProofGeneral\\.inform_file_processed"
@@ -369,7 +370,6 @@
"print_drafts"
"print_facts"
"print_induct_rules"
- "print_interps"
"print_locale"
"print_locales"
"print_methods"
@@ -423,7 +423,6 @@
"axiomatization"
"axioms"
"class"
- "class_locale"
"classes"
"classrel"
"code_abort"
@@ -507,7 +506,6 @@
(defconst isar-keywords-theory-goal
'("ax_specification"
- "class_interpretation"
"corollary"
"cpodef"
"function"
@@ -546,11 +544,9 @@
"subsubsect"))
(defconst isar-keywords-proof-goal
- '("class_interpret"
- "have"
+ '("have"
"hence"
- "interpret"
- "invoke"))
+ "interpret"))
(defconst isar-keywords-proof-block
'("next"
--- a/lib/jedit/isabelle.xml Wed Jan 21 23:21:44 2009 +0100
+++ b/lib/jedit/isabelle.xml Wed Jan 21 23:25:17 2009 +0100
@@ -2,7 +2,6 @@
<!DOCTYPE MODE SYSTEM "xmode.dtd">
<!-- Generated from Pure + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace + FOL + ZF. -->
<!-- *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** -->
-<!-- $Id$ -->
<MODE>
<PROPS>
<PROPERTY NAME="commentStart" VALUE="(*"/>
@@ -36,7 +35,11 @@
<OPERATOR>.</OPERATOR>
<OPERATOR>..</OPERATOR>
<INVALID>Isabelle.command</INVALID>
+ <INVALID>Isar.begin_document</INVALID>
<INVALID>Isar.command</INVALID>
+ <INVALID>Isar.define_command</INVALID>
+ <INVALID>Isar.edit_document</INVALID>
+ <INVALID>Isar.end_document</INVALID>
<INVALID>Isar.insert</INVALID>
<INVALID>Isar.remove</INVALID>
<OPERATOR>ML</OPERATOR>
@@ -171,7 +174,6 @@
<OPERATOR>interpret</OPERATOR>
<OPERATOR>interpretation</OPERATOR>
<KEYWORD4>intros</KEYWORD4>
- <OPERATOR>invoke</OPERATOR>
<KEYWORD4>is</KEYWORD4>
<OPERATOR>judgment</OPERATOR>
<INVALID>kill</INVALID>
@@ -239,7 +241,6 @@
<LABEL>print_drafts</LABEL>
<LABEL>print_facts</LABEL>
<LABEL>print_induct_rules</LABEL>
- <LABEL>print_interps</LABEL>
<LABEL>print_locale</LABEL>
<LABEL>print_locales</LABEL>
<LABEL>print_methods</LABEL>