[isabelle] Isabelle2019-RC0: generate_file - documentation and behavior



Hello,

in NEWS, it says

   The ML function Generate_File.generate writes all generated files from a
   given theory to the file-system, e.g. a temporary directory where some
   external compiler is applied.

This function does not exist. I think it should say Generated_Files.write_files.

Also, a file generated with generate_file does not show up in jEdit in the file browser while a file generated with export_code does. (Even though both of them show up using Generated_Files.get_files.) I don't know if this is the expected behavior.

A small example is attached.

Best wishes,
Dominique.


theory Scratch
  imports Main
begin

export_code 1 in SML file_prefix "hello"

generate_file "Pure.hs" = \<open>
  module Isabelle.Pure where
    allConst, impConst, eqConst :: String
    allConst = \<open>\<^const_name>\<open>Pure.all\<close>\<close>
    impConst = \<open>\<^const_name>\<open>Pure.imp\<close>\<close>
    eqConst = \<open>\<^const_name>\<open>Pure.eq\<close>\<close>
  \<close>

ML \<open>
Generated_Files.get_files \<^theory>
|> map #path
\<close>

end


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