# HG changeset patch
# User wenzelm
# Date 1439821632 -7200
# Node ID 10d463883dc205ff0516abeeaae68720b4d92819
# Parent  65149ae760a0f0ee97ab35339e71c0bbd48c1f4e
explicit debug flag for ML compiler;

diff -r 65149ae760a0 -r 10d463883dc2 src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML
--- a/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML	Mon Aug 17 15:29:30 2015 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/am_compiler.ML	Mon Aug 17 16:27:12 2015 +0200
@@ -184,7 +184,8 @@
 
     in
         compiled_rewriter := NONE;      
-        use_text ML_Env.local_context (1, "") false (!buffer);
+        use_text ML_Env.local_context
+          {line = 1, file = "", verbose = false, debug = false} (!buffer);
         case !compiled_rewriter of 
             NONE => raise (Compile "cannot communicate with compiled function")
           | SOME r => (compiled_rewriter := NONE; r)
diff -r 65149ae760a0 -r 10d463883dc2 src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML
--- a/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML	Mon Aug 17 15:29:30 2015 +0200
+++ b/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML	Mon Aug 17 16:27:12 2015 +0200
@@ -485,7 +485,8 @@
 
 fun writeTextFile name s = File.write (Path.explode name) s
 
-fun use_source src = use_text ML_Env.local_context (1, "") false src
+fun use_source src =
+  use_text ML_Env.local_context {line = 1, file = "", verbose = false, debug = false} src
     
 fun compile rules = 
     let
diff -r 65149ae760a0 -r 10d463883dc2 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Aug 17 15:29:30 2015 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Aug 17 16:27:12 2015 +0200
@@ -205,7 +205,9 @@
   File.read @{path "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs"}
 
 fun exec verbose code =
-  ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)
+  ML_Context.exec (fn () =>
+    Secure.use_text ML_Env.local_context
+      {line = 0, file = "generated code", verbose = verbose, debug = false} code)
 
 fun with_overlord_dir name f =
   let
diff -r 65149ae760a0 -r 10d463883dc2 src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Mon Aug 17 15:29:30 2015 +0200
+++ b/src/Pure/General/secure.ML	Mon Aug 17 16:27:12 2015 +0200
@@ -10,8 +10,9 @@
   val is_secure: unit -> bool
   val deny_secure: string -> unit
   val secure_mltext: unit -> unit
-  val use_text: use_context -> int * string -> bool -> string -> unit
-  val use_file: use_context -> bool -> string -> unit
+  val use_text: use_context ->
+    {line: int, file: string, verbose: bool, debug: bool} -> string -> unit
+  val use_file: use_context -> {verbose: bool, debug: bool} -> string -> unit
   val toplevel_pp: string list -> string -> unit
 end;
 
@@ -37,10 +38,9 @@
 val raw_use_file = use_file;
 val raw_toplevel_pp = toplevel_pp;
 
-fun use_text context pos verbose txt = (secure_mltext (); raw_use_text context pos verbose txt);
-fun use_file context verbose name = (secure_mltext (); raw_use_file context verbose name);
+fun use_text context flags (text: string) = (secure_mltext (); raw_use_text context flags text);
+fun use_file context flags (file: string) = (secure_mltext (); raw_use_file context flags file);
 
 fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp ML_Parse.global_context path pp);
 
 end;
-
diff -r 65149ae760a0 -r 10d463883dc2 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Aug 17 15:29:30 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Aug 17 16:27:12 2015 +0200
@@ -209,9 +209,9 @@
         let
           val ([{lines, pos, ...}], thy') = files thy;
           val source = Input.source true (cat_lines lines) (pos, pos);
-          val flags =
+          val flags: ML_Compiler.flags =
             {SML = true, exchange = false, redirect = true, verbose = true,
-              writeln = writeln, warning = warning};
+              debug = NONE, writeln = writeln, warning = warning};
         in
           thy' |> Context.theory_map
             (ML_Context.exec (fn () => ML_Context.eval_source flags source))
