--- a/NEWS Sat May 26 08:36:09 2018 +0100
+++ b/NEWS Sat May 26 08:36:19 2018 +0100
@@ -358,6 +358,11 @@
* Operation Export.export emits theory exports (arbitrary blobs), which
are stored persistently in the session build database.
+* Command 'ML_export' exports ML toplevel bindings to the global
+bootstrap environment of the ML process. This allows ML evaluation
+without a formal theory context, e.g. in command-line tools like
+"isabelle process".
+
*** System ***
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy Sat May 26 08:36:09 2018 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Sat May 26 08:36:19 2018 +0100
@@ -281,12 +281,14 @@
@{syntax_def mixfix}: '('
(@{syntax template} prios? @{syntax nat}? |
(@'infix' | @'infixl' | @'infixr') @{syntax template} @{syntax nat} |
- @'binder' @{syntax template} prios? @{syntax nat} |
+ @'binder' @{syntax template} prio? @{syntax nat} |
@'structure') ')'
;
@{syntax template}: string
;
prios: '[' (@{syntax nat} + ',') ']'
+ ;
+ prio: '[' @{syntax nat} ']'
\<close>}
The string given as \<open>template\<close> may include literal text, spacing, blocks,
--- a/src/Doc/Isar_Ref/Spec.thy Sat May 26 08:36:09 2018 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy Sat May 26 08:36:19 2018 +0100
@@ -1058,6 +1058,7 @@
@{command_def "ML_file_debug"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
@{command_def "ML_file_no_debug"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
@{command_def "ML"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
+ @{command_def "ML_export"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
@{command_def "ML_prf"} & : & \<open>proof \<rightarrow> proof\<close> \\
@{command_def "ML_val"} & : & \<open>any \<rightarrow>\<close> \\
@{command_def "ML_command"} & : & \<open>any \<rightarrow>\<close> \\
@@ -1081,8 +1082,9 @@
@@{command ML_file_debug} |
@@{command ML_file_no_debug}) @{syntax name} ';'?
;
- (@@{command ML} | @@{command ML_prf} | @@{command ML_val} |
- @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text}
+ (@@{command ML} | @@{command ML_export} | @@{command ML_prf} |
+ @@{command ML_val} | @@{command ML_command} | @@{command setup} |
+ @@{command local_setup}) @{syntax text}
;
@@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
\<close>}
@@ -1103,10 +1105,16 @@
\<^theory_text>\<open>ML_file_no_debug\<close> change the @{attribute ML_debugger} option locally while
the given file is compiled.
- \<^descr> \<^theory_text>\<open>ML text\<close> is similar to \<^theory_text>\<open>ML_file\<close>, but evaluates directly the given
- \<open>text\<close>. Top-level ML bindings are stored within the (global or local) theory
+ \<^descr> \<^theory_text>\<open>ML\<close> is similar to \<^theory_text>\<open>ML_file\<close>, but evaluates directly the given \<open>text\<close>.
+ Top-level ML bindings are stored within the (global or local) theory
context.
+ \<^descr> \<^theory_text>\<open>ML_export\<close> is similar to \<^theory_text>\<open>ML\<close>, but the resulting toplevel bindings are
+ exported to the global bootstrap environment of the ML process --- it has
+ a lasting effect that cannot be retracted. This allows ML evaluation
+ without a formal theory context, e.g. for command-line tools via @{tool
+ process} @{cite "isabelle-system"}.
+
\<^descr> \<^theory_text>\<open>ML_prf\<close> is analogous to \<^theory_text>\<open>ML\<close> but works within a proof context.
Top-level ML bindings are stored within the proof context in a purely
sequential fashion, disregarding the nested proof structure. ML bindings
--- a/src/Doc/System/Environment.thy Sat May 26 08:36:09 2018 +0100
+++ b/src/Doc/System/Environment.thy Sat May 26 08:36:19 2018 +0100
@@ -365,7 +365,7 @@
\<close>
-subsubsection \<open>Example\<close>
+subsubsection \<open>Examples\<close>
text \<open>
The subsequent example retrieves the \<^verbatim>\<open>Main\<close> theory value from the theory
@@ -375,6 +375,12 @@
Observe the delicate quoting rules for the GNU bash shell vs.\ ML. The
Isabelle/ML and Scala libraries provide functions for that, but here we need
to do it manually.
+
+ \<^medskip>
+ This is how to invoke a function body with proper return code and printing
+ of errors, and without printing of a redundant \<^verbatim>\<open>val it = (): unit\<close> result:
+ @{verbatim [display] \<open>isabelle process -e 'Command_Line.tool0 (fn () => writeln "OK")'\<close>}
+ @{verbatim [display] \<open>isabelle process -e 'Command_Line.tool0 (fn () => error "Bad")'\<close>}
\<close>
--- a/src/HOL/Decision_Procs/MIR.thy Sat May 26 08:36:09 2018 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy Sat May 26 08:36:19 2018 +0100
@@ -999,7 +999,7 @@
using real_of_int_div[OF gpdd] th2 gp0 by simp
finally have "?lhs = Inum bs t / real_of_int n" by simp
then have ?thesis using nnz g1 g'1 by (simp add: simp_num_pair_def) }
- ultimately have ?thesis by blast }
+ ultimately have ?thesis by auto }
ultimately have ?thesis by blast }
ultimately show ?thesis by blast
qed
@@ -1031,7 +1031,7 @@
have "n div ?g' >0" by simp
hence ?thesis using assms g1 g'1
by(auto simp add: simp_num_pair_def Let_def reducecoeffh_numbound0)}
- ultimately have ?thesis by blast }
+ ultimately have ?thesis by auto }
ultimately have ?thesis by blast }
ultimately show ?thesis by blast
qed
@@ -1171,7 +1171,7 @@
using rdvd_reduce[OF gpdd gpdgp g'p, where t="?t", simplified div_self[OF gp0]]
th2[symmetric] by simp
finally have ?thesis by simp }
- ultimately have ?thesis by blast
+ ultimately have ?thesis by auto
}
ultimately show ?thesis by blast
qed
@@ -3397,7 +3397,7 @@
((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (?ff (p,n,s)))))"
- using int_cases[rule_format] by blast
+ by (auto split: if_splits)
also have "\<dots> =
((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set [(p,0,Floor s)])) Un
(UNION {(p,n,s). (p,n,s)\<in> ?SS a\<and>n>0} (\<lambda>(p,n,s). set(map(?f(p,n,s)) [0..n]))) Un
@@ -3411,12 +3411,14 @@
also have "\<dots> =
((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un
(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {0 .. n}})) Un
- (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {n .. 0}})))" by blast
+ (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {n .. 0}})))"
+ by blast
finally
have FS: "?SS (Floor a) =
((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). {(p,0,Floor s)})) Un
(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {0 .. n}})) Un
- (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {n .. 0}})))" by blast
+ (UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). {?f(p,n,s) j| j. j\<in> {n .. 0}})))"
+ by blast
show ?case
proof(simp only: FS, clarsimp simp del: Ifm.simps Inum.simps, -)
fix p n s
@@ -3552,7 +3554,7 @@
((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (?ff (p,n,s)))) Un
(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n<0} (\<lambda> (p,n,s). set (?ff (p,n,s)))))"
- using int_cases[rule_format] by blast
+ by (auto split: if_splits)
also have "\<dots> =
((UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n=0} (\<lambda> (p,n,s). set [(p,0,Floor s)])) Un
(UNION {(p,n,s). (p,n,s) \<in> ?SS a \<and> n>0} (\<lambda> (p,n,s). set (map (?f(p,n,s)) [0..n]))) Un
--- a/src/HOL/GCD.thy Sat May 26 08:36:09 2018 +0100
+++ b/src/HOL/GCD.thy Sat May 26 08:36:19 2018 +0100
@@ -1287,7 +1287,7 @@
by (simp add: t_def)
qed
-lemma gcd_eq_1_imp_coprime:
+lemma gcd_eq_1_imp_coprime [dest!]:
"coprime a b" if "gcd a b = 1"
proof (rule coprimeI)
fix c
--- a/src/Pure/Isar/element.ML Sat May 26 08:36:09 2018 +0100
+++ b/src/Pure/Isar/element.ML Sat May 26 08:36:19 2018 +0100
@@ -171,9 +171,8 @@
| prt_mixfix mx = [Pretty.brk 2, Mixfix.pretty_mixfix mx];
fun prt_fix (x, SOME T, mx) = Pretty.block (prt_name (Binding.name_of x) :: Pretty.str " ::" ::
- Pretty.brk 1 :: prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
- | prt_fix (x, NONE, mx) = Pretty.block (prt_name (Binding.name_of x) ::
- Pretty.brk 1 :: prt_mixfix mx);
+ Pretty.brk 1 :: prt_typ T :: prt_mixfix mx)
+ | prt_fix (x, NONE, mx) = Pretty.block (prt_name (Binding.name_of x) :: prt_mixfix mx);
fun prt_constrain (x, T) = prt_fix (Binding.name x, SOME T, NoSyn);
fun prt_asm (a, ts) =
--- a/src/Pure/ML/ml_env.ML Sat May 26 08:36:09 2018 +0100
+++ b/src/Pure/ML/ml_env.ML Sat May 26 08:36:19 2018 +0100
@@ -13,6 +13,8 @@
val add_breakpoints: (serial * (bool Unsynchronized.ref * Thread_Position.T)) list -> unit
val init_bootstrap: Context.generic -> Context.generic
val SML_environment: bool Config.T
+ val set_bootstrap: bool -> Context.generic -> Context.generic
+ val restore_bootstrap: Context.generic -> Context.generic -> Context.generic
val add_name_space: {SML: bool} -> ML_Name_Space.T -> Context.generic -> Context.generic
val make_name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
val context: ML_Compiler0.context
@@ -130,6 +132,12 @@
in (val2, type1, fixity1, structure2, signature2, functor1) end);
in make_data (bootstrap, tables, sml_tables', breakpoints) end);
+fun set_bootstrap bootstrap =
+ Env.map (fn {tables, sml_tables, breakpoints, ...} =>
+ make_data (bootstrap, tables, sml_tables, breakpoints));
+
+val restore_bootstrap = set_bootstrap o #bootstrap o Env.get;
+
fun add_name_space {SML} (space: ML_Name_Space.T) =
Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
let
--- a/src/Pure/Pure.thy Sat May 26 08:36:09 2018 +0100
+++ b/src/Pure/Pure.thy Sat May 26 08:36:19 2018 +0100
@@ -23,7 +23,7 @@
and "external_file" "bibtex_file" :: thy_load
and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML"
and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
- and "SML_import" "SML_export" :: thy_decl % "ML"
+ and "SML_import" "SML_export" "ML_export" :: thy_decl % "ML"
and "ML_prf" :: prf_decl % "proof" (* FIXME % "ML" ?? *)
and "ML_val" "ML_command" :: diag % "ML"
and "simproc_setup" :: thy_decl % "ML"
@@ -191,6 +191,18 @@
end));
val _ =
+ Outer_Syntax.command ("ML_export", \<^here>)
+ "ML text within theory or local theory, and export to bootstrap environment"
+ (Parse.ML_source >> (fn source =>
+ Toplevel.generic_theory (fn context =>
+ context
+ |> ML_Env.set_bootstrap true
+ |> ML_Context.exec (fn () =>
+ ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source)
+ |> ML_Env.restore_bootstrap context
+ |> Local_Theory.propagate_ml_env)));
+
+val _ =
Outer_Syntax.command \<^command_keyword>\<open>ML_prf\<close> "ML text within proof"
(Parse.ML_source >> (fn source =>
Toplevel.proof (Proof.map_context (Context.proof_map
--- a/src/Pure/Syntax/mixfix.ML Sat May 26 08:36:09 2018 +0100
+++ b/src/Pure/Syntax/mixfix.ML Sat May 26 08:36:19 2018 +0100
@@ -97,12 +97,18 @@
fun pretty_mixfix NoSyn = Pretty.str ""
| pretty_mixfix (Mixfix (s, ps, p, _)) =
- parens (Pretty.breaks [quoted s, brackets (Pretty.commas (map int ps)), int p])
+ parens
+ (Pretty.breaks
+ (quoted s ::
+ (if null ps then [] else [brackets (Pretty.commas (map int ps))]) @
+ (if p = 1000 then [] else [int p])))
| pretty_mixfix (Infix (s, p, _)) = parens (Pretty.breaks [keyword "infix", quoted s, int p])
| pretty_mixfix (Infixl (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
- | pretty_mixfix (Infixr (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
+ | pretty_mixfix (Infixr (s, p, _)) = parens (Pretty.breaks [keyword "infixr", quoted s, int p])
| pretty_mixfix (Binder (s, p1, p2, _)) =
- parens (Pretty.breaks [keyword "binder", quoted s, brackets [int p1], int p2])
+ parens
+ (Pretty.breaks
+ ([keyword "binder", quoted s] @ (if p1 = p2 then [] else [brackets [int p1]]) @ [int p2]))
| pretty_mixfix (Structure _) = parens [keyword "structure"];
end;