# HG changeset patch
# User wenzelm
# Date 1302384590 -7200
# Node ID e2d22eb4aeb9f1da7c9bdf663b4f8504373f67ae
# Parent  1044726454437974b96d91f5aefc809b9ef50d6a
some position reports for 'translations';

diff -r 104472645443 -r e2d22eb4aeb9 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Apr 09 15:00:23 2011 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Sat Apr 09 23:29:50 2011 +0200
@@ -171,8 +171,9 @@
 (* translations *)
 
 val trans_pat =
-  Scan.optional (Parse.$$$ "(" |-- Parse.!!! (Parse.xname --| Parse.$$$ ")")) "logic"
-    -- Parse.string;
+  Scan.optional
+    (Parse.$$$ "(" |-- Parse.!!! (Parse.xname --| Parse.$$$ ")")) "logic"
+    -- Parse.inner_syntax Parse.string;
 
 fun trans_arrow toks =
   ((Parse.$$$ "\\<rightharpoonup>" || Parse.$$$ "=>") >> K Syntax.Parse_Rule ||
diff -r 104472645443 -r e2d22eb4aeb9 src/Pure/Isar/parse.ML
--- a/src/Pure/Isar/parse.ML	Sat Apr 09 15:00:23 2011 +0200
+++ b/src/Pure/Isar/parse.ML	Sat Apr 09 23:29:50 2011 +0200
@@ -15,7 +15,8 @@
   val triple2: 'a * ('b * 'c) -> 'a * 'b * 'c
   val triple_swap: ('a * 'b) * 'c -> ('a * 'c) * 'b
   val not_eof: Token.T parser
-  val position: (Token.T list -> 'a * 'b) -> Token.T list -> ('a * Position.T) * 'b
+  val position: 'a parser -> ('a * Position.T) parser
+  val inner_syntax: 'a parser -> string parser
   val command: string parser
   val keyword: string parser
   val short_ident: string parser