src/Doc/Isar_Ref/Spec.thy
changeset 68276 cbee43ff4ceb
parent 67764 0f8cb5568b63
child 68278 23e12da0866c
     1.1 --- a/src/Doc/Isar_Ref/Spec.thy	Fri May 25 22:47:36 2018 +0200
     1.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Fri May 25 22:47:57 2018 +0200
     1.3 @@ -1058,6 +1058,7 @@
     1.4      @{command_def "ML_file_debug"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
     1.5      @{command_def "ML_file_no_debug"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
     1.6      @{command_def "ML"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
     1.7 +    @{command_def "ML_export"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
     1.8      @{command_def "ML_prf"} & : & \<open>proof \<rightarrow> proof\<close> \\
     1.9      @{command_def "ML_val"} & : & \<open>any \<rightarrow>\<close> \\
    1.10      @{command_def "ML_command"} & : & \<open>any \<rightarrow>\<close> \\
    1.11 @@ -1081,8 +1082,9 @@
    1.12        @@{command ML_file_debug} |
    1.13        @@{command ML_file_no_debug}) @{syntax name} ';'?
    1.14      ;
    1.15 -    (@@{command ML} | @@{command ML_prf} | @@{command ML_val} |
    1.16 -      @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text}
    1.17 +    (@@{command ML} | @@{command ML_export} | @@{command ML_prf} |
    1.18 +      @@{command ML_val} | @@{command ML_command} | @@{command setup} |
    1.19 +      @@{command local_setup}) @{syntax text}
    1.20      ;
    1.21      @@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
    1.22    \<close>}
    1.23 @@ -1103,10 +1105,16 @@
    1.24    \<^theory_text>\<open>ML_file_no_debug\<close> change the @{attribute ML_debugger} option locally while
    1.25    the given file is compiled.
    1.26  
    1.27 -  \<^descr> \<^theory_text>\<open>ML text\<close> is similar to \<^theory_text>\<open>ML_file\<close>, but evaluates directly the given
    1.28 -  \<open>text\<close>. Top-level ML bindings are stored within the (global or local) theory
    1.29 +  \<^descr> \<^theory_text>\<open>ML\<close> is similar to \<^theory_text>\<open>ML_file\<close>, but evaluates directly the given \<open>text\<close>.
    1.30 +  Top-level ML bindings are stored within the (global or local) theory
    1.31    context.
    1.32  
    1.33 +  \<^descr> \<^theory_text>\<open>ML_export\<close> is similar to \<^theory_text>\<open>ML\<close>, but the resulting toplevel bindings are
    1.34 +  exported to the global bootstrap environment of the ML process --- it has
    1.35 +  has a lasting effect that cannot be retracted. This allows ML evaluation
    1.36 +  without a formal theory context, e.g. for command-line tools via @{tool
    1.37 +  process} @{cite "isabelle-system"}.
    1.38 +
    1.39    \<^descr> \<^theory_text>\<open>ML_prf\<close> is analogous to \<^theory_text>\<open>ML\<close> but works within a proof context.
    1.40    Top-level ML bindings are stored within the proof context in a purely
    1.41    sequential fashion, disregarding the nested proof structure. ML bindings