5   "chunks.ML"

     5   "chunks.ML"

     6   "antiquote_setup.ML"

     6   "antiquote_setup.ML"

     7 begin

     7 begin

     8 

     8 

     9 (* to have a special tag for text enclosed in ML *)

     9 (* to have a special tag for text enclosed in ML *)

    10 ML {*

    11 ML {*

    11 

    12 

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

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

    13       Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy)

    14       Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy)

    14   | propagate_env context = context

    15   | propagate_env context = context

    35   (OuterKeyword.tag "TutorialML" OuterKeyword.diag)

    36   (OuterKeyword.tag "TutorialML" OuterKeyword.diag)

    36     (OuterParse.ML_source >> IsarCmd.ml_diag true)

    37     (OuterParse.ML_source >> IsarCmd.ml_diag true)

    37 

    38 

    38 *}

    39 *}

    39 

    40 

    41 end

    41 end