1.1 --- a/lib/scripts/keywords	Fri Mar 16 18:21:22 2012 +0100
     1.2 +++ b/lib/scripts/keywords	Fri Mar 16 20:33:33 2012 +0100
     1.3 @@ -30,18 +30,67 @@
     1.4    }
     1.5  }
     1.6  
     1.7 +my %convert_kinds = (
     1.8 +  "thy_begin" => "theory-begin",
     1.9 +  "thy_end" => "theory-end",
    1.10 +  "thy_heading" => "theory-heading",
    1.11 +  "thy_decl" => "theory-decl",
    1.12 +  "thy_script" => "theory-script",
    1.13 +  "thy_goal" => "theory-goal",
    1.14 +  "thy_schematic_goal" => "theory-goal",
    1.15 +  "qed_block" => "qed-block",
    1.16 +  "qed_global" => "qed-global",
    1.17 +  "prf_heading" => "proof-heading",
    1.18 +  "prf_goal" => "proof-goal",
    1.19 +  "prf_block" => "proof-block",
    1.20 +  "prf_open" => "proof-open",
    1.21 +  "prf_close" => "proof-close",
    1.22 +  "prf_chain" => "proof-chain",
    1.23 +  "prf_decl" => "proof-decl",
    1.24 +  "prf_asm" => "proof-asm",
    1.25 +  "prf_asm_goal" => "proof-asm-goal",
    1.26 +  "prf_script" => "proof-script"
    1.27 +);
    1.28 +
    1.29 +my @emacs_kinds = (
    1.30 +  "major",
    1.31 +  "minor",
    1.32 +  "control",
    1.33 +  "diag",
    1.34 +  "theory-begin",
    1.35 +  "theory-switch",
    1.36 +  "theory-end",
    1.37 +  "theory-heading",
    1.38 +  "theory-decl",
    1.39 +  "theory-script",
    1.40 +  "theory-goal",
    1.41 +  "qed",
    1.42 +  "qed-block",
    1.43 +  "qed-global",
    1.44 +  "proof-heading",
    1.45 +  "proof-goal",
    1.46 +  "proof-block",
    1.47 +  "proof-open",
    1.48 +  "proof-close",
    1.49 +  "proof-chain",
    1.50 +  "proof-decl",
    1.51 +  "proof-asm",
    1.52 +  "proof-asm-goal",
    1.53 +  "proof-script"
    1.54 +);
    1.55 +
    1.56  sub collect_keywords {
    1.57    while(<STDIN>) {
    1.58 -    if (m/^Outer syntax keyword:\s*"(.*)"/) {
    1.59 +    if (m/^Outer syntax keyword "([^"]*)" :: (\S*)/) {
    1.60 +      my $name = $1;
    1.61 +      my $kind = $2;
    1.62 +      if (defined $convert_kinds{$kind}) { $kind = $convert_kinds{$kind} }
    1.63 +      &set_keyword($name, $kind);
    1.64 +    }
    1.65 +    elsif (m/^Outer syntax keyword "([^"]*)"/) {
    1.66        my $name = $1;
    1.67        &set_keyword($name, "minor");
    1.68      }
    1.69 -    elsif (m/^Outer syntax command:\s*"(.*)"\s*\((.*)\)/) {
    1.70 -      my $name = $1;
    1.71 -      my $kind = $2;
    1.72 -      if ($kind eq "theory-schematic-goal") { $kind = "theory-goal"; }
    1.73 -      &set_keyword($name, $kind);
    1.74 -    }
    1.75    }
    1.76  }
    1.77  
    1.78 @@ -49,32 +98,6 @@
    1.79  ## Emacs output
    1.80  
    1.81  sub emacs_output {
    1.82 -  my @kinds = (
    1.83 -    "major",
    1.84 -    "minor",
    1.85 -    "control",
    1.86 -    "diag",
    1.87 -    "theory-begin",
    1.88 -    "theory-switch",
    1.89 -    "theory-end",
    1.90 -    "theory-heading",
    1.91 -    "theory-decl",
    1.92 -    "theory-script",
    1.93 -    "theory-goal",
    1.94 -    "qed",
    1.95 -    "qed-block",
    1.96 -    "qed-global",
    1.97 -    "proof-heading",
    1.98 -    "proof-goal",
    1.99 -    "proof-block",
   1.100 -    "proof-open",
   1.101 -    "proof-close",
   1.102 -    "proof-chain",
   1.103 -    "proof-decl",
   1.104 -    "proof-asm",
   1.105 -    "proof-asm-goal",
   1.106 -    "proof-script"
   1.107 -  );
   1.108    my $file = $keywords_name eq "" ? "isar-keywords.el" : "isar-keywords-${keywords_name}.el";
   1.109    open (OUTPUT, "> ${file}") || die "$!";
   1.110    select OUTPUT;
   1.111 @@ -85,7 +108,7 @@
   1.112    print ";; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***\n";
   1.113    print ";;\n";
   1.114  
   1.115 -  for my $kind (@kinds) {
   1.116 +  for my $kind (@emacs_kinds) {
   1.117      my @names;
   1.118      for my $name (keys(%keywords)) {
   1.119        if ($kind eq "major" ? $keywords{$name} ne "minor" : $keywords{$name} eq $kind) {

     2.1 --- a/src/Pure/Isar/keyword.ML	Fri Mar 16 18:21:22 2012 +0100
     2.2 +++ b/src/Pure/Isar/keyword.ML	Fri Mar 16 20:33:33 2012 +0100
     2.3 @@ -11,7 +11,6 @@
     2.4    val control: T
     2.5    val diag: T
     2.6    val thy_begin: T
     2.7 -  val thy_switch: T
     2.8    val thy_end: T
     2.9    val thy_heading: T
    2.10    val thy_decl: T
    2.11 @@ -77,30 +76,29 @@
    2.12  
    2.13  val control = kind "control";
    2.14  val diag = kind "diag";
    2.15 -val thy_begin = kind "theory-begin";
    2.16 -val thy_switch = kind "theory-switch";
    2.17 -val thy_end = kind "theory-end";
    2.18 -val thy_heading = kind "theory-heading";
    2.19 -val thy_decl = kind "theory-decl";
    2.20 -val thy_script = kind "theory-script";
    2.21 -val thy_goal = kind "theory-goal";
    2.22 -val thy_schematic_goal = kind "theory-schematic-goal";
    2.23 +val thy_begin = kind "thy_begin";
    2.24 +val thy_end = kind "thy_end";
    2.25 +val thy_heading = kind "thy_heading";
    2.26 +val thy_decl = kind "thy_decl";
    2.27 +val thy_script = kind "thy_script";
    2.28 +val thy_goal = kind "thy_goal";
    2.29 +val thy_schematic_goal = kind "thy_schematic_goal";
    2.30  val qed = kind "qed";
    2.31 -val qed_block = kind "qed-block";
    2.32 -val qed_global = kind "qed-global";
    2.33 -val prf_heading = kind "proof-heading";
    2.34 -val prf_goal = kind "proof-goal";
    2.35 -val prf_block = kind "proof-block";
    2.36 -val prf_open = kind "proof-open";
    2.37 -val prf_close = kind "proof-close";
    2.38 -val prf_chain = kind "proof-chain";
    2.39 -val prf_decl = kind "proof-decl";
    2.40 -val prf_asm = kind "proof-asm";
    2.41 -val prf_asm_goal = kind "proof-asm-goal";
    2.42 -val prf_script = kind "proof-script";
    2.43 +val qed_block = kind "qed_block";
    2.44 +val qed_global = kind "qed_global";
    2.45 +val prf_heading = kind "prf_heading";
    2.46 +val prf_goal = kind "prf_goal";
    2.47 +val prf_block = kind "prf_block";
    2.48 +val prf_open = kind "prf_open";
    2.49 +val prf_close = kind "prf_close";
    2.50 +val prf_chain = kind "prf_chain";
    2.51 +val prf_decl = kind "prf_decl";
    2.52 +val prf_asm = kind "prf_asm";
    2.53 +val prf_asm_goal = kind "prf_asm_goal";
    2.54 +val prf_script = kind "prf_script";
    2.55  
    2.56  val kinds =
    2.57 -  [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal,
    2.58 +  [control, diag, thy_begin, thy_end, thy_heading, thy_decl, thy_script, thy_goal,
    2.59      thy_schematic_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open,
    2.60      prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script]
    2.61   |> map kind_of;
    2.62 @@ -122,7 +120,6 @@
    2.63    [("control",            control),
    2.64     ("diag",               diag),
    2.65     ("thy_begin",          thy_begin),
    2.66 -   ("thy_switch",         thy_switch),
    2.67     ("thy_end",            thy_end),
    2.68     ("thy_heading",        thy_heading),
    2.69     ("thy_decl",           thy_decl),
    2.70 @@ -206,11 +203,11 @@
    2.71  
    2.72  fun keyword_status name =
    2.73    status_message (Isabelle_Markup.keyword_decl name)
    2.74 -    ("Outer syntax keyword: " ^ quote name);
    2.75 +    ("Outer syntax keyword " ^ quote name);
    2.76  
    2.77  fun command_status (name, kind) =
    2.78    status_message (Isabelle_Markup.command_decl name (kind_of kind))
    2.79 -    ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")");
    2.80 +    ("Outer syntax keyword " ^ quote name ^ " :: " ^ kind_of kind);
    2.81  
    2.82  fun status () =
    2.83    let
    2.84 @@ -253,7 +250,7 @@
    2.85  val is_theory_begin = command_category [thy_begin];
    2.86  
    2.87  val is_theory = command_category
    2.88 -  [thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal, thy_schematic_goal];
    2.89 +  [thy_begin, thy_end, thy_heading, thy_decl, thy_script, thy_goal, thy_schematic_goal];
    2.90  
    2.91  val is_proof = command_category
    2.92    [qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,

     3.1 --- a/src/Pure/Isar/keyword.scala	Fri Mar 16 18:21:22 2012 +0100
     3.2 +++ b/src/Pure/Isar/keyword.scala	Fri Mar 16 20:33:33 2012 +0100
     3.3 @@ -14,27 +14,26 @@
     3.4    val MINOR = "minor"
     3.5    val CONTROL = "control"
     3.6    val DIAG = "diag"
     3.7 -  val THY_BEGIN = "theory-begin"
     3.8 -  val THY_SWITCH = "theory-switch"
     3.9 -  val THY_END = "theory-end"
    3.10 -  val THY_HEADING = "theory-heading"
    3.11 -  val THY_DECL = "theory-decl"
    3.12 -  val THY_SCRIPT = "theory-script"
    3.13 -  val THY_GOAL = "theory-goal"
    3.14 -  val THY_SCHEMATIC_GOAL = "theory-schematic-goal"
    3.15 +  val THY_BEGIN = "thy_begin"
    3.16 +  val THY_END = "thy_end"
    3.17 +  val THY_HEADING = "thy_heading"
    3.18 +  val THY_DECL = "thy_decl"
    3.19 +  val THY_SCRIPT = "thy_script"
    3.20 +  val THY_GOAL = "thy_goal"
    3.21 +  val THY_SCHEMATIC_GOAL = "thy_schematic_goal"
    3.22    val QED = "qed"
    3.23 -  val QED_BLOCK = "qed-block"
    3.24 -  val QED_GLOBAL = "qed-global"
    3.25 -  val PRF_HEADING = "proof-heading"
    3.26 -  val PRF_GOAL = "proof-goal"
    3.27 -  val PRF_BLOCK = "proof-block"
    3.28 -  val PRF_OPEN = "proof-open"
    3.29 -  val PRF_CLOSE = "proof-close"
    3.30 -  val PRF_CHAIN = "proof-chain"
    3.31 -  val PRF_DECL = "proof-decl"
    3.32 -  val PRF_ASM = "proof-asm"
    3.33 -  val PRF_ASM_GOAL = "proof-asm-goal"
    3.34 -  val PRF_SCRIPT = "proof-script"
    3.35 +  val QED_BLOCK = "qed_block"
    3.36 +  val QED_GLOBAL = "qed_global"
    3.37 +  val PRF_HEADING = "prf_heading"
    3.38 +  val PRF_GOAL = "prf_goal"
    3.39 +  val PRF_BLOCK = "prf_block"
    3.40 +  val PRF_OPEN = "prf_open"
    3.41 +  val PRF_CLOSE = "prf_close"
    3.42 +  val PRF_CHAIN = "prf_chain"
    3.43 +  val PRF_DECL = "prf_decl"
    3.44 +  val PRF_ASM = "prf_asm"
    3.45 +  val PRF_ASM_GOAL = "prf_asm_goal"
    3.46 +  val PRF_SCRIPT = "prf_script"
    3.47  
    3.48  
    3.49    /* categories */
    3.50 @@ -43,9 +42,8 @@
    3.51    val control = Set(CONTROL)
    3.52    val diag = Set(DIAG)
    3.53    val theory =
    3.54 -    Set(THY_BEGIN, THY_SWITCH, THY_END, THY_HEADING, THY_DECL, THY_SCRIPT,
    3.55 -      THY_GOAL, THY_SCHEMATIC_GOAL)
    3.56 -  val theory1 = Set(THY_BEGIN, THY_SWITCH, THY_END)
    3.57 +    Set(THY_BEGIN, THY_END, THY_HEADING, THY_DECL, THY_SCRIPT, THY_GOAL, THY_SCHEMATIC_GOAL)
    3.58 +  val theory1 = Set(THY_BEGIN, THY_END)
    3.59    val theory2 = Set(THY_DECL, THY_GOAL)
    3.60    val proof =
    3.61      Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING, PRF_GOAL, PRF_BLOCK,

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