uniform keyword names within ML/Scala -- produce elisp names via external conversion;
discontinued obsolete Keyword.thy_switch;

--- a/lib/scripts/keywords	Fri Mar 16 18:21:22 2012 +0100
+++ b/lib/scripts/keywords	Fri Mar 16 20:33:33 2012 +0100
@@ -30,18 +30,67 @@
   }
 }
 
+my %convert_kinds = (
+  "thy_begin" => "theory-begin",
+  "thy_end" => "theory-end",
+  "thy_heading" => "theory-heading",
+  "thy_decl" => "theory-decl",
+  "thy_script" => "theory-script",
+  "thy_goal" => "theory-goal",
+  "thy_schematic_goal" => "theory-goal",
+  "qed_block" => "qed-block",
+  "qed_global" => "qed-global",
+  "prf_heading" => "proof-heading",
+  "prf_goal" => "proof-goal",
+  "prf_block" => "proof-block",
+  "prf_open" => "proof-open",
+  "prf_close" => "proof-close",
+  "prf_chain" => "proof-chain",
+  "prf_decl" => "proof-decl",
+  "prf_asm" => "proof-asm",
+  "prf_asm_goal" => "proof-asm-goal",
+  "prf_script" => "proof-script"
+);
+
+my @emacs_kinds = (
+  "major",
+  "minor",
+  "control",
+  "diag",
+  "theory-begin",
+  "theory-switch",
+  "theory-end",
+  "theory-heading",
+  "theory-decl",
+  "theory-script",
+  "theory-goal",
+  "qed",
+  "qed-block",
+  "qed-global",
+  "proof-heading",
+  "proof-goal",
+  "proof-block",
+  "proof-open",
+  "proof-close",
+  "proof-chain",
+  "proof-decl",
+  "proof-asm",
+  "proof-asm-goal",
+  "proof-script"
+);
+
 sub collect_keywords {
   while(<STDIN>) {
-    if (m/^Outer syntax keyword:\s*"(.*)"/) {
+    if (m/^Outer syntax keyword "([^"]*)" :: (\S*)/) {
+      my $name = $1;
+      my $kind = $2;
+      if (defined $convert_kinds{$kind}) { $kind = $convert_kinds{$kind} }
+      &set_keyword($name, $kind);
+    }
+    elsif (m/^Outer syntax keyword "([^"]*)"/) {
       my $name = $1;
       &set_keyword($name, "minor");
     }
-    elsif (m/^Outer syntax command:\s*"(.*)"\s*\((.*)\)/) {
-      my $name = $1;
-      my $kind = $2;
-      if ($kind eq "theory-schematic-goal") { $kind = "theory-goal"; }
-      &set_keyword($name, $kind);
-    }
   }
 }
 
