retain compile-time context visibility, which is particularly important for "apply tactic";
authorwenzelm
Mon Jul 15 19:23:19 2013 +0200 (2013-07-15)
changeset 526636e71d43775e5
parent 52660 7f7311d04727
child 52664 e99a0a43720b
retain compile-time context visibility, which is particularly important for "apply tactic";
src/Pure/ML/ml_context.ML
     1.1 --- a/src/Pure/ML/ml_context.ML	Mon Jul 15 15:50:39 2013 +0200
     1.2 +++ b/src/Pure/ML/ml_context.ML	Mon Jul 15 19:23:19 2013 +0200
     1.3 @@ -131,9 +131,12 @@
     1.4    >> (fn ((x, pos), y) => Args.src ((x, y), pos));
     1.5  
     1.6  val begin_env0 = ML_Lex.tokenize "structure Isabelle =\nstruct\n";
     1.7 -val begin_env =
     1.8 +
     1.9 +fun begin_env visible =
    1.10    ML_Lex.tokenize
    1.11 -    "structure Isabelle =\nstruct\nval ML_context = ML_Context.the_local_context ();\n";
    1.12 +    ("structure Isabelle =\nstruct\n\
    1.13 +     \val ML_context = Context_Position.set_visible " ^ Bool.toString visible ^
    1.14 +     " (ML_Context.the_local_context ());\n");
    1.15  
    1.16  val end_env = ML_Lex.tokenize "end;";
    1.17  val reset_env = ML_Lex.tokenize "structure Isabelle = struct end";
    1.18 @@ -142,7 +145,12 @@
    1.19  
    1.20  fun eval_antiquotes (ants, pos) opt_context =
    1.21    let
    1.22 +    val visible =
    1.23 +      (case opt_context of
    1.24 +        SOME (Context.Proof ctxt) => Context_Position.is_visible ctxt
    1.25 +      | _ => true);
    1.26      val opt_ctxt = Option.map (Context.Proof o Context.proof_of) opt_context;
    1.27 +
    1.28      val ((ml_env, ml_body), opt_ctxt') =
    1.29        if forall Antiquote.is_text ants
    1.30        then ((begin_env0, map (fn Antiquote.Text tok => tok) ants), opt_ctxt)
    1.31 @@ -171,8 +179,9 @@
    1.32                  (no_decl, (Stack.pop scope, background));
    1.33  
    1.34            val (decls, (_, ctxt')) = fold_map expand ants (Stack.init ctxt, ctxt);
    1.35 -          val (ml_env, ml_body) = decls |> map (fn decl => decl ctxt') |> split_list |> pairself flat;
    1.36 -        in ((begin_env @ ml_env, ml_body), SOME (Context.Proof ctxt')) end;
    1.37 +          val (ml_env, ml_body) =
    1.38 +            decls |> map (fn decl => decl ctxt') |> split_list |> pairself flat;
    1.39 +        in ((begin_env visible @ ml_env, ml_body), SOME (Context.Proof ctxt')) end;
    1.40    in ((ml_env @ end_env, ml_body), opt_ctxt') end;
    1.41  
    1.42  val trace_raw = Config.declare "ML_trace" (fn _ => Config.Bool false);