trim_blanks after read, before eval;
clarified Raw_Token: uniform output_text;
tuned signature;

--- a/src/Pure/General/antiquote.ML	Thu Oct 15 21:17:41 2015 +0200
+++ b/src/Pure/General/antiquote.ML	Thu Oct 15 22:25:57 2015 +0200
@@ -16,6 +16,7 @@
     'a antiquote list -> Position.report_text list
   val scan_antiq: Symbol_Pos.T list -> antiq * Symbol_Pos.T list
   val scan_antiquote: Symbol_Pos.T list -> text_antiquote * Symbol_Pos.T list
+  val read': Position.T -> Symbol_Pos.T list -> text_antiquote list
   val read: Input.source -> text_antiquote list
 end;
 
@@ -99,10 +100,11 @@
 
 (* read *)
 
-fun read source =
-  (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) (Input.source_explode source) of
+fun read' pos syms =
+  (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
     SOME xs => (Position.reports_text (antiquote_reports (K []) xs); xs)
-  | NONE =>
-      error ("Malformed quotation/antiquotation source" ^ Position.here (Input.pos_of source)));
+  | NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos));
+
+fun read source = read' (Input.pos_of source) (Input.source_explode source);
 
 end;

--- a/src/Pure/General/symbol_pos.ML	Thu Oct 15 21:17:41 2015 +0200
+++ b/src/Pure/General/symbol_pos.ML	Thu Oct 15 22:25:57 2015 +0200
@@ -14,6 +14,7 @@
   val ~$$$ : Symbol.symbol -> T list -> T list * T list
   val content: T list -> string
   val range: T list -> Position.range