@@ -49,32 +98,6 @@
 ## Emacs output
 
 sub emacs_output {
-  my @kinds = (
-    "major",
-    "minor",
-    "control",
-    "diag",
-    "theory-begin",
-    "theory-switch",
-    "theory-end",
-    "theory-heading",
-    "theory-decl",
-    "theory-script",
-    "theory-goal",
-    "qed",
-    "qed-block",
-    "qed-global",
-    "proof-heading",
-    "proof-goal",
-    "proof-block",
-    "proof-open",
-    "proof-close",
-    "proof-chain",
-    "proof-decl",
-    "proof-asm",
-    "proof-asm-goal",
-    "proof-script"
-  );
   my $file = $keywords_name eq "" ? "isar-keywords.el" : "isar-keywords-${keywords_name}.el";
   open (OUTPUT, "> ${file}") || die "$!";
   select OUTPUT;
@@ -85,7 +108,7 @@
   print ";; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***\n";
   print ";;\n";
 
-  for my $kind (@kinds) {
+  for my $kind (@emacs_kinds) {
     my @names;
     for my $name (keys(%keywords)) {
       if ($kind eq "major" ? $keywords{$name} ne "minor" : $keywords{$name} eq $kind) {

--- a/src/Pure/Isar/keyword.ML	Fri Mar 16 18:21:22 2012 +0100
+++ b/src/Pure/Isar/keyword.ML	Fri Mar 16 20:33:33 2012 +0100
@@ -11,7 +11,6 @@
   val control: T
   val diag: T
   val thy_begin: T
-  val thy_switch: T
   val thy_end: T
   val thy_heading: T
   val thy_decl: T
@@ -77,30 +76,29 @@
 
 val control = kind "control";
 val diag = kind "diag";
-val thy_begin = kind "theory-begin";
-val thy_switch = kind "theory-switch";
-val thy_end = kind "theory-end";
-val thy_heading = kind "theory-heading";
-val thy_decl = kind "theory-decl";
-val thy_script = kind "theory-script";
-val thy_goal = kind "theory-goal";
-val thy_schematic_goal = kind "theory-schematic-goal";
+val thy_begin = kind "thy_begin";
+val thy_end = kind "thy_end";
+val thy_heading = kind "thy_heading";
+val thy_decl = kind "thy_decl";
+val thy_script = kind "thy_script";
+val thy_goal = kind "thy_goal";
+val thy_schematic_goal = kind "thy_schematic_goal";
 val qed = kind "qed";
-val qed_block = kind "qed-block";
-val qed_global = kind "qed-global";
-val prf_heading = kind "proof-heading";
-val prf_goal = kind "proof-goal";
-val prf_block = kind "proof-block";
-val prf_open = kind "proof-open";
-val prf_close = kind "proof-close";
-val prf_chain = kind "proof-chain";
-val prf_decl = kind "proof-decl";
-val prf_asm = kind "proof-asm";
-val prf_asm_goal = kind "proof-asm-goal";
-val prf_script = kind "proof-script";
+val qed_block = kind "qed_block";
+val qed_global = kind "qed_global";
+val prf_heading = kind "prf_heading";
+val prf_goal = kind "prf_goal";
+val prf_block = kind "prf_block";
+val prf_open = kind "prf_open";
+val prf_close = kind "prf_close";
+val prf_chain = kind "prf_chain";
+val prf_decl = kind "prf_decl";
+val prf_asm = kind "prf_asm";
+val prf_asm_goal = kind "prf_asm_goal";
+val prf_script = kind "prf_script";
 
 val kinds =
-  [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal,
+  [control, diag, thy_begin, thy_end, thy_heading, thy_decl, thy_script, thy_goal,
     thy_schematic_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open,
     prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script]
  |> map kind_of;
@@ -122,7 +120,6 @@
   [("control",            control),
    ("diag",               diag),
    ("thy_begin",          thy_begin),
-   ("thy_switch",         thy_switch),
    ("thy_end",            thy_end),
    ("thy_heading",        thy_heading),
    ("thy_decl",           thy_decl),
@@ -206,11 +203,11 @@
 
 fun keyword_status name =
   status_message (Isabelle_Markup.keyword_decl name)
-    ("Outer syntax keyword: " ^ quote name);
+    ("Outer syntax keyword " ^ quote name);
 
 fun command_status (name, kind) =
   status_message (Isabelle_Markup.command_decl name (kind_of kind))
-    ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")");
+    ("Outer syntax keyword " ^ quote name ^ " :: " ^ kind_of kind);
 
 fun status () =
   let
@@ -253,7 +250,7 @@
 val is_theory_begin = command_category [thy_begin];
 
 val is_theory = command_category
-  [thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal, thy_schematic_goal];
+  [thy_begin, thy_end, thy_heading, thy_decl, thy_script, thy_goal, thy_schematic_goal];
 
 val is_proof = command_category
   [qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,

--- a/src/Pure/Isar/keyword.scala	Fri Mar 16 18:21:22 2012 +0100
+++ b/src/Pure/Isar/keyword.scala	Fri Mar 16 20:33:33 2012 +0100
@@ -14,27 +14,26 @@
   val MINOR = "minor"
   val CONTROL = "control"
   val DIAG = "diag"
-  val THY_BEGIN = "theory-begin"
-  val THY_SWITCH = "theory-switch"
-  val THY_END = "theory-end"
-  val THY_HEADING = "theory-heading"
-  val THY_DECL = "theory-decl"
-  val THY_SCRIPT = "theory-script"
-  val THY_GOAL = "theory-goal"
-  val THY_SCHEMATIC_GOAL = "theory-schematic-goal"
+  val THY_BEGIN = "thy_begin"
+  val THY_END = "thy_end"
+  val THY_HEADING = "thy_heading"
+  val THY_DECL = "thy_decl"
+  val THY_SCRIPT = "thy_script"
+  val THY_GOAL = "thy_goal"
+  val THY_SCHEMATIC_GOAL = "thy_schematic_goal"
   val QED = "qed"
-  val QED_BLOCK = "qed-block"
-  val QED_GLOBAL = "qed-global"
-  val PRF_HEADING = "proof-heading"
-  val PRF_GOAL = "proof-goal"
-  val PRF_BLOCK = "proof-block"
-  val PRF_OPEN = "proof-open"
-  val PRF_CLOSE = "proof-close"
-  val PRF_CHAIN = "proof-chain"
-  val PRF_DECL = "proof-decl"
-  val PRF_ASM = "proof-asm"
-  val PRF_ASM_GOAL = "proof-asm-goal"
-  val PRF_SCRIPT = "proof-script"
+  val QED_BLOCK = "qed_block"
+  val QED_GLOBAL = "qed_global"
+  val PRF_HEADING = "prf_heading"
+  val PRF_GOAL = "prf_goal"
+  val PRF_BLOCK = "prf_block"
+  val PRF_OPEN = "prf_open"
+  val PRF_CLOSE = "prf_close"
+  val PRF_CHAIN = "prf_chain"
+  val PRF_DECL = "prf_decl"
+  val PRF_ASM = "prf_asm"
+  val PRF_ASM_GOAL = "prf_asm_goal"
+  val PRF_SCRIPT = "prf_script"
 
 
   /* categories */
@@ -43,9 +42,8 @@
   val control = Set(CONTROL)
   val diag = Set(DIAG)
   val theory =
-    Set(THY_BEGIN, THY_SWITCH, THY_END, THY_HEADING, THY_DECL, THY_SCRIPT,
-      THY_GOAL, THY_SCHEMATIC_GOAL)
-  val theory1 = Set(THY_BEGIN, THY_SWITCH, THY_END)
+    Set(THY_BEGIN, THY_END, THY_HEADING, THY_DECL, THY_SCRIPT, THY_GOAL, THY_SCHEMATIC_GOAL)
+  val theory1 = Set(THY_BEGIN, THY_END)
   val theory2 = Set(THY_DECL, THY_GOAL)
   val proof =
     Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING, PRF_GOAL, PRF_BLOCK,

--- a/src/Pure/ProofGeneral/pgip_parser.ML	Fri Mar 16 18:21:22 2012 +0100
+++ b/src/Pure/ProofGeneral/pgip_parser.ML	Fri Mar 16 20:33:33 2012 +0100
@@ -56,7 +56,6 @@
   |> command Keyword.control          badcmd
   |> command Keyword.diag             (fn text => [D.Spuriouscmd {text = text}])
   |> command Keyword.thy_begin        thy_begin
-  |> command Keyword.thy_switch       badcmd
   |> command Keyword.thy_end          (fn text => [D.Closeblock {}, D.Closetheory {text = text}])
   |> command Keyword.thy_heading      thy_heading
   |> command Keyword.thy_decl         thy_decl