# HG changeset patch
# User wenzelm
# Date 1214930323 -7200
# Node ID f6751d265cf6340d044e73c9f90b2e272ba7ca6d
# Parent  c0ef698c09041ec7043525609779cf928889688e
added name_of;
added get_id/put_id;
tuned;

diff -r c0ef698c0904 -r f6751d265cf6 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Jul 01 18:38:41 2008 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Jul 01 18:38:43 2008 +0200
@@ -46,6 +46,7 @@
   type transition
   val undo_limit: bool -> int option
   val empty: transition
+  val name_of: transition -> string
   val name: string -> transition -> transition
   val position: Position.T -> transition -> transition
   val interactive: bool -> transition -> transition
@@ -83,6 +84,8 @@
   val actual_proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition
   val skip_proof: (int History.T -> int History.T) -> transition -> transition
   val skip_proof_to_theory: (int -> bool) -> transition -> transition
+  val get_id: transition -> string option
+  val put_id: string -> transition -> transition
   val unknown_theory: transition -> transition
   val unknown_proof: transition -> transition
   val unknown_context: transition -> transition
@@ -455,9 +458,10 @@
 
 (* diagnostics *)
 
-fun str_of_transition (Transition {name, pos, ...}) = quote name ^ Position.str_of pos;
+fun name_of (Transition {name, ...}) = name;
+fun str_of (Transition {name, pos, ...}) = quote name ^ Position.str_of pos;
 
-fun command_msg msg tr = msg ^ "command " ^ str_of_transition tr;
+fun command_msg msg tr = msg ^ "command " ^ str_of tr;
 fun at_command tr = command_msg "At " tr ^ ".";
 
 fun type_error tr state =
@@ -632,6 +636,12 @@
 
 (** toplevel transactions **)
 
+(* identification *)
+
+fun get_id (Transition {pos, ...}) = Position.get_id pos;
+fun put_id id (tr as Transition {pos, ...}) = position (Position.put_id id pos) tr;
+
+
 (* thread position *)
 
 fun setmp_thread_position (Transition {pos, ...}) f x =