src/Pure/ROOT.ML
changeset 62490 39d01eaf5292
parent 62459 7a5d88dd8cc9
child 62493 dd154240a53c
--- a/src/Pure/ROOT.ML	Tue Mar 01 17:26:53 2016 +0100
+++ b/src/Pure/ROOT.ML	Tue Mar 01 19:42:59 2016 +0100
@@ -39,11 +39,18 @@
 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
+local
+  fun use_ opt_debug file =
+    Position.setmp_thread_data (Position.file_only file)
+      (fn () =>
+        Secure.use_file ML_Parse.global_context
+          {verbose = true, debug = use_debug_option opt_debug} file
         handle ERROR msg => (writeln msg; error "ML error")) ();
+in
+  val use = use_ NONE;
+  val use_debug = use_ (SOME true);
+  val use_no_debug = use_ (SOME false);
+end;
 
 
 
@@ -223,9 +230,19 @@
 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_ opt_debug file =
+    let val flags = ML_Compiler.debug_flags opt_debug |> ML_Compiler.verbose true 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;