# HG changeset patch
# User wenzelm
# Date 1314957133 -7200
# Node ID 317e4962dd0f5df3099f1687dd43c55f515e5982
# Parent  9987ae55e17b3e50910eff08c5562bdbf0d7e136
clarified define_command: store name as structural information;

diff -r 9987ae55e17b -r 317e4962dd0f src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Thu Sep 01 23:08:42 2011 +0200
+++ b/src/Pure/PIDE/document.ML	Fri Sep 02 11:52:13 2011 +0200
@@ -24,7 +24,7 @@
   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
@@ -233,7 +233,7 @@
 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*)
@@ -248,7 +248,7 @@
 
 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);
 
@@ -269,7 +269,7 @@
 
 (* 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;
@@ -278,14 +278,14 @@
           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) =>
@@ -400,12 +400,12 @@
 
 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)
diff -r 9987ae55e17b -r 317e4962dd0f src/Pure/PIDE/isar_document.ML
--- a/src/Pure/PIDE/isar_document.ML	Thu Sep 01 23:08:42 2011 +0200
+++ b/src/Pure/PIDE/isar_document.ML	Fri Sep 02 11:52:13 2011 +0200
@@ -9,7 +9,8 @@
 
 val _ =
   Isabelle_Process.add_command "Isar_Document.define_command"
-    (fn [id, text] => Document.change_state (Document.define_command (Document.parse_id id) text));
+    (fn [id, name, text] =>
+      Document.change_state (Document.define_command (Document.parse_id id) name text));
 
 val _ =
   Isabelle_Process.add_command "Isar_Document.cancel_execution"
diff -r 9987ae55e17b -r 317e4962dd0f src/Pure/PIDE/isar_document.scala
--- a/src/Pure/PIDE/isar_document.scala	Thu Sep 01 23:08:42 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Fri Sep 02 11:52:13 2011 +0200
@@ -148,8 +148,9 @@
 {
   /* commands */
 
-  def define_command(id: Document.Command_ID, text: String): Unit =
-    input("Isar_Document.define_command", Document.ID(id), text)
+  def define_command(command: Command): Unit =
+    input("Isar_Document.define_command",
+      Document.ID(command.id), Symbol.encode(command.name), Symbol.encode(command.source))
 
 
   /* document versions */
diff -r 9987ae55e17b -r 317e4962dd0f src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Thu Sep 01 23:08:42 2011 +0200
+++ b/src/Pure/System/session.scala	Fri Sep 02 11:52:13 2011 +0200
@@ -253,7 +253,7 @@
       {
         if (!global_state().defined_command(command.id)) {
           global_state.change(_.define_command(command))
-          prover.get.define_command(command.id, Symbol.encode(command.source))
+          prover.get.define_command(command)
         }
       }
       doc_edits foreach {