# HG changeset patch
# User wenzelm
# Date 1304436676 -7200
# Node ID 6b404fe4087761683db333ed1fba6c7dac9d7e31
# Parent  89132fbd852a18a33bd7bc802d59a0043fbc9179
more precise source position for @{rail};

diff -r 89132fbd852a -r 6b404fe40877 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Tue May 03 16:54:26 2011 +0200
+++ b/src/Pure/Isar/parse.ML	Tue May 03 17:31:16 2011 +0200
@@ -16,6 +16,7 @@
   val triple_swap: ('a * 'b) * 'c -> ('a * 'c) * 'b
   val not_eof: Token.T parser
   val position: 'a parser -> ('a * Position.T) parser
+  val source_position: 'a parser -> (Symbol_Pos.text * Position.T) parser
   val inner_syntax: 'a parser -> string parser
   val command: string parser
   val keyword: string parser
diff -r 89132fbd852a -r 6b404fe40877 src/Pure/Thy/rail.ML
--- a/src/Pure/Thy/rail.ML	Tue May 03 16:54:26 2011 +0200
+++ b/src/Pure/Thy/rail.ML	Tue May 03 17:31:16 2011 +0200
@@ -258,7 +258,7 @@
 in
 
 val _ =
-  Thy_Output.antiquotation "rail" (Scan.lift (Parse.position Args.name))
+  Thy_Output.antiquotation "rail" (Scan.lift (Parse.source_position Parse.string))
     (fn {state, ...} => output_rules state o read);
 
 end;