@@ -221,9 +221,9 @@
   Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment"
     (Parse.ML_source >> (fn source =>
       let
-        val flags =
+        val flags: ML_Compiler.flags =
           {SML = true, exchange = true, redirect = false, verbose = true,
-            writeln = writeln, warning = warning};
+            debug = NONE, writeln = writeln, warning = warning};
       in
         Toplevel.theory
           (Context.theory_map (ML_Context.exec (fn () => ML_Context.eval_source flags source)))
@@ -233,9 +233,9 @@
   Outer_Syntax.command @{command_keyword SML_import} "evaluate Isabelle/ML within SML environment"
     (Parse.ML_source >> (fn source =>
       let
-        val flags =
+        val flags: ML_Compiler.flags =
           {SML = false, exchange = true, redirect = false, verbose = true,
-            writeln = writeln, warning = warning};
+            debug = NONE, writeln = writeln, warning = warning};
       in
         Toplevel.generic_theory
           (ML_Context.exec (fn () => ML_Context.eval_source flags source) #>
diff -r 65149ae760a0 -r 10d463883dc2 src/Pure/ML-Systems/compiler_polyml.ML
--- a/src/Pure/ML-Systems/compiler_polyml.ML	Mon Aug 17 15:29:30 2015 +0200
+++ b/src/Pure/ML-Systems/compiler_polyml.ML	Mon Aug 17 16:27:12 2015 +0200
@@ -12,11 +12,11 @@
 in
 
 fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
-    (line, file) verbose txt =
+    {line, file, verbose, debug} text =
   let
     val current_line = Unsynchronized.ref line;
     val in_buffer =
-      Unsynchronized.ref (String.explode (tune_source (ml_positions line file txt)));
+      Unsynchronized.ref (String.explode (tune_source (ml_positions line file text)));
     val out_buffer = Unsynchronized.ref ([]: string list);
     fun output () = drop_newline (implode (rev (! out_buffer)));
 
@@ -38,7 +38,8 @@
       PolyML.Compiler.CPErrorMessageProc put_message,
       PolyML.Compiler.CPLineNo (fn () => ! current_line),
       PolyML.Compiler.CPFileName file,
-      PolyML.Compiler.CPPrintInAlphabeticalOrder false];
+      PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
+      ML_Compiler_Parameters.debug debug;
     val _ =
       (while not (List.null (! in_buffer)) do
         PolyML.compiler (get, parameters) ())
@@ -49,10 +50,10 @@
           error (output ()); reraise exn);
   in if verbose then print (output ()) else () end;
 
-fun use_file context verbose file =
+fun use_file context {verbose, debug} file =
   let
     val instream = TextIO.openIn file;
-    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
-  in use_text context (1, file) verbose txt end;
+    val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
+  in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
 
 end;
diff -r 65149ae760a0 -r 10d463883dc2 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Mon Aug 17 15:29:30 2015 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Mon Aug 17 16:27:12 2015 +0200
@@ -177,6 +177,10 @@
   val display_val = pretty_ml o PolyML.NameSpace.displayVal;
 end;
 
+use "ML-Systems/ml_compiler_parameters.ML";
+if ML_System.name = "polyml-5.5.3"
+then use "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML" else ();
+
 use "ML-Systems/use_context.ML";
 use "ML-Systems/ml_positions.ML";
 use "ML-Systems/compiler_polyml.ML";
@@ -191,12 +195,8 @@
 if ML_System.name = "polyml-5.5.3"
 then use "ML-Systems/ml_parse_tree_polyml-5.5.3.ML" else ();
 
-use "ML-Systems/ml_compiler_parameters.ML";
-if ML_System.name = "polyml-5.5.3"
-then use "ML-Systems/ml_compiler_parameters_polyml-5.5.3.ML" else ();
-
 fun toplevel_pp context (_: string list) pp =
-  use_text context (1, "pp") false
+  use_text context {line = 1, file = "pp", verbose = false, debug = false}
     ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
 
 fun ml_make_string struct_name =
diff -r 65149ae760a0 -r 10d463883dc2 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Mon Aug 17 15:29:30 2015 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Mon Aug 17 16:27:12 2015 +0200
@@ -82,7 +82,8 @@
 
 (* ML command execution *)
 
-fun use_text ({tune_source, print, error, ...}: use_context) (line, file) verbose txt =
+fun use_text ({tune_source, print, error, ...}: use_context)
+    {line, file, verbose, debug = _: bool} text =
   let
     val ref out_orig = Control.Print.out;
 
@@ -93,7 +94,7 @@
       in String.substring (str, 0, Int.max (0, size str - 1)) end;
   in
     Control.Print.out := out;
-    Backend.Interact.useStream (TextIO.openString (tune_source (ml_positions line file txt)))
+    Backend.Interact.useStream (TextIO.openString (tune_source (ml_positions line file text)))
       handle exn =>
         (Control.Print.out := out_orig;
           error ((if file = "" then "" else "Error in " ^ file ^ "\n") ^ output ()); raise exn);
@@ -101,11 +102,11 @@
     if verbose then print (output ()) else ()
   end;
 
-fun use_file context verbose file =
+fun use_file context {verbose, debug} file =
   let
     val instream = TextIO.openIn file;
-    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
-  in use_text context (1, file) verbose txt end;
+    val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
+  in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
 
 
 (* toplevel pretty printing *)
@@ -123,7 +124,7 @@
   in pprint end;
 
 fun toplevel_pp context path pp =
-  use_text context (1, "pp") false
+  use_text context {line = 1, file = "pp", verbose = false, debug = false}
     ("CompilerPPTable.install_pp [" ^ String.concatWith "," (map (fn s => "\"" ^ s ^ "\"")  path) ^
       "] (fn pps => ml_pprint pps o Pretty.to_ML o (" ^ pp ^ "))");
 
diff -r 65149ae760a0 -r 10d463883dc2 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Mon Aug 17 15:29:30 2015 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Mon Aug 17 16:27:12 2015 +0200
@@ -8,7 +8,7 @@
 sig
   type flags =
     {SML: bool, exchange: bool, redirect: bool, verbose: bool,
-      writeln: string -> unit, warning: string -> unit}
+      debug: bool option, writeln: string -> unit, warning: string -> unit}
   val flags: flags
   val verbose: bool -> flags -> flags
   val eval: flags -> Position.T -> ML_Lex.token list -> unit
