# HG changeset patch
# User wenzelm
# Date 1214408316 -7200
# Node ID cb052da62549a40bace34b4586732f0948bd0063
# Parent  a9d738d201748a54eaf67c56514239533ed97d31
moved global keywords from OuterSyntax to OuterKeyword, tuned interfaces;
moved check_text here;

diff -r a9d738d20174 -r cb052da62549 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Jun 25 17:38:35 2008 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Jun 25 17:38:36 2008 +0200
@@ -634,13 +634,16 @@
 
 (* markup commands *)
 
+fun check_text s state =
+  (ThyOutput.eval_antiquote (#1 (OuterKeyword.get_lexicons ())) state s; ());
+
 fun add_header s = Toplevel.keep' (fn int => fn state =>
   (if Toplevel.is_toplevel state then () else raise Toplevel.UNDEF;
-   if int then OuterSyntax.check_text s NONE else ()));
+   if int then check_text s NONE else ()));
 
 local
 
-fun present _ txt true node = OuterSyntax.check_text txt (SOME node)
+fun present _ txt true node = check_text txt (SOME node)
   | present f (s, _) false node = Context.setmp_thread_data
       (try (Toplevel.cases_node I (Context.Proof o Proof.context_of)) node) f s;