14 

    15 

    16 (* re-definition of various ML antiquotations     *)

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

    18 (* they also write the code into a separate file  *)

    19 

    20 ML {*

    21 val filename = Attrib.setup_config_string @{binding "filename"} (K "File_Code.ML")

    22 *}

    23 

    24 

    25 ML {*

    26 fun write_file txt thy =

    27 let 

    28   val stream = Config.get_global thy filename

    29                |> TextIO.openAppend 

    30 in

    31   TextIO.output (stream, txt); 

    32   TextIO.flushOut stream;       (* needed ?*)

    33   TextIO.closeOut stream

    34 end

    35 *}

    36 

    37 ML {*

    38 fun write_file_ml_blk txt thy =

    39 let

    40   val pre  = implode ["\n", "ML ", "{", "*", "\n"]

    41   val post = implode ["\n", "*", "}", "\n"]

    42   val _ = write_file (enclose pre post txt) thy

    43 in

    44   thy

    45 end

    46 

    47 fun write_file_setup_blk txt thy =

    48 let

    49   val pre  = implode ["\n", "setup ", "{", "*", "\n"]

    50   val post = implode ["\n", "*", "}", "\n"]

    51   val _ = write_file (enclose pre post txt) thy

    52 in

    53   thy

    54 end

    55 

    56 fun write_file_lsetup_blk txt lthy =

    57 let

    58   val pre  = implode ["\n", "local_setup ", "{", "*", "\n"]

    59   val post = implode ["\n", "*", "}", "\n"]

    60   val _ = write_file (enclose pre post txt) (Proof_Context.theory_of lthy)

    61 in

    62   lthy

    63 end

    64 

    65 *}

    66 

    67 ML {*

    68 fun open_file name thy =

    69 let  

    70   val _ = tracing ("Open File: " ^ name)

    71   val _ = TextIO.openOut name

    72 in 

    73   Config.put_global filename name thy

    74 end

    75 *}

    76 

    77 ML {*

    78 fun open_file_with_prelude name txts thy =

    79 let 

    80   val thy' = open_file name thy 

    81   val _ = write_file (cat_lines txts) thy'

    82 in

    83   thy'

    84 end

    85 *}

    86 

    87 ML {*

    88 val _ =

    89   Outer_Syntax.command ("ML", Keyword.tag "TutorialML" Keyword.thy_decl)

    90     "ML text within theory or local theory"

    91     (Parse.ML_source >> (fn (txt, pos) =>

    92       Toplevel.generic_theory

    93         (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #>

    94           Local_Theory.propagate_ml_env #> Context.map_theory (write_file_ml_blk txt))))

    95 *}

    96 

    97 ML {*

    98 val _ =

    99   Outer_Syntax.command ("ML_prf", Keyword.tag "TutorialMLprf" Keyword.prf_decl) "ML text within proof"

   100     (Parse.ML_source >> (fn (txt, pos) =>

   101       Toplevel.proof (Proof.map_context (Context.proof_map

   102         (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> Proof.propagate_ml_env)));

   103 *}

   104 

   105 

   106 ML {*

   107 val _ =

   108   Outer_Syntax.command ("ML_val", Keyword.tag "TutorialML" Keyword.diag) "diagnostic ML text" 

   109     (Parse.ML_source >> Isar_Cmd.ml_diag true)

   110 *}

   111 

   112 ML {*

   113 val _ =

   114   Outer_Syntax.command ("setup", Keyword.tag_ml Keyword.thy_decl) "ML theory setup" 

   115       (Parse.ML_source >> (fn (txt, pos) => 

   116         (Toplevel.theory (Isar_Cmd.global_setup (txt, pos) #> write_file_setup_blk txt))))

   117 *}

   118 

   119 ML {*

   120 val _ =

   121   Outer_Syntax.local_theory ("local_setup", Keyword.tag_ml Keyword.thy_decl) "ML local theory setup" 

   122       (Parse.ML_source >> (fn (txt, pos) => 

   123          Isar_Cmd.local_setup (txt, pos) #> write_file_lsetup_blk txt));

   124 *}