clarified language context, e.g. relevant for symbols;
--- 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));
--- 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"