# HG changeset patch # User wenzelm # Date 1439832855 -7200 # Node ID 574254152856be599e3a93346af9832f9dbe7e59 # Parent 10d463883dc205ff0516abeeaae68720b4d92819 support for ML files with/without debugger information; diff -r 10d463883dc2 -r 574254152856 src/Pure/Isar/isar_syn.ML --- 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" diff -r 10d463883dc2 -r 574254152856 src/Pure/ML/ml_file.ML --- 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; diff -r 10d463883dc2 -r 574254152856 src/Pure/Pure.thy --- 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" ?? *) diff -r 10d463883dc2 -r 574254152856 src/Pure/ROOT.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; - diff -r 10d463883dc2 -r 574254152856 src/Pure/Thy/thy_header.ML --- 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 *) diff -r 10d463883dc2 -r 574254152856 src/Pure/Thy/thy_header.scala --- 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)