merged
authorwenzelm
Fri May 25 22:48:37 2018 +0200 (20 months ago)
changeset 68277c2b227b8e361
parent 68270 2bc921b2159b
parent 68276 cbee43ff4ceb
child 68278 23e12da0866c
merged
     1.1 --- a/NEWS	Thu May 24 09:26:26 2018 +0000
     1.2 +++ b/NEWS	Fri May 25 22:48:37 2018 +0200
     1.3 @@ -358,6 +358,11 @@
     1.4  * Operation Export.export emits theory exports (arbitrary blobs), which
     1.5  are stored persistently in the session build database.
     1.6  
     1.7 +* Command 'ML_export' exports ML toplevel bindings to the global
     1.8 +bootstrap environment of the ML process. This allows ML evaluation
     1.9 +without a formal theory context, e.g. in command-line tools like
    1.10 +"isabelle process".
    1.11 +
    1.12  
    1.13  *** System ***
    1.14  
     2.1 --- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Thu May 24 09:26:26 2018 +0000
     2.2 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Fri May 25 22:48:37 2018 +0200
     2.3 @@ -281,12 +281,14 @@
     2.4      @{syntax_def mixfix}: '('
     2.5        (@{syntax template} prios? @{syntax nat}? |
     2.6          (@'infix' | @'infixl' | @'infixr') @{syntax template} @{syntax nat} |
     2.7 -        @'binder' @{syntax template} prios? @{syntax nat} |
     2.8 +        @'binder' @{syntax template} prio? @{syntax nat} |
     2.9          @'structure') ')'
    2.10      ;
    2.11      @{syntax template}: string
    2.12      ;
    2.13      prios: '[' (@{syntax nat} + ',') ']'
    2.14 +    ;
    2.15 +    prio: '[' @{syntax nat} ']'
    2.16    \<close>}
    2.17  
    2.18    The string given as \<open>template\<close> may include literal text, spacing, blocks,
     3.1 --- a/src/Doc/Isar_Ref/Spec.thy	Thu May 24 09:26:26 2018 +0000
     3.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Fri May 25 22:48:37 2018 +0200
     3.3 @@ -1058,6 +1058,7 @@
     3.4      @{command_def "ML_file_debug"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
     3.5      @{command_def "ML_file_no_debug"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
     3.6      @{command_def "ML"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
     3.7 +    @{command_def "ML_export"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
     3.8      @{command_def "ML_prf"} & : & \<open>proof \<rightarrow> proof\<close> \\
     3.9      @{command_def "ML_val"} & : & \<open>any \<rightarrow>\<close> \\
    3.10      @{command_def "ML_command"} & : & \<open>any \<rightarrow>\<close> \\
    3.11 @@ -1081,8 +1082,9 @@
    3.12        @@{command ML_file_debug} |
    3.13        @@{command ML_file_no_debug}) @{syntax name} ';'?
    3.14      ;
    3.15 -    (@@{command ML} | @@{command ML_prf} | @@{command ML_val} |
    3.16 -      @@{command ML_command} | @@{command setup} | @@{command local_setup}) @{syntax text}
    3.17 +    (@@{command ML} | @@{command ML_export} | @@{command ML_prf} |
    3.18 +      @@{command ML_val} | @@{command ML_command} | @@{command setup} |
    3.19 +      @@{command local_setup}) @{syntax text}
    3.20      ;
    3.21      @@{command attribute_setup} @{syntax name} '=' @{syntax text} @{syntax text}?
    3.22    \<close>}
    3.23 @@ -1103,10 +1105,16 @@
    3.24    \<^theory_text>\<open>ML_file_no_debug\<close> change the @{attribute ML_debugger} option locally while
    3.25    the given file is compiled.
    3.26  
    3.27 -  \<^descr> \<^theory_text>\<open>ML text\<close> is similar to \<^theory_text>\<open>ML_file\<close>, but evaluates directly the given
    3.28 -  \<open>text\<close>. Top-level ML bindings are stored within the (global or local) theory
    3.29 +  \<^descr> \<^theory_text>\<open>ML\<close> is similar to \<^theory_text>\<open>ML_file\<close>, but evaluates directly the given \<open>text\<close>.
    3.30 +  Top-level ML bindings are stored within the (global or local) theory
    3.31    context.
    3.32  
    3.33 +  \<^descr> \<^theory_text>\<open>ML_export\<close> is similar to \<^theory_text>\<open>ML\<close>, but the resulting toplevel bindings are
    3.34 +  exported to the global bootstrap environment of the ML process --- it has
    3.35 +  has a lasting effect that cannot be retracted. This allows ML evaluation
    3.36 +  without a formal theory context, e.g. for command-line tools via @{tool
    3.37 +  process} @{cite "isabelle-system"}.
    3.38 +
    3.39    \<^descr> \<^theory_text>\<open>ML_prf\<close> is analogous to \<^theory_text>\<open>ML\<close> but works within a proof context.
    3.40    Top-level ML bindings are stored within the proof context in a purely
    3.41    sequential fashion, disregarding the nested proof structure. ML bindings
     4.1 --- a/src/Doc/System/Environment.thy	Thu May 24 09:26:26 2018 +0000
     4.2 +++ b/src/Doc/System/Environment.thy	Fri May 25 22:48:37 2018 +0200
     4.3 @@ -365,7 +365,7 @@
     4.4  \<close>
     4.5  
     4.6  
     4.7 -subsubsection \<open>Example\<close>
     4.8 +subsubsection \<open>Examples\<close>
     4.9  
    4.10  text \<open>
    4.11    The subsequent example retrieves the \<^verbatim>\<open>Main\<close> theory value from the theory
    4.12 @@ -375,6 +375,12 @@
    4.13    Observe the delicate quoting rules for the GNU bash shell vs.\ ML. The
    4.14    Isabelle/ML and Scala libraries provide functions for that, but here we need
    4.15    to do it manually.
    4.16 +
    4.17 +  \<^medskip>
    4.18 +  This is how to invoke a function body with proper return code and printing
    4.19 +  of errors, and without printing of a redundant \<^verbatim>\<open>val it = (): unit\<close> result:
    4.20 +  @{verbatim [display] \<open>isabelle process -e 'Command_Line.tool0 (fn () => writeln "OK")'\<close>}
    4.21 +  @{verbatim [display] \<open>isabelle process -e 'Command_Line.tool0 (fn () => error "Bad")'\<close>}
    4.22  \<close>
    4.23  
    4.24  
     5.1 --- a/src/Pure/Isar/element.ML	Thu May 24 09:26:26 2018 +0000
     5.2 +++ b/src/Pure/Isar/element.ML	Fri May 25 22:48:37 2018 +0200
     5.3 @@ -171,9 +171,8 @@
     5.4        | prt_mixfix mx = [Pretty.brk 2, Mixfix.pretty_mixfix mx];
     5.5  
     5.6      fun prt_fix (x, SOME T, mx) = Pretty.block (prt_name (Binding.name_of x) :: Pretty.str " ::" ::
     5.7 -          Pretty.brk 1 :: prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
     5.8 -      | prt_fix (x, NONE, mx) = Pretty.block (prt_name (Binding.name_of x) ::
     5.9 -          Pretty.brk 1 :: prt_mixfix mx);
    5.10 +          Pretty.brk 1 :: prt_typ T :: prt_mixfix mx)
    5.11 +      | prt_fix (x, NONE, mx) = Pretty.block (prt_name (Binding.name_of x) :: prt_mixfix mx);
    5.12      fun prt_constrain (x, T) = prt_fix (Binding.name x, SOME T, NoSyn);
    5.13  
    5.14      fun prt_asm (a, ts) =
     6.1 --- a/src/Pure/ML/ml_env.ML	Thu May 24 09:26:26 2018 +0000
     6.2 +++ b/src/Pure/ML/ml_env.ML	Fri May 25 22:48:37 2018 +0200
     6.3 @@ -13,6 +13,8 @@
     6.4    val add_breakpoints: (serial * (bool Unsynchronized.ref * Thread_Position.T)) list -> unit
     6.5    val init_bootstrap: Context.generic -> Context.generic
     6.6    val SML_environment: bool Config.T
     6.7 +  val set_bootstrap: bool -> Context.generic -> Context.generic
     6.8 +  val restore_bootstrap: Context.generic -> Context.generic -> Context.generic
     6.9    val add_name_space: {SML: bool} -> ML_Name_Space.T -> Context.generic -> Context.generic
    6.10    val make_name_space: {SML: bool, exchange: bool} -> ML_Name_Space.T
    6.11    val context: ML_Compiler0.context
    6.12 @@ -130,6 +132,12 @@
    6.13              in (val2, type1, fixity1, structure2, signature2, functor1) end);
    6.14      in make_data (bootstrap, tables, sml_tables', breakpoints) end);
    6.15  
    6.16 +fun set_bootstrap bootstrap =
    6.17 +  Env.map (fn {tables, sml_tables, breakpoints, ...} =>
    6.18 +    make_data (bootstrap, tables, sml_tables, breakpoints));
    6.19 +
    6.20 +val restore_bootstrap = set_bootstrap o #bootstrap o Env.get;
    6.21 +
    6.22  fun add_name_space {SML} (space: ML_Name_Space.T) =
    6.23    Env.map (fn {bootstrap, tables, sml_tables, breakpoints} =>
    6.24      let
     7.1 --- a/src/Pure/Pure.thy	Thu May 24 09:26:26 2018 +0000
     7.2 +++ b/src/Pure/Pure.thy	Fri May 25 22:48:37 2018 +0200
     7.3 @@ -23,7 +23,7 @@
     7.4    and "external_file" "bibtex_file" :: thy_load
     7.5    and "ML_file" "ML_file_debug" "ML_file_no_debug" :: thy_load % "ML"
     7.6    and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
     7.7 -  and "SML_import" "SML_export" :: thy_decl % "ML"
     7.8 +  and "SML_import" "SML_export" "ML_export" :: thy_decl % "ML"
     7.9    and "ML_prf" :: prf_decl % "proof"  (* FIXME % "ML" ?? *)
    7.10    and "ML_val" "ML_command" :: diag % "ML"
    7.11    and "simproc_setup" :: thy_decl % "ML"
    7.12 @@ -191,6 +191,18 @@
    7.13        end));
    7.14  
    7.15  val _ =
    7.16 +  Outer_Syntax.command ("ML_export", \<^here>)
    7.17 +    "ML text within theory or local theory, and export to bootstrap environment"
    7.18 +    (Parse.ML_source >> (fn source =>
    7.19 +      Toplevel.generic_theory (fn context =>
    7.20 +        context
    7.21 +        |> ML_Env.set_bootstrap true
    7.22 +        |> ML_Context.exec (fn () =>
    7.23 +            ML_Context.eval_source (ML_Compiler.verbose true ML_Compiler.flags) source)
    7.24 +        |> ML_Env.restore_bootstrap context
    7.25 +        |> Local_Theory.propagate_ml_env)));
    7.26 +
    7.27 +val _ =
    7.28    Outer_Syntax.command \<^command_keyword>\<open>ML_prf\<close> "ML text within proof"
    7.29      (Parse.ML_source >> (fn source =>
    7.30        Toplevel.proof (Proof.map_context (Context.proof_map
     8.1 --- a/src/Pure/Syntax/mixfix.ML	Thu May 24 09:26:26 2018 +0000
     8.2 +++ b/src/Pure/Syntax/mixfix.ML	Fri May 25 22:48:37 2018 +0200
     8.3 @@ -97,12 +97,18 @@
     8.4  
     8.5  fun pretty_mixfix NoSyn = Pretty.str ""
     8.6    | pretty_mixfix (Mixfix (s, ps, p, _)) =
     8.7 -      parens (Pretty.breaks [quoted s, brackets (Pretty.commas (map int ps)), int p])
     8.8 +      parens
     8.9 +        (Pretty.breaks
    8.10 +          (quoted s ::
    8.11 +            (if null ps then [] else [brackets (Pretty.commas (map int ps))]) @
    8.12 +            (if p = 1000 then [] else [int p])))
    8.13    | pretty_mixfix (Infix (s, p, _)) = parens (Pretty.breaks [keyword "infix", quoted s, int p])
    8.14    | pretty_mixfix (Infixl (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
    8.15 -  | pretty_mixfix (Infixr (s, p, _)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
    8.16 +  | pretty_mixfix (Infixr (s, p, _)) = parens (Pretty.breaks [keyword "infixr", quoted s, int p])
    8.17    | pretty_mixfix (Binder (s, p1, p2, _)) =
    8.18 -      parens (Pretty.breaks [keyword "binder", quoted s, brackets [int p1], int p2])
    8.19 +      parens
    8.20 +        (Pretty.breaks
    8.21 +          ([keyword "binder", quoted s] @ (if p1 = p2 then [] else [brackets [int p1]]) @ [int p2]))
    8.22    | pretty_mixfix (Structure _) = parens [keyword "structure"];
    8.23  
    8.24  end;