Re: [isabelle] Export files generated by code_export to hard drive



> Am 30.04.2019 um 14:14 schrieb Makarius <makarius at sketis.net>:
> 
> Since export_code uses Generated_Files internally (apart from Export),
> you could experiment with Generated_Files.write_file or better use the
> command 'compile_generated_files' to turn the individual sources into
> some derived artifact. Thus the shell programming happens in Isabelle/ML.

Thanks for the pointer. For now I use the following Isabelle/ML script:

====================
theory Scratch
  imports Main
begin

export_code binomial in Haskell

ML ‹
val gen_files = Generated_Files.get_files (Proof_Context.theory_of @{context})
val output_dir = Path.explode "~/output_hs/"
›

(*
(* The next line creates output_dir and writes the files there *)
ML ‹map (Generated_Files.write_file write_dir) gen_files›
*)

end
====================



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.