# HG changeset patch
# User wenzelm
# Date 1218737621 -7200
# Node ID 4b79407825dab5a8c8f6b124bc2dda9b4e893b03
# Parent  1b46d9ec3788eee484ff7da8bc12eddfc1826abb
report doc_source;

diff -r 1b46d9ec3788 -r 4b79407825da src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Aug 14 20:13:40 2008 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Aug 14 20:13:41 2008 +0200
@@ -534,8 +534,9 @@
 
 (* markup commands *)
 
-fun check_text txt opt_node =
-  ignore (ThyOutput.eval_antiquote (#1 (OuterKeyword.get_lexicons ())) opt_node txt);
+fun check_text (txt, pos) opt_node =
+ (Position.report Markup.doc_source pos;
+  ignore (ThyOutput.eval_antiquote (#1 (OuterKeyword.get_lexicons ())) opt_node (txt, pos)));
 
 fun header_markup txt = Toplevel.keep (fn state =>
   if Toplevel.is_toplevel state then check_text txt NONE