# HG changeset patch
# User wenzelm
# Date 1253022297 -7200
# Node ID bf6c78d9f94c2e09203532090ba7d7b80617626d
# Parent  719426c9e1eb656340a73457066aaf663b5f873b# Parent  62b5b538408d11b2b59a08f4e6821ff8b6356f68
merged

diff -r 719426c9e1eb -r bf6c78d9f94c src/Pure/General/position.ML
--- a/src/Pure/General/position.ML	Tue Sep 15 15:29:11 2009 +0200
+++ b/src/Pure/General/position.ML	Tue Sep 15 15:44:57 2009 +0200
@@ -21,6 +21,7 @@
   val line: int -> T
   val line_file: int -> string -> T
   val id: string -> T
+  val id_only: string -> T
   val get_id: T -> string option
   val put_id: string -> T -> T
   val of_properties: Properties.T -> T
@@ -97,8 +98,8 @@
 fun line_file i name = Pos ((i, 0, 0), file_name name);
 fun line i = line_file i "";
 
-
 fun id id = Pos ((0, 0, 1), [(Markup.idN, id)]);
+fun id_only id = Pos ((0, 0, 0), [(Markup.idN, id)]);
 
 fun get_id (Pos (_, props)) = Properties.get props Markup.idN;
 fun put_id id (Pos (count, props)) = Pos (count, Properties.put (Markup.idN, id) props);
diff -r 719426c9e1eb -r bf6c78d9f94c src/Pure/Isar/isar_document.ML
--- a/src/Pure/Isar/isar_document.ML	Tue Sep 15 15:29:11 2009 +0200
+++ b/src/Pure/Isar/isar_document.ML	Tue Sep 15 15:44:57 2009 +0200
@@ -278,6 +278,7 @@
 val _ =
   OuterSyntax.internal_command "Isar.define_command"
     (P.string -- P.string >> (fn (id, text) =>
+      Toplevel.position (Position.id_only id) o
       Toplevel.imperative (fn () =>
         define_command id (OuterSyntax.prepare_command (Position.id id) text))));