# HG changeset patch
# User wenzelm
# Date 1220434019 -7200
# Node ID 44054657ea5607f6d954088f8e5b772be020664d
# Parent  c62364a6aeed3428ce0126eaa3eeeb74169d1c45
added pos_of;

diff -r c62364a6aeed -r 44054657ea56 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Sep 03 11:18:55 2008 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Sep 03 11:26:59 2008 +0200
@@ -46,6 +46,7 @@
   val empty: transition
   val init_of: transition -> string option
   val name_of: transition -> string
+  val pos_of: transition -> Position.T
   val str_of: transition -> string
   val name: string -> transition -> transition
   val position: Position.T -> transition -> transition
@@ -423,7 +424,8 @@
   | init_of _ = NONE;
 
 fun name_of (Transition {name, ...}) = name;
-fun str_of (Transition {name, pos, ...}) = quote name ^ Position.str_of pos;
+fun pos_of (Transition {pos, ...}) = pos;
+fun str_of tr = quote (name_of tr) ^ Position.str_of (pos_of tr);
 
 fun command_msg msg tr = msg ^ "command " ^ str_of tr;
 fun at_command tr = command_msg "At " tr ^ ".";