src/Pure/Isar/isar.ML
changeset 27432 c5ec309c6de8
parent 27428 f92d47cdc0de
child 27438 9b2427cc234e
     1.1 --- a/src/Pure/Isar/isar.ML	Tue Jul 01 21:20:18 2008 +0200
     1.2 +++ b/src/Pure/Isar/isar.ML	Tue Jul 01 21:30:08 2008 +0200
     1.3 @@ -22,6 +22,7 @@
     1.4  structure Isar: ISAR =
     1.5  struct
     1.6  
     1.7 +
     1.8  (** individual toplevel commands **)
     1.9  
    1.10  (* unique identification *)
    1.11 @@ -46,21 +47,18 @@
    1.12  
    1.13  (* datatype command *)
    1.14  
    1.15 -datatype kind = Theory | Proof | Other;
    1.16 -
    1.17  datatype command = Command of
    1.18   {prev: id,
    1.19 -  up: id,
    1.20 -  kind: kind,
    1.21 +  category: OuterKeyword.category,
    1.22    status: status};
    1.23  
    1.24 -fun make_command (prev, up, kind, status) =
    1.25 -  Command {prev = prev, up = up, kind = kind, status = status};
    1.26 +fun make_command (prev, category, status) =
    1.27 +  Command {prev = prev, category = category, status = status};
    1.28  
    1.29 -val empty_command = make_command (no_id, no_id, Other, Final (Toplevel.toplevel, NONE));
    1.30 +val empty_command = make_command (no_id, OuterKeyword.Other, Final (Toplevel.toplevel, NONE));
    1.31  
    1.32 -fun map_command f (Command {prev, up, kind, status}) = make_command (f (prev, up, kind, status));
    1.33 -fun map_status f = map_command (fn (prev, up, kind, status) => (prev, up, kind, f status));
    1.34 +fun map_command f (Command {prev, category, status}) = make_command (f (prev, category, status));
    1.35 +fun map_status f = map_command (fn (prev, category, status) => (prev, category, f status));
    1.36  
    1.37  
    1.38  (* table of identified commands *)
    1.39 @@ -76,21 +74,22 @@
    1.40  fun init_commands () = change_commands (K empty_commands);
    1.41  
    1.42  fun the_command id =
    1.43 -  if id = no_id then empty_command
    1.44 -  else
    1.45 -    (case Symtab.lookup (! global_commands) id of
    1.46 -      SOME cmd => cmd
    1.47 -    | NONE => sys_error ("Unknown command " ^ quote id));
    1.48 +  let val Command cmd =
    1.49 +    if id = no_id then empty_command
    1.50 +    else
    1.51 +      (case Symtab.lookup (! global_commands) id of
    1.52 +        SOME cmd => cmd
    1.53 +      | NONE => sys_error ("Unknown command " ^ quote id))
    1.54 +  in cmd end;
    1.55  
    1.56  fun the_state id =
    1.57    (case the_command id of
    1.58 -    Command {status = Final res, ...} => res
    1.59 +    {status = Final res, ...} => res
    1.60    | _ => sys_error ("Unfinished command " ^ quote id));
    1.61  
    1.62  end;
    1.63  
    1.64  
    1.65 -
    1.66  (** TTY interaction **)
    1.67  
    1.68  (* global point *)
    1.69 @@ -124,9 +123,8 @@
    1.70    let
    1.71      val (id, tr) = identify raw_tr;
    1.72      val (prev, (prev_state, _)) = point_state ();
    1.73 -    val up = no_id;  (* FIXME *)
    1.74 -    val kind = Other;  (* FIXME *)
    1.75 -    val _ = change_commands (Symtab.update (id, make_command (prev, up, kind, Initial tr)));
    1.76 +    val category = OuterKeyword.category_of (Toplevel.name_of tr);
    1.77 +    val _ = change_commands (Symtab.update (id, make_command (prev, category, Initial tr)));
    1.78    in
    1.79      (case Toplevel.transition true tr prev_state of
    1.80        NONE => (change_commands (Symtab.delete_safe id); false)