ML_Context.eval: produce antiquotation environment preferably in invisible context, to avoid displaced report messages from ML_Compiler;
--- 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
--- 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 ();