# HG changeset patch # User paulson # Date 1527320179 -3600 # Node ID 9d93b13f07cea92a1cd170679be0023b30cb2def # Parent 23e12da0866cd32b51a9f9bf1a458e82ee7e9d4a# Parent 5e4e006f9552666c7b814b72d68c42052c451f9e merged diff -r 5e4e006f9552 -r 9d93b13f07ce NEWS --- 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 *** diff -r 5e4e006f9552 -r 9d93b13f07ce src/Doc/Isar_Ref/Inner_Syntax.thy --- 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} ']' \} The string given as \template\ may include literal text, spacing, blocks, diff -r 5e4e006f9552 -r 9d93b13f07ce src/Doc/Isar_Ref/Spec.thy --- 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"} & : & \local_theory \ local_theory\ \\ @{command_def "ML_file_no_debug"} & : & \local_theory \ local_theory\ \\ @{command_def "ML"} & : & \local_theory \ local_theory\ \\ + @{command_def "ML_export"} & : & \local_theory \ local_theory\ \\ @{command_def "ML_prf"} & : & \proof \ proof\ \\ @{command_def "ML_val"} & : & \any \\ \\ @{command_def "ML_command"} & : & \any \\ \\ @@ -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}? \} @@ -1103,10 +1105,16 @@ \<^theory_text>\ML_file_no_debug\ change the @{attribute ML_debugger} option locally while the given file is compiled. - \<^descr> \<^theory_text>\ML text\ is similar to \<^theory_text>\ML_file\, but evaluates directly the given - \text\. Top-level ML bindings are stored within the (global or local) theory + \<^descr> \<^theory_text>\ML\ is similar to \<^theory_text>\ML_file\, but evaluates directly the given \text\. + Top-level ML bindings are stored within the (global or local) theory context. + \<^descr> \<^theory_text>\ML_export\ is similar to \<^theory_text>\ML\, 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>\ML_prf\ is analogous to \<^theory_text>\ML\ 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 diff -r 5e4e006f9552 -r 9d93b13f07ce src/Doc/System/Environment.thy --- 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 @@ \ -subsubsection \Example\ +subsubsection \Examples\ text \ The subsequent example retrieves the \<^verbatim>\Main\ 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>\val it = (): unit\ result: + @{verbatim [display] \isabelle process -e 'Command_Line.tool0 (fn () => writeln "OK")'\} + @{verbatim [display] \isabelle process -e 'Command_Line.tool0 (fn () => error "Bad")'\} \ diff -r 5e4e006f9552 -r 9d93b13f07ce src/HOL/Decision_Procs/MIR.thy --- 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) \ ?SS a \ n=0} (\ (p,n,s). set (?ff (p,n,s)))) Un (UNION {(p,n,s). (p,n,s) \ ?SS a \ n>0} (\ (p,n,s). set (?ff (p,n,s)))) Un (UNION {(p,n,s). (p,n,s) \ ?SS a \ n<0} (\ (p,n,s). set (?ff (p,n,s)))))" - using int_cases[rule_format] by blast + by (auto split: if_splits) also have "\ = ((UNION {(p,n,s). (p,n,s) \ ?SS a \ n=0} (\ (p,n,s). set [(p,0,Floor s)])) Un (UNION {(p,n,s). (p,n,s)\ ?SS a\n>0} (\(p,n,s). set(map(?f(p,n,s)) [0..n]))) Un @@ -3411,12 +3411,14 @@ also have "\ = ((UNION {(p,n,s). (p,n,s) \ ?SS a \ n=0} (\ (p,n,s). {(p,0,Floor s)})) Un (UNION {(p,n,s). (p,n,s) \ ?SS a \ n>0} (\ (p,n,s). {?f(p,n,s) j| j. j\ {0 .. n}})) Un - (UNION {(p,n,s). (p,n,s) \ ?SS a \ n<0} (\ (p,n,s). {?f(p,n,s) j| j. j\ {n .. 0}})))" by blast + (UNION {(p,n,s). (p,n,s) \ ?SS a \ n<0} (\ (p,n,s). {?f(p,n,s) j| j. j\ {n .. 0}})))" + by blast finally have FS: "?SS (Floor a) = ((UNION {(p,n,s). (p,n,s) \ ?SS a \ n=0} (\ (p,n,s). {(p,0,Floor s)})) Un (UNION {(p,n,s). (p,n,s) \ ?SS a \ n>0} (\ (p,n,s). {?f(p,n,s) j| j. j\ {0 .. n}})) Un - (UNION {(p,n,s). (p,n,s) \ ?SS a \ n<0} (\ (p,n,s). {?f(p,n,s) j| j. j\ {n .. 0}})))" by blast + (UNION {(p,n,s). (p,n,s) \ ?SS a \ n<0} (\ (p,n,s). {?f(p,n,s) j| j. j\ {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) \ ?SS a \ n=0} (\ (p,n,s). set (?ff (p,n,s)))) Un (UNION {(p,n,s). (p,n,s) \ ?SS a \ n>0} (\ (p,n,s). set (?ff (p,n,s)))) Un (UNION {(p,n,s). (p,n,s) \ ?SS a \ n<0} (\ (p,n,s). set (?ff (p,n,s)))))" - using int_cases[rule_format] by blast + by (auto split: if_splits) also have "\ = ((UNION {(p,n,s). (p,n,s) \ ?SS a \ n=0} (\ (p,n,s). set [(p,0,Floor s)])) Un (UNION {(p,n,s). (p,n,s) \ ?SS a \ n>0} (\ (p,n,s). set (map (?f(p,n,s)) [0..n]))) Un diff -r 5e4e006f9552 -r 9d93b13f07ce src/HOL/GCD.thy --- 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 diff -r 5e4e006f9552 -r 9d93b13f07ce src/Pure/Isar/element.ML --- 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) = diff -r 5e4e006f9552 -r 9d93b13f07ce src/Pure/ML/ml_env.ML --- 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 diff -r 5e4e006f9552 -r 9d93b13f07ce src/Pure/Pure.thy --- 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>\ML_prf\ "ML text within proof" (Parse.ML_source >> (fn source => Toplevel.proof (Proof.map_context (Context.proof_map diff -r 5e4e006f9552 -r 9d93b13f07ce src/Pure/Syntax/mixfix.ML --- 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;