--- 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)
--- 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"
--- 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 */
--- 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 {