--- a/src/Pure/Thy/thy_output.ML Fri Aug 24 11:32:12 2012 +0200
+++ b/src/Pure/Thy/thy_output.ML Fri Aug 24 12:35:39 2012 +0200
@@ -32,6 +32,7 @@
val modes: string list Unsynchronized.ref
val eval_antiq: Scan.lexicon -> Toplevel.state -> Symbol_Pos.T list * Position.range -> string
val eval_antiquote: Scan.lexicon -> Toplevel.state -> Symbol_Pos.text * Position.T -> string
+ val check_text: Symbol_Pos.text * Position.T -> Toplevel.state -> unit
val present_thy: Scan.lexicon -> (string -> string list) -> (markup -> string -> bool) ->
(Toplevel.transition * Toplevel.state) list -> Token.T list -> Buffer.T
val pretty_text: Proof.context -> string -> Pretty.T
@@ -202,6 +203,11 @@
end;
+fun check_text (txt, pos) state =
+ (Position.report pos Isabelle_Markup.doc_source;
+ ignore (eval_antiquote (#1 (Keyword.get_lexicons ())) state (txt, pos)));
+
+
(** present theory source **)