--- a/src/Pure/Isar/isar_syn.ML Mon Aug 17 16:27:12 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML Mon Aug 17 19:34:15 2015 +0200
@@ -203,19 +203,31 @@
(* use ML text *)
+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 @{command_keyword SML_file} "read and evaluate Standard ML file"
- (Resources.provide_parse_files "SML_file" >> (fn files => Toplevel.theory (fn thy =>
- let
- val ([{lines, pos, ...}], 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 = NONE, writeln = writeln, warning = warning};
- in
- thy' |> Context.theory_map
- (ML_Context.exec (fn () => ML_Context.eval_source flags source))
- end)));
+ (Resources.provide_parse_files "SML_file" >> SML_file_cmd 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));
+
+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));
val _ =
Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment"
--- a/src/Pure/ML/ml_file.ML Mon Aug 17 16:27:12 2015 +0200
+++ b/src/Pure/ML/ml_file.ML Mon Aug 17 19:34:15 2015 +0200
@@ -7,21 +7,33 @@
structure ML_File: sig end =
struct
+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);
+
val _ =
- Outer_Syntax.command ("ML_file", @{here}) "ML text from file"
- (Resources.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
- let
- val [{src_path, lines, digest, pos}] = 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 = NONE, 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)));
+ Outer_Syntax.command ("ML_file", @{here}) "read and evaluate Isabelle/ML file"
+ (Resources.parse_files "ML_file" >> ML_file_cmd 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));
+
+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));
end;
--- a/src/Pure/Pure.thy Mon Aug 17 16:27:12 2015 +0200
+++ b/src/Pure/Pure.thy Mon Aug 17 19:34:15 2015 +0200
@@ -21,7 +21,7 @@
"definition" "abbreviation" "type_notation" "no_type_notation" "notation"
"no_notation" "axiomatization" "theorems" "lemmas" "declare"
"hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
- and "SML_file" :: 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 "ML" :: thy_decl % "ML"
and "ML_prf" :: prf_decl % "proof" (* FIXME % "ML" ?? *)
--- a/src/Pure/ROOT.ML Mon Aug 17 16:27:12 2015 +0200
+++ b/src/Pure/ROOT.ML Mon Aug 17 19:34:15 2015 +0200
@@ -41,11 +41,23 @@
val use_text = Secure.use_text;
val use_file = Secure.use_file;
-fun use file =
- Position.setmp_thread_data (Position.file_only file)
- (fn () =>
- Secure.use_file ML_Parse.global_context {verbose = true, debug = false} file
- handle ERROR msg => (writeln msg; error "ML error")) ();
+fun use_fns default_debug_option =
+ let
+ fun use_ debug_option file =
+ let
+ val debug =
+ (case debug_option of
+ SOME debug => debug
+ | NONE => default_debug_option ());
+ in
+ Position.setmp_thread_data (Position.file_only file)
+ (fn () =>
+ Secure.use_file ML_Parse.global_context {verbose = true, debug = debug} file
+ handle ERROR msg => (writeln msg; error "ML error")) ()
+ end;
+ in {use = use_ NONE, use_debug = use_ (SOME true), use_no_debug = use_ (SOME false)} end;
+
+val {use, use_debug, use_no_debug} = use_fns (K false);
val toplevel_pp = Secure.toplevel_pp;
@@ -95,6 +107,8 @@
use "System/options.ML";
use "config.ML";
+val {use, use_debug, use_no_debug} = use_fns (fn () => Options.default_bool "ML_debugger");
+
(* concurrency within the ML runtime *)
@@ -204,6 +218,10 @@
use "ML/ml_syntax.ML";
use "ML/ml_env.ML";
use "ML/ml_options.ML";
+
+val {use, use_debug, use_no_debug} =
+ use_fns (fn () => ML_Options.debugger_enabled (Context.thread_data ()));
+
use "ML/exn_output.ML";
if ML_System.is_polyml then use "ML/exn_output_polyml.ML" else ();
use "ML/ml_options.ML";
@@ -244,9 +262,21 @@
use "ML/ml_context.ML";
use "ML/ml_antiquotation.ML";
-fun use s =
- ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode s)
- handle ERROR msg => (writeln msg; error "ML error");
+local
+ fun use_ debug file =
+ let
+ val flags =
+ {SML = false, exchange = false, redirect = false, verbose = true,
+ debug = debug, writeln = writeln, warning = warning};
+ in
+ ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode file)
+ handle ERROR msg => (writeln msg; error "ML error")
+ end
+in
+ val use = use_ NONE;
+ val use_debug = use_ (SOME true);
+ val use_no_debug = use_ (SOME false);
+end;
@@ -377,4 +407,3 @@
val cd = File.cd o Path.explode;
Proofterm.proofs := 0;
-
--- a/src/Pure/Thy/thy_header.ML Mon Aug 17 16:27:12 2015 +0200
+++ b/src/Pure/Thy/thy_header.ML Mon Aug 17 19:34:15 2015 +0200
@@ -78,7 +78,9 @@
((txtN, @{here}), SOME ((Keyword.document_body, []), [])),
((text_rawN, @{here}), SOME ((Keyword.document_raw, []), [])),
((theoryN, @{here}), SOME ((Keyword.thy_begin, []), ["theory"])),
- (("ML_file", @{here}), SOME ((Keyword.thy_load, []), ["ML"]))];
+ (("ML_file", @{here}), SOME ((Keyword.thy_load, []), ["ML"])),
+ (("ML_file_debug", @{here}), SOME ((Keyword.thy_load, []), ["ML"])),
+ (("ML_file_no_debug", @{here}), SOME ((Keyword.thy_load, []), ["ML"]))];
(* theory data *)
--- a/src/Pure/Thy/thy_header.scala Mon Aug 17 16:27:12 2015 +0200
+++ b/src/Pure/Thy/thy_header.scala Mon Aug 17 19:34:15 2015 +0200
@@ -55,7 +55,9 @@
(TXT, Some(((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
(TEXT_RAW, Some(((Keyword.DOCUMENT_RAW, Nil), Nil)), None),
(THEORY, Some((Keyword.THY_BEGIN, Nil), List("theory")), None),
- ("ML_file", Some((Keyword.THY_LOAD, Nil), List("ML")), None))
+ ("ML_file", Some((Keyword.THY_LOAD, Nil), List("ML")), None),
+ ("ML_file_debug", Some((Keyword.THY_LOAD, Nil), List("ML")), None),
+ ("ML_file_no_debug", Some((Keyword.THY_LOAD, Nil), List("ML")), None))
private val bootstrap_keywords =
Keyword.Keywords.empty.add_keywords(bootstrap_header)