# HG changeset patch # User Lars Hupel # Date 1527325561 -7200 # Node ID 310b8c1e4dbb7a6530c6772bbb3be833277c9dc5 # Parent 5824e400cecca36fcba704d9f9df72c52073d549# Parent 23e12da0866cd32b51a9f9bf1a458e82ee7e9d4a merged diff -r 5824e400cecc -r 310b8c1e4dbb NEWS --- a/NEWS Fri May 25 21:08:00 2018 +0200 +++ b/NEWS Sat May 26 11:06:01 2018 +0200 @@ -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 5824e400cecc -r 310b8c1e4dbb src/Doc/Isar_Ref/Inner_Syntax.thy --- a/src/Doc/Isar_Ref/Inner_Syntax.thy Fri May 25 21:08:00 2018 +0200 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Sat May 26 11:06:01 2018 +0200 @@ -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 5824e400cecc -r 310b8c1e4dbb src/Doc/Isar_Ref/Spec.thy --- a/src/Doc/Isar_Ref/Spec.thy Fri May 25 21:08:00 2018 +0200 +++ b/src/Doc/Isar_Ref/Spec.thy Sat May 26 11:06:01 2018 +0200 @@ -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 5824e400cecc -r 310b8c1e4dbb src/Doc/System/Environment.thy --- a/src/Doc/System/Environment.thy Fri May 25 21:08:00 2018 +0200 +++ b/src/Doc/System/Environment.thy Sat May 26 11:06:01 2018 +0200 @@ -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 5824e400cecc -r 310b8c1e4dbb src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Fri May 25 21:08:00 2018 +0200 +++ b/src/Pure/Isar/element.ML Sat May 26 11:06:01 2018 +0200 @@ -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 5824e400cecc -r 310b8c1e4dbb src/Pure/ML/ml_env.ML --- a/src/Pure/ML/ml_env.ML Fri May 25 21:08:00 2018 +0200 +++ b/src/Pure/ML/ml_env.ML Sat May 26 11:06:01 2018 +0200 @@ -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 5824e400cecc -r 310b8c1e4dbb src/Pure/Pure.thy --- a/src/Pure/Pure.thy Fri May 25 21:08:00 2018 +0200 +++ b/src/Pure/Pure.thy Sat May 26 11:06:01 2018 +0200 @@ -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 5824e400cecc -r 310b8c1e4dbb src/Pure/Syntax/mixfix.ML --- a/src/Pure/Syntax/mixfix.ML Fri May 25 21:08:00 2018 +0200 +++ b/src/Pure/Syntax/mixfix.ML Sat May 26 11:06:01 2018 +0200 @@ -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;