explicit identification of toplevel commands, with status etc.;
explicit point for tty mode;
prompt: markup prev id;
tuned signature;

--- a/src/Pure/Isar/isar.ML	Tue Jul 01 18:38:43 2008 +0200
+++ b/src/Pure/Isar/isar.ML	Tue Jul 01 18:38:44 2008 +0200
@@ -13,7 +13,6 @@
   val goal: unit -> thm
   val >> : Toplevel.transition -> bool
   val >>> : Toplevel.transition list -> unit
-  val init: unit -> unit
   val crashes: exn list ref
   val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
   val loop: unit -> unit
@@ -23,12 +22,88 @@
 structure Isar: ISAR =
 struct
 
-(* the global state *)
+(** individual toplevel commands **)
+
+(* unique identification *)
+
+type id = string;
+val no_id : id = "";
+
+fun identify tr =
+  (case Toplevel.get_id tr of
+    SOME id => (id, tr)
+  | NONE =>
+      let val id = "isabelle:" ^ serial_string ()
+      in (id, Toplevel.put_id id tr) end);
+
+
+(* execution status *)
+
+datatype status =
+  Initial of Toplevel.transition |
+  Final of Toplevel.state * (exn * string) option;
+
+
+(* datatype command *)
+
+datatype kind = Theory | Proof | Other;
+
+datatype command = Command of
+ {prev: id,
+  up: id,
+  kind: kind,
+  status: status};
+
+fun make_command (prev, up, kind, status) =
+  Command {prev = prev, up = up, kind = kind, status = status};
+
+val empty_command = make_command (no_id, no_id, Other, Final (Toplevel.toplevel, NONE));
+
+fun map_command f (Command {prev, up, kind, status}) = make_command (f (prev, up, kind, status));
+fun map_status f = map_command (fn (prev, up, kind, status) => (prev, up, kind, f status));
+
 
-val global_state = ref (Toplevel.toplevel, NONE: (exn * string) option);
+(* table of identified commands *)
+
+local
+
+val empty_commands = Symtab.empty: command Symtab.table;
+val global_commands = ref empty_commands;
+
+in
+
+fun change_commands f = NAMED_CRITICAL "Isar" (fn () => change global_commands f);
+fun init_commands () = change_commands (K empty_commands);
+
+fun the_command id =
+  if id = no_id then empty_command
+  else
+    (case Symtab.lookup (! global_commands) id of
+      SOME cmd => cmd
+    | NONE => sys_error ("Unknown command " ^ quote id));
 
-fun state () = #1 (! global_state);
-fun exn () = #2 (! global_state);
+fun the_state id =
+  (case the_command id of
+    Command {status = Final res, ...} => res
+  | _ => sys_error ("Unfinished command " ^ quote id));
+
+end;
+
+
+
+(** TTY interaction **)
+
+(* global point *)
+
+local val global_point = ref no_id in
+
+fun change_point f = NAMED_CRITICAL "Isar" (fn () => change global_point f);
+
+fun point_state () = NAMED_CRITICAL "Isar" (fn () =>
+  let val id = ! global_point in (id, the_state id) end);
+
+fun state () = #1 (#2 (point_state ()));
+fun exn () = #2 (#2 (point_state ()));
 
 fun context () =
   Toplevel.context_of (state ())
@@ -38,26 +113,35 @@
   #2 (#2 (Proof.get_goal (Toplevel.proof_of (state ()))))
     handle Toplevel.UNDEF => error "No goal present";
 
+end;
+
 
 (* interactive state transformations --- NOT THREAD-SAFE! *)
 
 nonfix >> >>>;
 
-fun >> tr =
-  (case Toplevel.transition true tr (state ()) of
-    NONE => false
-  | SOME (state', exn_info) =>
-      (global_state := (state', exn_info);
-        (case exn_info of
-          NONE => ()
-        | SOME err => Toplevel.error_msg tr err);
-        true));
+fun >> raw_tr =
+  let
+    val (id, tr) = identify raw_tr;
+    val (prev, (prev_state, _)) = point_state ();
+    val up = no_id;  (* FIXME *)
+    val kind = Other;  (* FIXME *)
+    val _ = change_commands (Symtab.update (id, make_command (prev, up, kind, Initial tr)));
+  in
+    (case Toplevel.transition true tr prev_state of
+      NONE => (change_commands (Symtab.delete_safe id); false)
+    | SOME result =>
+        (change_commands (Symtab.map_entry id (map_status (K (Final result))));
+          change_point (K id);
+          (case #2 result of
+            NONE => ()
+          | SOME err => Toplevel.error_msg tr err);
+          true))
+  end;
 
 fun >>> [] = ()
   | >>> (tr :: trs) = if >> tr then >>> trs else ();
 
-fun init () = (>> (Toplevel.init_empty (K true) (K ()) Toplevel.empty); ());
-
 
 (* toplevel loop *)
 
@@ -69,8 +153,12 @@
   let
     fun check_secure () =
       (if secure then warning "Secure loop -- cannot exit to ML" else (); secure);
+    val prev = #1 (point_state ());
+    val prompt_markup =
+      if prev = no_id then I
+      else Markup.markup (Markup.properties [(Markup.idN, prev)] Markup.position);
   in
-    (case Source.get_single (Source.set_prompt Source.default_prompt src) of
+    (case Source.get_single (Source.set_prompt (prompt_markup Source.default_prompt) src) of
       NONE => if secure then quit () else ()
     | SOME (tr, src') => if >> tr orelse check_secure () then raw_loop secure src' else ())
     handle exn => (Output.error_msg (Toplevel.exn_message exn) handle crash =>
@@ -81,9 +169,9 @@
 
 in
 
-fun toplevel_loop {init = do_init, welcome, sync, secure} =
+fun toplevel_loop {init, welcome, sync, secure} =
  (Context.set_thread_data NONE;
-  if do_init then init () else ();
+  if init then init_commands () else ();
   if welcome then writeln (Session.welcome ()) else ();
   uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ());