# HG changeset patch
# User wenzelm
# Date 1440752966 -7200
# Node ID f6f2959bed672f3344067b1d0396de362faa0213
# Parent  5fa9962e6c389cb0dec67dff301859fe86f431d0
clarified language context, e.g. relevant for symbols;

diff -r 5fa9962e6c38 -r f6f2959bed67 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Fri Aug 28 10:50:48 2015 +0200
+++ b/src/Pure/Thy/thy_output.ML	Fri Aug 28 11:09:26 2015 +0200
@@ -24,6 +24,7 @@
   val boolean: string -> bool
   val integer: string -> int
   val eval_antiq: Toplevel.state -> Antiquote.antiq -> 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
   val pretty_text: Proof.context -> string -> Pretty.T
@@ -194,8 +195,11 @@
     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 =
- (Position.report (Input.pos_of source) (Markup.language_document (Input.is_delimited source));
+ (report_text source;
   if Toplevel.is_skipped_proof state then ()
   else ignore (eval_antiquote state source));
 
diff -r 5fa9962e6c38 -r f6f2959bed67 src/Pure/pure_syn.ML
--- a/src/Pure/pure_syn.ML	Fri Aug 28 10:50:48 2015 +0200
+++ b/src/Pure/pure_syn.ML	Fri Aug 28 11:09:26 2015 +0200
@@ -43,7 +43,7 @@
 
 val _ =
   Outer_Syntax.command ("text_raw", @{here}) "raw LaTeX text"
-    (Parse.document_source >> K (Toplevel.keep (fn _ => ())));
+    (Parse.document_source >> (fn s => Toplevel.keep (fn _ => Thy_Output.report_text s)));
 
 val _ =
   Outer_Syntax.command ("theory", @{here}) "begin theory"