# HG changeset patch # User wenzelm # Date 1439839961 -7200 # Node ID 3565c9f407eca37e3f233bde5307d3297bbaf710 # Parent 5d70b5c509f82cdbecb8f72a835892ddbe098590 no ML_debugger support in Pure -- too complicated; diff -r 5d70b5c509f8 -r 3565c9f407ec src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Mon Aug 17 21:22:55 2015 +0200 +++ b/src/Pure/ROOT.ML Mon Aug 17 21:32:41 2015 +0200 @@ -41,24 +41,11 @@ val use_text = Secure.use_text; val use_file = Secure.use_file; -local - fun use_ debug_option file = - let - val debug = - (case debug_option of - SOME debug => debug - | NONE => getenv "ISABELLE_ML_DEBUGGER" = "true"); - 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 - val use = use_ NONE; - val use_debug = use_ (SOME true); - val use_no_debug = use_ (SOME false); -end; +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")) (); val toplevel_pp = Secure.toplevel_pp; @@ -257,21 +244,9 @@ use "ML/ml_context.ML"; use "ML/ml_antiquotation.ML"; -local - fun use_ debug file = - let - val flags: ML_Compiler.flags = - {SML = false, exchange = false, redirect = false, verbose = true, - debug = debug, writeln = writeln, warning = warning}; - in - ML_Context.eval_file 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; +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"); diff -r 5d70b5c509f8 -r 3565c9f407ec src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Mon Aug 17 21:22:55 2015 +0200 +++ b/src/Pure/Tools/build.scala Mon Aug 17 21:32:41 2015 +0200 @@ -590,16 +590,11 @@ (info.chapter, (name, theories))))))))))) })) - private val env0 = + private val env = Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output), (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") -> Isabelle_System.posix_path(args_file)) - private val env = - if (is_pure(name)) - env0 + ("ISABELLE_ML_DEBUGGER" -> info.options.bool("ML_debugger").toString) - else env0 - private val script = if (is_pure(name)) { if (do_output) "./build " + name + " \"$OUTPUT\""