src/Pure/PIDE/document.ML

     Header of node_header |
     Perspective of command_id list
   type edit = string * node_edit
   type state
   val init_state: state
-  val define_command: command_id -> string -> state -> state
+  val define_command: command_id -> string -> string -> state -> state
   val join_commands: state -> state
   val cancel_execution: state -> Future.task list
   val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
   val update: version_id -> version_id -> edit list -> state ->
     ((command_id * exec_id option) list * (string * command_id option) list) * state

 (** global state -- document structure and execution process **)
 
 abstype state = State of
  {versions: version Inttab.table,  (*version_id -> document content*)
   commands:
-    Toplevel.transition future Inttab.table *  (*command_id -> transition (future parsing)*)
+    (string * Toplevel.transition future) Inttab.table *  (*command_id -> name * transition*)
     Toplevel.transition future list,  (*recent commands to be joined*)
   execs: (command_id * (Toplevel.state * unit lazy) lazy) Inttab.table,
     (*exec_id -> command_id with eval/print process*)
   execution: Future.group}  (*global execution process*)
 with

 fun map_state f (State {versions, commands, execs, execution}) =
   make_state (f (versions, commands, execs, execution));
 
 val init_state =
   make_state (Inttab.make [(no_id, empty_version)],
-    (Inttab.make [(no_id, Future.value Toplevel.empty)], []),
+    (Inttab.make [(no_id, (Toplevel.name_of Toplevel.empty, Future.value Toplevel.empty))], []),
     Inttab.make [(no_id, (no_id, Lazy.value (Toplevel.toplevel, no_print)))],
     Future.new_group NONE);
 
 
 (* document versions *)

   | SOME version => version);
 
 
 (* commands *)
 
-fun define_command (id: command_id) text =
+fun define_command (id: command_id) name text =
   map_state (fn (versions, (commands, recent), execs, execution) =>
     let
       val id_string = print_id id;
       val tr =
         Future.fork_pri 2 (fn () =>
           Position.setmp_thread_data (Position.id_only id_string)
             (fn () => Outer_Syntax.read_command (Position.id id_string) text) ());
       val commands' =
-        Inttab.update_new (id, tr) commands
+        Inttab.update_new (id, (name, tr)) commands
           handle Inttab.DUP dup => err_dup "command" dup;
     in (versions, (commands', tr :: recent), execs, execution) end);
 
 fun the_command (State {commands, ...}) (id: command_id) =
   (case Inttab.lookup (#1 commands) id of
     NONE => err_undef "command" id
-  | SOME tr => tr);
+  | SOME command => command);
 
 val join_commands =
     map_state (fn (versions, (commands, recent), execs, execution) =>
       (Future.join_results recent; (versions, (commands, []), execs, execution)));
 

     val visible' = visible andalso common' <> last_visible;
   in (common', visible') end;
 
 fun new_exec state init command_id' (execs, exec) =
   let
-    val command' = the_command state command_id';
+    val (_, tr0) = the_command state command_id';
     val exec_id' = new_id ();
     val exec' =
       snd exec |> Lazy.map (fn (st, _) =>
         let val tr =
-          Future.join command'
+          Future.join tr0
           |> Toplevel.modify_init init
           |> Toplevel.put_id (print_id exec_id');
         in run_command tr st end)
       |> pair command_id';
   in ((exec_id', exec') :: execs, exec') end;