# HG changeset patch
# User wenzelm
# Date 1215009615 -7200
# Node ID 9b2427cc234e862869a5488fab34bb4848a848cc
# Parent  727297fcf7c82aa0f17684ffe2da3f8899b4ae05
command: always keep transition, not just as initial status;
improved datatype category (moved here from outer_keyword.ML);

diff -r 727297fcf7c8 -r 9b2427cc234e src/Pure/Isar/isar.ML
--- a/src/Pure/Isar/isar.ML	Wed Jul 02 11:47:27 2008 +0200
+++ b/src/Pure/Isar/isar.ML	Wed Jul 02 16:40:15 2008 +0200
@@ -38,27 +38,46 @@
       in (id, Toplevel.put_id id tr) end);
 
 
-(* execution status *)
+(* command category *)
+
+datatype category = Empty | BeginTheory of string | Theory | Proof | Other;
 
-datatype status =
-  Initial of Toplevel.transition |
-  Final of Toplevel.state * (exn * string) option;
+fun category_of tr =
+  let val name = Toplevel.name_of tr in
+    if name = "" then Empty
+    else
+      (case Toplevel.init_of tr of
+        SOME thy_name => BeginTheory thy_name
+      | NONE =>
+          if OuterKeyword.is_theory name then Theory
+          else if OuterKeyword.is_proof name then Proof
+          else Other)
+  end;
 
 
 (* datatype command *)
 
+datatype status =
+  Initial |
+  Final of Toplevel.state * (exn * string) option;
+
 datatype command = Command of
  {prev: id,
-  category: OuterKeyword.category,
+  category: category,
+  transition: Toplevel.transition,
   status: status};
 
-fun make_command (prev, category, status) =
-  Command {prev = prev, category = category, status = status};
+fun make_command (prev, category, transition, status) =
+  Command {prev = prev, category = category, transition = transition, status = status};
+
+val empty_command =
+  make_command (no_id, Empty, Toplevel.empty, Final (Toplevel.toplevel, NONE));
 
-val empty_command = make_command (no_id, OuterKeyword.Other, Final (Toplevel.toplevel, NONE));
+fun map_command f (Command {prev, category, transition, status}) =
+  make_command (f (prev, category, transition, status));
 
-fun map_command f (Command {prev, category, status}) = make_command (f (prev, category, status));
-fun map_status f = map_command (fn (prev, category, status) => (prev, category, f status));
+fun map_status f = map_command (fn (prev, category, transition, status) =>
+  (prev, category, transition, f status));
 
 
 (* table of identified commands *)
@@ -123,8 +142,8 @@
   let
     val (id, tr) = identify raw_tr;
     val (prev, (prev_state, _)) = point_state ();
-    val category = OuterKeyword.category_of (Toplevel.name_of tr);
-    val _ = change_commands (Symtab.update (id, make_command (prev, category, Initial tr)));
+    val category = category_of tr;
+    val _ = change_commands (Symtab.update (id, make_command (prev, category, tr, Initial)));
   in
     (case Toplevel.transition true tr prev_state of
       NONE => (change_commands (Symtab.delete_safe id); false)