more documentation;
authorwenzelm
Fri May 10 10:41:38 2019 +0200 (4 months ago)
changeset 7026022cfcfcadd8b
parent 70259 42f73412fa06
child 70261 efbdfcaa6258
more documentation;
NEWS
src/Doc/Isar_Ref/Spec.thy
     1.1 --- a/NEWS	Thu May 09 16:48:25 2019 +0200
     1.2 +++ b/NEWS	Fri May 10 10:41:38 2019 +0200
     1.3 @@ -317,25 +317,9 @@
     1.4  See also commands 'export_generated_files' and 'compile_generated_files'
     1.5  to use the results.
     1.6  
     1.7 -* ML evaluation (notably via commands 'ML' and 'ML_file') is subject to
     1.8 +* ML evaluation (notably via command 'ML' or 'ML_file') is subject to
     1.9  option ML_environment to select a named environment, such as "Isabelle"
    1.10 -for Isabelle/ML, or "SML" for official Standard ML. It is also possible
    1.11 -to move toplevel bindings between environments, using a notation with
    1.12 -">" as separator. For example:
    1.13 -
    1.14 -  declare [[ML_environment = "Isabelle>SML"]]
    1.15 -  ML \<open>val println = writeln\<close>
    1.16 -
    1.17 -  declare [[ML_environment = "SML"]]
    1.18 -  ML \<open>println "test"\<close>
    1.19 -
    1.20 -  declare [[ML_environment = "Isabelle"]]
    1.21 -  ML \<open>println\<close>  \<comment> \<open>not present\<close>
    1.22 -
    1.23 -The Isabelle/ML function ML_Env.setup defines new ML environments. This
    1.24 -is useful to incorporate big SML projects in an isolated name space, and
    1.25 -potentially with variations on ML syntax (existing ML_Env.SML_operations
    1.26 -observes the official standard).
    1.27 +for Isabelle/ML, or "SML" for official Standard ML.
    1.28  
    1.29  * ML antiquotation @{master_dir} refers to the master directory of the
    1.30  underlying theory, i.e. the directory of the theory file.
     2.1 --- a/src/Doc/Isar_Ref/Spec.thy	Thu May 09 16:48:25 2019 +0200
     2.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Fri May 10 10:41:38 2019 +0200
     2.3 @@ -1071,6 +1071,7 @@
     2.4      @{attribute_def ML_debugger} & : & \<open>attribute\<close> & default \<open>false\<close> \\
     2.5      @{attribute_def ML_exception_trace} & : & \<open>attribute\<close> & default \<open>false\<close> \\
     2.6      @{attribute_def ML_exception_debugger} & : & \<open>attribute\<close> & default \<open>false\<close> \\
     2.7 +    @{attribute_def ML_environment} & : & \<open>attribute\<close> & default \<open>Isabelle\<close> \\
     2.8    \end{tabular}
     2.9  
    2.10    \<^rail>\<open>
    2.11 @@ -1185,8 +1186,37 @@
    2.12    the Poly/ML debugger, at the cost of extra compile-time and run-time
    2.13    overhead. Relevant ML modules need to be compiled beforehand with debugging
    2.14    enabled, see @{attribute ML_debugger} above.
    2.15 +
    2.16 +  \<^descr> @{attribute ML_environment} determines the named ML environment for
    2.17 +  toplevel declarations, e.g.\ in command \<^theory_text>\<open>ML\<close> or \<^theory_text>\<open>ML_file\<close>. The following
    2.18 +  ML environments are predefined in Isabelle/Pure:
    2.19 +
    2.20 +    \<^item> \<open>Isabelle\<close> for Isabelle/ML. It contains all modules of Isabelle/Pure and
    2.21 +    further add-ons, e.g. material from Isabelle/HOL.
    2.22 +
    2.23 +    \<^item> \<open>SML\<close> for official Standard ML. It contains only the initial basis
    2.24 +    according to \<^url>\<open>http://sml-family.org/Basis/overview.html\<close>.
    2.25 +
    2.26 +  The Isabelle/ML function \<^ML>\<open>ML_Env.setup\<close> defines a new ML environment.
    2.27 +  This is useful to incorporate big SML projects in an isolated name space,
    2.28 +  possibly with variations on ML syntax; the existing setup of
    2.29 +  \<^ML>\<open>ML_Env.SML_operations\<close> follows the official standard.
    2.30 +
    2.31 +  It is also possible to move toplevel bindings between ML environments, using
    2.32 +  a notation with ``\<open>>\<close>'' as separator. For example:
    2.33  \<close>
    2.34  
    2.35 +(*<*)experiment begin(*>*)
    2.36 +        declare [[ML_environment = "Isabelle>SML"]]
    2.37 +        ML \<open>val println = writeln\<close>
    2.38 +
    2.39 +        declare [[ML_environment = "SML"]]
    2.40 +        ML \<open>println "test"\<close>
    2.41 +
    2.42 +        declare [[ML_environment = "Isabelle"]]
    2.43 +        ML \<open>ML \<open>println\<close> (*bad*) handle ERROR msg => warning msg\<close>
    2.44 +(*<*)end(*>*)
    2.45 +
    2.46  
    2.47  section \<open>Generated files and external files\<close>
    2.48