+  val trim_blanks: T list -> T list
   val is_eof: T -> bool
   val stopper: T Scan.stopper
   val !!! : Scan.message -> (T list -> 'a) -> T list -> 'a
@@ -59,6 +60,10 @@
       in Position.range pos pos' end
   | range [] = Position.no_range;
 
+val trim_blanks =
+  take_prefix (Symbol.is_blank o symbol) #> #2 #>
+  take_suffix (Symbol.is_blank o symbol) #> #1;
+
 
 (* stopper *)
 

--- a/src/Pure/Thy/thy_output.ML	Thu Oct 15 21:17:41 2015 +0200
+++ b/src/Pure/Thy/thy_output.ML	Thu Oct 15 22:25:57 2015 +0200
@@ -23,7 +23,7 @@
       theory -> theory
   val boolean: string -> bool
   val integer: string -> int
-  val eval_antiq: Toplevel.state -> Antiquote.antiq -> string
+  val eval_antiquote: Toplevel.state -> Antiquote.text_antiquote -> string
   val report_text: Input.source -> unit
   val check_text: Input.source -> Toplevel.state -> unit
   val present_thy: theory -> (Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
@@ -160,48 +160,50 @@
 end;
 
 
-(* eval_antiq *)
+(* eval antiquotes *)
 
-fun eval_antiq state ((ss, {range = (pos, _), ...}): Antiquote.antiq) =
+fun read_antiquotes state source =
   let
-    val keywords =
-      (case try Toplevel.presentation_context_of state of
-        SOME ctxt => Thy_Header.get_keywords' ctxt
-      | NONE =>
-          error ("Unknown context -- cannot expand document antiquotations" ^
-            Position.here pos));
+    val ants =
+      Antiquote.read' (Input.pos_of source) (Symbol_Pos.trim_blanks (Input.source_explode source));
+
+    fun words (Antiquote.Text ss) = [(#1 (Symbol_Pos.range ss), Markup.words)]
+      | words (Antiquote.Antiq _) = [];
+    val _ = Position.reports (maps words ants);
+  in ants end;
 
-    val (opts, src) = Token.read_antiq keywords antiq (ss, pos);
-    fun cmd ctxt = wrap ctxt (fn () => command src state ctxt) ();
+fun eval_antiquote _ (Antiquote.Text ss) = Symbol_Pos.content ss
+  | eval_antiquote state (Antiquote.Antiq (ss, {range = (pos, _), ...})) =
+      let
+        val keywords =
+          (case try Toplevel.presentation_context_of state of
+            SOME ctxt => Thy_Header.get_keywords' ctxt
+          | NONE =>
+              error ("Unknown context -- cannot expand document antiquotations" ^
+                Position.here pos));
 
-    val preview_ctxt = fold option opts (Toplevel.presentation_context_of state);
-    val print_ctxt = Context_Position.set_visible false preview_ctxt;
-    val _ = cmd preview_ctxt;
-    val print_modes = space_explode "," (Config.get print_ctxt modes) @ Latex.modes;
-  in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end;
+        val (opts, src) = Token.read_antiq keywords antiq (ss, pos);
+        fun cmd ctxt = wrap ctxt (fn () => command src state ctxt) ();
+
+        val preview_ctxt = fold option opts (Toplevel.presentation_context_of state);
+        val print_ctxt = Context_Position.set_visible false preview_ctxt;
+        val _ = cmd preview_ctxt;
+        val print_modes = space_explode "," (Config.get print_ctxt modes) @ Latex.modes;
+      in Print_Mode.with_modes print_modes (fn () => cmd print_ctxt) () end;
 
 
 (* check_text *)
 
-fun eval_antiquote state source =
-  let
-    fun words (Antiquote.Text ss) = [(#1 (Symbol_Pos.range ss), Markup.words)]
-      | words (Antiquote.Antiq _) = [];
-
-    fun expand (Antiquote.Text ss) = Symbol_Pos.content ss
-      | expand (Antiquote.Antiq antiq) = eval_antiq state antiq;
-
-    val ants = Antiquote.read source;
-    val _ = Position.reports (maps words ants);
-  in implode (map expand ants) end;
-
 fun report_text source =
   Position.report (Input.pos_of source) (Markup.language_document (Input.is_delimited source));
 
 fun check_text source state =
  (report_text source;
   if Toplevel.is_skipped_proof state then ()
-  else ignore (eval_antiquote state source));
+  else
+    source
+    |> read_antiquotes state
+    |> List.app (ignore o eval_antiquote state));
 
 
 
@@ -216,7 +218,7 @@
   | Basic_Token of Token.T
   | Markup_Token of string * Input.source
   | Markup_Env_Token of string * Input.source
-  | Verbatim_Token of Input.source;
+  | Raw_Token of Input.source;
 
 
 fun basic_token pred (Basic_Token tok) = pred tok
@@ -230,22 +232,20 @@
 
 (* output token *)
 
-val output_text =
-  Symbol.trim_blanks #> Symbol.explode #> Latex.output_ctrl_symbols;
-
 fun output_token state =
   let
-    val eval = eval_antiquote state;
+    val make_text = read_antiquotes state #> map (eval_antiquote state) #> implode;
+    val output_text = make_text #> Symbol.explode #> Latex.output_ctrl_symbols;
     fun output No_Token = ""
       | output (Basic_Token tok) = Latex.output_token tok
       | output (Markup_Token (cmd, source)) =
-          "%\n\\isamarkup" ^ cmd ^ "{" ^ output_text (eval source) ^ "%\n}\n"
+          "%\n\\isamarkup" ^ cmd ^ "{" ^ output_text source ^ "%\n}\n"
       | output (Markup_Env_Token (cmd, source)) =
           "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
-          output_text (eval source) ^
+          output_text source ^
           "%\n\\end{isamarkup" ^ cmd ^ "}%\n"
-      | output (Verbatim_Token source) =
-          "%\n" ^ Symbol.trim_blanks (eval source) ^ "\n";
+      | output (Raw_Token source) =
+          "%\n" ^ output_text source ^ "\n";
   in output end;
 
 
@@ -422,7 +422,7 @@
       (ignored ||
         markup Keyword.is_document_heading Markup_Token markup_true ||
         markup Keyword.is_document_body Markup_Env_Token markup_true ||
-        markup Keyword.is_document_raw (Verbatim_Token o #2) "") >> single ||
+        markup Keyword.is_document_raw (Raw_Token o #2) "") >> single ||
       command ||
       (cmt || other) >> single;
 

--- a/src/Pure/Tools/rail.ML	Thu Oct 15 21:17:41 2015 +0200
+++ b/src/Pure/Tools/rail.ML	Thu Oct 15 22:25:57 2015 +0200
@@ -315,7 +315,7 @@
 
 fun output_rules state rules =
   let
-    val output_antiq = Thy_Output.eval_antiq state;
+    val output_antiq = Thy_Output.eval_antiquote state o Antiquote.Antiq;
     fun output_text b s =
       Output.output s
       |> b ? enclose "\\isakeyword{" "}"