# HG changeset patch # User wenzelm # Date 1459807128 -7200 # Node ID 007c454d0d0fe0d0de1fdb34f375aad8ec5a2ceb # Parent cfd2749e1352c9bd6c9010b01d5429a0b3f6c8c8 more uniform ML file commands; diff -r cfd2749e1352 -r 007c454d0d0f src/Doc/Isar_Ref/Spec.thy --- a/src/Doc/Isar_Ref/Spec.thy Mon Apr 04 23:13:41 2016 +0200 +++ b/src/Doc/Isar_Ref/Spec.thy Mon Apr 04 23:58:48 2016 +0200 @@ -1026,7 +1026,7 @@ text \ \begin{matharray}{rcl} - @{command_def "SML_file"} & : & \theory \ theory\ \\ + @{command_def "SML_file"} & : & \local_theory \ local_theory\ \\ @{command_def "ML_file"} & : & \local_theory \ local_theory\ \\ @{command_def "ML"} & : & \local_theory \ local_theory\ \\ @{command_def "ML_prf"} & : & \proof \ proof\ \\ @@ -1052,11 +1052,11 @@ \} \<^descr> \<^theory_text>\SML_file name\ reads and evaluates the given Standard ML file. Top-level - SML bindings are stored within the theory context; the initial environment - is restricted to the Standard ML implementation of Poly/ML, without the many - add-ons of Isabelle/ML. Multiple \<^theory_text>\SML_file\ commands may be used to build - larger Standard ML projects, independently of the regular Isabelle/ML - environment. + SML bindings are stored within the (global or local) theory context; the + initial environment is restricted to the Standard ML implementation of + Poly/ML, without the many add-ons of Isabelle/ML. Multiple \<^theory_text>\SML_file\ + commands may be used to build larger Standard ML projects, independently of + the regular Isabelle/ML environment. \<^descr> \<^theory_text>\ML_file name\ reads and evaluates the given ML file. The current theory context is passed down to the ML toplevel and may be modified, using @{ML diff -r cfd2749e1352 -r 007c454d0d0f src/Pure/ML/ml_file.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML/ml_file.ML Mon Apr 04 23:58:48 2016 +0200 @@ -0,0 +1,45 @@ +(* Title: Pure/ML/ml_file.ML + Author: Makarius + +Commands to load ML files. +*) + +signature ML_FILE = +sig + val ML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition + val SML: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition + val any: bool option -> (theory -> Token.file list) -> Toplevel.transition -> Toplevel.transition +end; + +structure ML_File: ML_FILE = +struct + +fun command SML debug files = Toplevel.generic_theory (fn gthy => + let + val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy); + val provide = Resources.provide (src_path, digest); + val source = Input.source true (cat_lines lines) (pos, pos); + val flags = + {SML = SML src_path, exchange = false, redirect = true, verbose = true, + debug = debug, writeln = writeln, warning = warning}; + in + gthy + |> ML_Context.exec (fn () => ML_Context.eval_source flags source) + |> Local_Theory.propagate_ml_env + |> Context.mapping provide (Local_Theory.background_theory provide) + end); + +val ML = command (K false); +val SML = command (K true); + +val any = + command (fn path => + (case try (#2 o Path.split_ext) path of + SOME "ML" => false + | SOME "sml" => true + | SOME "sig" => true + | _ => + error ("Bad file name " ^ Path.print path ^ + "\nExpected .ML for Isabelle/ML or .sml/.sig for Standard ML"))); + +end; diff -r cfd2749e1352 -r 007c454d0d0f src/Pure/Pure.thy --- a/src/Pure/Pure.thy Mon Apr 04 23:13:41 2016 +0200 +++ b/src/Pure/Pure.thy Mon Apr 04 23:58:48 2016 +0200 @@ -100,60 +100,33 @@ ML \ local -fun ML_file_cmd debug files = Toplevel.generic_theory (fn gthy => - let - val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy); - val provide = Resources.provide (src_path, digest); - val source = Input.source true (cat_lines lines) (pos, pos); - val flags: ML_Compiler.flags = - {SML = false, exchange = false, redirect = true, verbose = true, - debug = debug, writeln = writeln, warning = warning}; - in - gthy - |> ML_Context.exec (fn () => ML_Context.eval_source flags source) - |> Local_Theory.propagate_ml_env - |> Context.mapping provide (Local_Theory.background_theory provide) - end); - -fun SML_file_cmd debug files = Toplevel.theory (fn thy => - let - val ([{lines, pos, ...}: Token.file], thy') = files thy; - val source = Input.source true (cat_lines lines) (pos, pos); - val flags: ML_Compiler.flags = - {SML = true, exchange = false, redirect = true, verbose = true, - debug = debug, writeln = writeln, warning = warning}; - in - thy' |> Context.theory_map - (ML_Context.exec (fn () => ML_Context.eval_source flags source)) - end); - val _ = Outer_Syntax.command ("ML_file", @{here}) "read and evaluate Isabelle/ML file" - (Resources.parse_files "ML_file" >> ML_file_cmd NONE); + (Resources.parse_files "ML_file" >> ML_File.ML NONE); val _ = Outer_Syntax.command ("ML_file_debug", @{here}) "read and evaluate Isabelle/ML file (with debugger information)" - (Resources.parse_files "ML_file_debug" >> ML_file_cmd (SOME true)); + (Resources.parse_files "ML_file_debug" >> ML_File.ML (SOME true)); val _ = Outer_Syntax.command ("ML_file_no_debug", @{here}) "read and evaluate Isabelle/ML file (no debugger information)" - (Resources.parse_files "ML_file_no_debug" >> ML_file_cmd (SOME false)); + (Resources.parse_files "ML_file_no_debug" >> ML_File.ML (SOME false)); val _ = Outer_Syntax.command @{command_keyword SML_file} "read and evaluate Standard ML file" - (Resources.provide_parse_files "SML_file" >> SML_file_cmd NONE); + (Resources.parse_files "SML_file" >> ML_File.SML NONE); val _ = Outer_Syntax.command @{command_keyword SML_file_debug} "read and evaluate Standard ML file (with debugger information)" - (Resources.provide_parse_files "SML_file_debug" >> SML_file_cmd (SOME true)); + (Resources.parse_files "SML_file_debug" >> ML_File.SML (SOME true)); val _ = Outer_Syntax.command @{command_keyword SML_file_no_debug} "read and evaluate Standard ML file (no debugger information)" - (Resources.provide_parse_files "SML_file_no_debug" >> SML_file_cmd (SOME false)); + (Resources.parse_files "SML_file_no_debug" >> ML_File.SML (SOME false)); val _ = Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment" diff -r cfd2749e1352 -r 007c454d0d0f src/Pure/ROOT --- a/src/Pure/ROOT Mon Apr 04 23:13:41 2016 +0200 +++ b/src/Pure/ROOT Mon Apr 04 23:58:48 2016 +0200 @@ -107,6 +107,7 @@ "ML/ml_context.ML" "ML/ml_debugger.ML" "ML/ml_env.ML" + "ML/ml_file.ML" "ML/ml_heap.ML" "ML/ml_lex.ML" "ML/ml_name_space.ML" diff -r cfd2749e1352 -r 007c454d0d0f src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Mon Apr 04 23:13:41 2016 +0200 +++ b/src/Pure/ROOT.ML Mon Apr 04 23:58:48 2016 +0200 @@ -316,6 +316,7 @@ use "ML/ml_pp.ML"; use "ML/ml_antiquotations.ML"; use "ML/ml_thms.ML"; +use "ML/ml_file.ML"; use "Tools/build.ML"; use "Tools/named_thms.ML";