Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
updated generated file;
authorwenzelm
Sat, 29 Mar 2008 19:14:03 +0100
changeset 26482 e7f677b85bfd
parent 26481 92e901171cc8
child 26483 b8f62618ad0a
updated generated file;
etc/isar-keywords-ZF.el file | annotate | diff | comparison | revisions
etc/isar-keywords.el file | annotate | diff | comparison | revisions
lib/jedit/isabelle.xml file | annotate | diff | comparison | revisions 
--- a/etc/isar-keywords-ZF.el	Sat Mar 29 19:14:03 2008 +0100
+++ b/etc/isar-keywords-ZF.el	Sat Mar 29 19:14:03 2008 +0100
@@ -12,7 +12,6 @@
     "Isabelle\\.command"
     "ML"
     "ML_command"
-    "ML_setup"
     "ML_val"
     "ProofGeneral\\.inform_file_processed"
     "ProofGeneral\\.inform_file_retracted"
@@ -266,8 +265,7 @@
     "undos_proof"))
 
 (defconst isar-keywords-diag
-  '("ML"
-    "ML_command"
+  '("ML_command"
     "ML_val"
     "cd"
     "class_deps"
@@ -321,7 +319,6 @@
     "touch_thy"
     "typ"
     "unused_thms"
-    "use"
     "use_thy"
     "value"
     "welcome"))
@@ -342,7 +339,7 @@
     "subsubsection"))
 
 (defconst isar-keywords-theory-decl
-  '("ML_setup"
+  '("ML"
     "abbreviation"
     "arities"
     "axclass"
@@ -405,7 +402,8 @@
     "typed_print_translation"
     "typedecl"
     "types"
-    "types_code"))
+    "types_code"
+    "use"))
 
 (defconst isar-keywords-theory-script
   '("inductive_cases"))
--- a/etc/isar-keywords.el	Sat Mar 29 19:14:03 2008 +0100
+++ b/etc/isar-keywords.el	Sat Mar 29 19:14:03 2008 +0100
@@ -12,7 +12,6 @@
     "Isabelle\\.command"
     "ML"
     "ML_command"
-    "ML_setup"
     "ML_val"
     "ProofGeneral\\.inform_file_processed"
     "ProofGeneral\\.inform_file_retracted"
@@ -326,8 +325,7 @@
     "undos_proof"))
 
 (defconst isar-keywords-diag
-  '("ML"
-    "ML_command"
+  '("ML_command"
     "ML_val"
     "cd"
     "class_deps"
@@ -389,7 +387,6 @@
     "touch_thy"
     "typ"
     "unused_thms"
-    "use"
     "use_thy"
     "value"
     "welcome"))
@@ -410,7 +407,7 @@
     "subsubsection"))
 
 (defconst isar-keywords-theory-decl
-  '("ML_setup"
+  '("ML"
     "abbreviation"
     "arities"
     "atom_decl"
@@ -497,7 +494,8 @@
     "typed_print_translation"
     "typedecl"
     "types"
-    "types_code"))
+    "types_code"
+    "use"))
 
 (defconst isar-keywords-theory-script
   '("inductive_cases"))
--- a/lib/jedit/isabelle.xml	Sat Mar 29 19:14:03 2008 +0100
+++ b/lib/jedit/isabelle.xml	Sat Mar 29 19:14:03 2008 +0100
@@ -36,9 +36,8 @@
       <OPERATOR>.</OPERATOR>
       <OPERATOR>..</OPERATOR>
       <INVALID>Isabelle.command</INVALID>
-      <LABEL>ML</LABEL>
+      <OPERATOR>ML</OPERATOR>
       <LABEL>ML_command</LABEL>
-      <OPERATOR>ML_setup</OPERATOR>
       <LABEL>ML_val</LABEL>
       <OPERATOR>abbreviation</OPERATOR>
       <KEYWORD4>actions</KEYWORD4>
@@ -325,7 +324,7 @@
       <INVALID>undos_proof</INVALID>
       <OPERATOR>unfolding</OPERATOR>
       <LABEL>unused_thms</LABEL>
-      <LABEL>use</LABEL>
+      <OPERATOR>use</OPERATOR>
       <LABEL>use_thy</LABEL>
       <KEYWORD4>uses</KEYWORD4>
       <OPERATOR>using</OPERATOR>
isabelle