@@ -19,23 +19,26 @@
 
 type flags =
   {SML: bool, exchange: bool, redirect: bool, verbose: bool,
-    writeln: string -> unit, warning: string -> unit};
+    debug: bool option, writeln: string -> unit, warning: string -> unit};
 
 val flags: flags =
   {SML = false, exchange = false, redirect = false, verbose = false,
-    writeln = writeln, warning = warning};
+    debug = NONE, writeln = writeln, warning = warning};
 
 fun verbose b (flags: flags) =
-  {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags, verbose = b,
-    writeln = #writeln flags, warning = #warning flags};
+  {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags,
+    verbose = b, debug = #debug flags, writeln = #writeln flags, warning = #warning flags};
 
 fun eval (flags: flags) pos toks =
   let
     val _ = if #SML flags then error ("Standard ML is unsupported on " ^ ML_System.name) else ();
     val line = the_default 1 (Position.line_of pos);
     val file = the_default "ML" (Position.file_of pos);
+    val debug = the_default false (#debug flags);
     val text = ML_Lex.flatten toks;
-  in Secure.use_text ML_Env.local_context (line, file) (#verbose flags) text end;
+  in
+    Secure.use_text ML_Env.local_context
+      {line = line, file = file, verbose = #verbose flags, debug = debug} text
+  end;
 
 end;
-
diff -r 65149ae760a0 -r 10d463883dc2 src/Pure/ML/ml_compiler_polyml.ML
--- a/src/Pure/ML/ml_compiler_polyml.ML	Mon Aug 17 15:29:30 2015 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Mon Aug 17 16:27:12 2015 +0200
@@ -225,6 +225,11 @@
 
     (* compiler invocation *)
 
+    val debug =
+      (case #debug flags of
+        SOME debug => debug
+      | NONE => ML_Options.debugger_enabled opt_context);
+
     val parameters =
      [PolyML.Compiler.CPOutStream write,
       PolyML.Compiler.CPNameSpace space,
@@ -235,7 +240,8 @@
       PolyML.Compiler.CPPrintDepth ML_Options.get_print_depth,
       PolyML.Compiler.CPCompilerResultFun result_fun,
       PolyML.Compiler.CPPrintInAlphabeticalOrder false] @
-     ML_Compiler_Parameters.debug (ML_Options.debugger_enabled opt_context);
+     ML_Compiler_Parameters.debug debug;
+
     val _ =
       (while not (List.null (! input_buffer)) do
         PolyML.compiler (get, parameters) ())
@@ -257,4 +263,3 @@
   end;
 
 end;
-
diff -r 65149ae760a0 -r 10d463883dc2 src/Pure/ML/ml_file.ML
--- a/src/Pure/ML/ml_file.ML	Mon Aug 17 15:29:30 2015 +0200
+++ b/src/Pure/ML/ml_file.ML	Mon Aug 17 16:27:12 2015 +0200
@@ -14,9 +14,9 @@
           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 =
+          val flags: ML_Compiler.flags =
             {SML = false, exchange = false, redirect = true, verbose = true,
-              writeln = writeln, warning = warning};
+              debug = NONE, writeln = writeln, warning = warning};
         in
           gthy
           |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
diff -r 65149ae760a0 -r 10d463883dc2 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Aug 17 15:29:30 2015 +0200
+++ b/src/Pure/ROOT.ML	Mon Aug 17 16:27:12 2015 +0200
@@ -41,10 +41,10 @@
 val use_text = Secure.use_text;
 val use_file = Secure.use_file;
 
-fun use s =
-  Position.setmp_thread_data (Position.file_only s)
+fun use file =
+  Position.setmp_thread_data (Position.file_only file)
     (fn () =>
-      Secure.use_file ML_Parse.global_context true s
+      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;
diff -r 65149ae760a0 -r 10d463883dc2 src/Pure/Tools/debugger.ML
--- a/src/Pure/Tools/debugger.ML	Mon Aug 17 15:29:30 2015 +0200
+++ b/src/Pure/Tools/debugger.ML	Mon Aug 17 16:27:12 2015 +0200
@@ -144,13 +144,12 @@
 fun evaluate {SML, verbose} =
   ML_Context.eval
     {SML = SML, exchange = false, redirect = false, verbose = verbose,
-      writeln = writeln_message, warning = warning_message}
+      debug = SOME false, writeln = writeln_message, warning = warning_message}
     Position.none;
 
 fun eval_setup thread_name index SML context =
   context
   |> Context_Position.set_visible_generic false
-  |> Config.put_generic ML_Options.debugger false
   |> ML_Env.add_name_space {SML = SML}
       (ML_Debugger.debug_name_space (the_debug_state thread_name index));
 
diff -r 65149ae760a0 -r 10d463883dc2 src/Tools/Code/code_runtime.ML
--- a/src/Tools/Code/code_runtime.ML	Mon Aug 17 15:29:30 2015 +0200
+++ b/src/Tools/Code/code_runtime.ML	Mon Aug 17 16:27:12 2015 +0200
@@ -80,8 +80,10 @@
 val trace = Attrib.setup_config_bool @{binding "code_runtime_trace"} (K false);
 
 fun exec ctxt verbose code =
-  (if Config.get ctxt trace then tracing code else ();
-  ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code));
+ (if Config.get ctxt trace then tracing code else ();
+  ML_Context.exec (fn () =>
+    Secure.use_text ML_Env.local_context
+      {line = 0, file = "generated code", verbose = verbose, debug = false} code));
 
 fun value ctxt (get, put, put_ml) (prelude, value) =
   let
@@ -538,8 +540,10 @@
   let
     val thy' = Loaded_Values.put [] thy;
     val _ = Context.set_thread_data ((SOME o Context.Theory) thy');
-    val _ = Secure.use_text notifying_context
-      (0, Path.implode filepath) false (File.read filepath);
+    val _ =
+      Secure.use_text notifying_context
+        {line = 0, file = Path.implode filepath, verbose = false, debug = false}
+        (File.read filepath);
     val thy'' = Context.the_theory (Context.the_thread_data ());
     val names = Loaded_Values.get thy'';
   in (names, thy'') end;
diff -r 65149ae760a0 -r 10d463883dc2 src/Tools/Spec_Check/spec_check.ML
--- a/src/Tools/Spec_Check/spec_check.ML	Mon Aug 17 15:29:30 2015 +0200
+++ b/src/Tools/Spec_Check/spec_check.ML	Mon Aug 17 16:27:12 2015 +0200
@@ -135,7 +135,9 @@
       error = #error ML_Env.local_context}
     val _ =
       Context.setmp_thread_data (SOME (Context.Proof ctxt))
-        (fn () => Secure.use_text use_context (0, "generated code") true s) ()
+        (fn () =>
+          Secure.use_text use_context
+            {line = 0, file = "generated code", verbose = true, debug = false} s) ()
   in
     Gen_Construction.parse_pred (! return)
   end;
@@ -143,7 +145,9 @@
 (*call the compiler and run the test*)
 fun run_test ctxt s =
   Context.setmp_thread_data (SOME (Context.Proof ctxt))
-    (fn () => Secure.use_text ML_Env.local_context (0, "generated code") false s) ();
+    (fn () =>
+      Secure.use_text ML_Env.local_context
+        {line = 0, file = "generated code", verbose = false, debug = false} s) ();
 
 (*split input into tokens*)
 fun input_split s =