retain compile-time context visibility, which is particularly important for "apply tactic";

--- a/src/Pure/ML/ml_context.ML	Mon Jul 15 15:50:39 2013 +0200
+++ b/src/Pure/ML/ml_context.ML	Mon Jul 15 19:23:19 2013 +0200
@@ -131,9 +131,12 @@
   >> (fn ((x, pos), y) => Args.src ((x, y), pos));
 
 val begin_env0 = ML_Lex.tokenize "structure Isabelle =\nstruct\n";
-val begin_env =
+
+fun begin_env visible =
   ML_Lex.tokenize
-    "structure Isabelle =\nstruct\nval ML_context = ML_Context.the_local_context ();\n";
+    ("structure Isabelle =\nstruct\n\
+     \val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^
+     " (ML_Context.the_local_context ());\n");
 
 val end_env = ML_Lex.tokenize "end;";
 val reset_env = ML_Lex.tokenize "structure Isabelle = struct end";
@@ -142,7 +145,12 @@
 
 fun eval_antiquotes (ants, pos) opt_context =
   let
+    val visible =
+      (case opt_context of
+        SOME (Context.Proof ctxt) => Context_Position.is_visible ctxt
+      | _ => true);
     val opt_ctxt = Option.map (Context.Proof o Context.proof_of) opt_context;
+
     val ((ml_env, ml_body), opt_ctxt') =
       if forall Antiquote.is_text ants
       then ((begin_env0, map (fn Antiquote.Text tok => tok) ants), opt_ctxt)
@@ -171,8 +179,9 @@
                 (no_decl, (Stack.pop scope, background));
 
           val (decls, (_, ctxt')) = fold_map expand ants (Stack.init ctxt, ctxt);
-          val (ml_env, ml_body) = decls |> map (fn decl => decl ctxt') |> split_list |> pairself flat;
-        in ((begin_env @ ml_env, ml_body), SOME (Context.Proof ctxt')) end;
+          val (ml_env, ml_body) =
+            decls |> map (fn decl => decl ctxt') |> split_list |> pairself flat;
+        in ((begin_env visible @ ml_env, ml_body), SOME (Context.Proof ctxt')) end;
   in ((ml_env @ end_env, ml_body), opt_ctxt') end;
 
 val trace_raw = Config.declare "ML_trace" (fn _ => Config.Bool false);