more precise source position for @{rail};
authorwenzelm
Tue, 03 May 2011 17:31:16 +0200
changeset 42657 6b404fe40877
parent 42656 89132fbd852a
child 42658 8f5d5d71add0
more precise source position for @{rail};
src/Pure/Isar/parse.ML
src/Pure/Thy/rail.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
--- 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;