# HG changeset patch
# User wenzelm
# Date 1445206759 -7200
# Node ID 078ec7b710abb81dfeb39900c4bd1b90e0848e16
# Parent  eec2c9aee907b56139b07a0ac1e86b74c7af7443
tuned;

diff -r eec2c9aee907 -r 078ec7b710ab src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Sun Oct 18 23:03:43 2015 +0200
+++ b/src/Pure/General/antiquote.ML	Mon Oct 19 00:19:19 2015 +0200
@@ -84,15 +84,15 @@
 
 val scan_antiq_body =
   Scan.trace (Symbol_Pos.scan_string_qq err_prefix || Symbol_Pos.scan_string_bq err_prefix) >> #2 ||
-  Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >> #2 ||
+  Symbol_Pos.scan_cartouche err_prefix ||
   Scan.one (fn (s, _) => s <> "}" andalso Symbol.not_eof s) >> single;
 
 in
 
 val scan_control =
   Scan.one (Symbol.is_control o Symbol_Pos.symbol) --
-  Scan.trace (Symbol_Pos.scan_cartouche err_prefix) >>
-    (fn ((control, pos), (_, body)) =>
+  Symbol_Pos.scan_cartouche err_prefix >>
+    (fn ((control, pos), body) =>
       let
         val Symbol.Control name = Symbol.decode control;
         val range = Symbol_Pos.range ((control, pos) :: body);
@@ -109,7 +109,7 @@
        body = body});
 
 val scan_antiquote =
-  scan_control >> Control || scan_antiq >> Antiq || scan_txt >> Text;
+  scan_txt >> Text || scan_control >> Control || scan_antiq >> Antiq;
 
 end;
 
diff -r eec2c9aee907 -r 078ec7b710ab src/Pure/General/antiquote.scala
--- a/src/Pure/General/antiquote.scala	Sun Oct 18 23:03:43 2015 +0200
+++ b/src/Pure/General/antiquote.scala	Mon Oct 19 00:19:19 2015 +0200
@@ -42,7 +42,7 @@
       "@{" ~ rep(antiq_body) ~ "}" ^^ { case x ~ y ~ z => x + y.mkString + z }
 
     val antiquote: Parser[Antiquote] =
-      control ^^ (x => Control(x)) | (antiq ^^ (x => Antiq(x)) | txt ^^ (x => Text(x)))
+      txt ^^ (x => Text(x)) | (control ^^ (x => Control(x)) | antiq ^^ (x => Antiq(x)))
   }