2 imports Main LaTeXsugar

     2 imports Main LaTeXsugar

     3 uses

     3 uses

     4   ("output_tutorial.ML")

     4   ("output_tutorial.ML")

     5   ("antiquote_setup.ML")

     5   ("antiquote_setup.ML")

     6 begin

     6 begin

     7 

    11 

     8 (* rebinding of writeln and tracing so that it can *)

    12 (* rebinding of writeln and tracing so that it can *)

     9 (* be compared in intiquotations                   *)

    13 (* be compared in intiquotations                   *)

    10 ML {* 

    14 ML {* 

    11 fun writeln s = (Output.writeln s; s)

    15 fun writeln s = (Output.writeln s; s)

    84 end

    88 end

    85 *}

    89 *}

    86 

    90 

    87 ML {*

    91 ML {*

    88 fun propagate_env (context as Context.Proof lthy) =

    92 fun propagate_env (context as Context.Proof lthy) =

    90   | propagate_env context = context

    94   | propagate_env context = context

    91 

    95 

    92 fun propagate_env_prf prf = Proof.map_contexts

    96 fun propagate_env_prf prf = Proof.map_contexts

    93   (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf

    97   (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf

    94 *}

    98 *}