# HG changeset patch
# User wenzelm
# Date 1282761783 -7200
# Node ID 7f8bc335e203e10401feab5a25f48a7fa387ae4c
# Parent  7f69af169e879beb09cc8d79cba0e8b258337f0e
ML_Context.eval: produce antiquotation environment preferably in invisible context, to avoid displaced report messages from ML_Compiler;

diff -r 7f69af169e87 -r 7f8bc335e203 src/Pure/ML/ml_compiler_polyml-5.3.ML
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Wed Aug 25 18:46:22 2010 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Wed Aug 25 20:43:03 2010 +0200
@@ -44,13 +44,18 @@
 
 fun report_parse_tree depth space =
   let
+    val report_text =
+      (case Context.thread_data () of
+        SOME (Context.Proof ctxt) => Context_Position.report_text ctxt
+      | _ => Position.report_text);
+
     fun report_decl markup loc decl =
-      Position.report_text Markup.ML_ref (position_of loc)
+      report_text Markup.ML_ref (position_of loc)
         (Markup.markup (Markup.properties (Position.properties_of (position_of decl)) markup) "");
     fun report loc (PolyML.PTtype types) =
           PolyML.NameSpace.displayTypeExpression (types, depth, space)
           |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
-          |> Position.report_text Markup.ML_typing (position_of loc)
+          |> report_text Markup.ML_typing (position_of loc)
       | report loc (PolyML.PTdeclaredAt decl) = report_decl Markup.ML_def loc decl
       | report loc (PolyML.PTopenedAt decl) = report_decl Markup.ML_open loc decl
       | report loc (PolyML.PTstructureAt decl) = report_decl Markup.ML_struct loc decl
diff -r 7f69af169e87 -r 7f8bc335e203 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Wed Aug 25 18:46:22 2010 +0200
+++ b/src/Pure/ML/ml_context.ML	Wed Aug 25 20:43:03 2010 +0200
@@ -166,7 +166,9 @@
 fun eval verbose pos ants =
   let
     (*prepare source text*)
-    val ((env, body), env_ctxt) = eval_antiquotes (ants, pos) (Context.thread_data ());
+    val ((env, body), env_ctxt) =
+      eval_antiquotes (ants, pos) (Context.thread_data ())
+      ||> Option.map (Context.mapping I (Context_Position.set_visible false));
     val _ =
       if ! trace then tracing (cat_lines [ML_Lex.flatten env, ML_Lex.flatten body])
       else ();