# HG changeset patch
# User wenzelm
# Date 1456857779 -3600
# Node ID 39d01eaf5292cc90e52a14f3216939d00c3df0d0
# Parent  36f11bc393a26b0dbcf417f5ce75d9177367b2db
ML debugger support in Pure (again, see 3565c9f407ec);

diff -r 36f11bc393a2 -r 39d01eaf5292 src/Pure/ML/ml_compiler.ML
--- a/src/Pure/ML/ml_compiler.ML	Tue Mar 01 17:26:53 2016 +0100
+++ b/src/Pure/ML/ml_compiler.ML	Tue Mar 01 19:42:59 2016 +0100
@@ -9,11 +9,11 @@
   type flags =
     {SML: bool, exchange: bool, redirect: bool, verbose: bool,
       debug: bool option, writeln: string -> unit, warning: string -> unit}
+  val debug_flags: bool option -> flags
   val flags: flags
   val verbose: bool -> flags -> flags
   val eval: flags -> Position.T -> ML_Lex.token list -> unit
-end
-
+end;
 
 structure ML_Compiler: ML_COMPILER =
 struct
@@ -24,9 +24,11 @@
   {SML: bool, exchange: bool, redirect: bool, verbose: bool,
     debug: bool option, writeln: string -> unit, warning: string -> unit};
 
-val flags: flags =
+fun debug_flags opt_debug : flags =
   {SML = false, exchange = false, redirect = false, verbose = false,
-    debug = NONE, writeln = writeln, warning = warning};
+    debug = opt_debug, writeln = writeln, warning = warning};
+
+val flags = debug_flags NONE;
 
 fun verbose b (flags: flags) =
   {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags,
diff -r 36f11bc393a2 -r 39d01eaf5292 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Tue Mar 01 17:26:53 2016 +0100
+++ b/src/Pure/Pure.thy	Tue Mar 01 19:42:59 2016 +0100
@@ -107,7 +107,7 @@
 ML_file "Tools/find_theorems.ML"
 ML_file "Tools/find_consts.ML"
 ML_file "Tools/simplifier_trace.ML"
-ML_file "Tools/debugger.ML"
+ML_file_no_debug "Tools/debugger.ML"
 ML_file "Tools/named_theorems.ML"
 ML_file "Tools/jedit.ML"
 
diff -r 36f11bc393a2 -r 39d01eaf5292 src/Pure/RAW/ROOT_polyml.ML
--- a/src/Pure/RAW/ROOT_polyml.ML	Tue Mar 01 17:26:53 2016 +0100
+++ b/src/Pure/RAW/ROOT_polyml.ML	Tue Mar 01 19:42:59 2016 +0100
@@ -164,7 +164,6 @@
 if ML_System.name = "polyml-5.6"
 then use "RAW/ml_compiler_parameters_polyml-5.6.ML" else ();
 
-use "RAW/use_context.ML";
 use "RAW/ml_positions.ML";
 use "RAW/compiler_polyml.ML";
 
@@ -186,5 +185,5 @@
 (* ML debugger *)
 
 if ML_System.name = "polyml-5.6"
-then use "RAW/ml_debugger_polyml-5.6.ML"
-else use "RAW/ml_debugger.ML";
+then use_no_debug "RAW/ml_debugger_polyml-5.6.ML"
+else use_no_debug "RAW/ml_debugger.ML";
diff -r 36f11bc393a2 -r 39d01eaf5292 src/Pure/RAW/compiler_polyml.ML
--- a/src/Pure/RAW/compiler_polyml.ML	Tue Mar 01 17:26:53 2016 +0100
+++ b/src/Pure/RAW/compiler_polyml.ML	Tue Mar 01 19:42:59 2016 +0100
@@ -3,8 +3,20 @@
 Basic runtime compilation for Poly/ML (cf. Pure/ML/ml_compiler_polyml.ML).
 *)
 
+type use_context =
+ {name_space: ML_Name_Space.T,
+  str_of_pos: int -> string -> string,
+  print: string -> unit,
+  error: string -> unit};
+
 local
 
+val boot_context: use_context =
+ {name_space = ML_Name_Space.global,
+  str_of_pos = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")",
+  print = fn s => (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut),
+  error = fn s => raise Fail s};
+
 fun drop_newline s =
   if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
   else s;
@@ -55,8 +67,22 @@
     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;
 
-fun use file =
-  use_file boot_context {verbose = true, debug = false} file
+
+fun use_debug_option NONE = OS.Process.getEnv "ISABELLE_ML_DEBUGGER" = SOME "true"
+  | use_debug_option (SOME debug) = debug;
+
+local
+
+fun use_ opt_debug file =
+  use_file boot_context {verbose = true, debug = use_debug_option opt_debug} file
     handle Fail msg => (#print boot_context msg; raise Fail "ML error");
 
+in
+
+val use = use_ NONE;
+val use_debug = use_ (SOME true);
+val use_no_debug = use_ (SOME false);
+
 end;
+
+end;
diff -r 36f11bc393a2 -r 39d01eaf5292 src/Pure/RAW/use_context.ML
--- a/src/Pure/RAW/use_context.ML	Tue Mar 01 17:26:53 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-(*  Title:      Pure/RAW/use_context.ML
-    Author:     Makarius
-
-Common context for "use" operations (compiler invocation).
-*)
-
-type use_context =
- {name_space: ML_Name_Space.T,
-  str_of_pos: int -> string -> string,
-  print: string -> unit,
-  error: string -> unit};
-
-val boot_context: use_context =
- {name_space = ML_Name_Space.global,
-  str_of_pos = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")",
-  print = fn s => (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut),
-  error = fn s => raise Fail s};
diff -r 36f11bc393a2 -r 39d01eaf5292 src/Pure/ROOT
--- a/src/Pure/ROOT	Tue Mar 01 17:26:53 2016 +0100
+++ b/src/Pure/ROOT	Tue Mar 01 19:42:59 2016 +0100
@@ -30,7 +30,6 @@
     "RAW/multithreading.ML"
     "RAW/single_assignment_polyml.ML"
     "RAW/unsynchronized.ML"
-    "RAW/use_context.ML"
 
 session Pure =
   global_theories Pure
@@ -62,7 +61,6 @@
     "RAW/multithreading.ML"
     "RAW/single_assignment_polyml.ML"
     "RAW/unsynchronized.ML"
-    "RAW/use_context.ML"
 
     "Concurrent/bash.ML"
     "Concurrent/bash_windows.ML"
diff -r 36f11bc393a2 -r 39d01eaf5292 src/Pure/ROOT.ML
--- 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;
 
 
 
diff -r 36f11bc393a2 -r 39d01eaf5292 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Mar 01 17:26:53 2016 +0100
+++ b/src/Pure/Tools/build.scala	Tue Mar 01 19:42:59 2016 +0100
@@ -567,9 +567,15 @@
         }))
 
     private val env =
-      Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output_standard_path,
-        (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") ->
-          File.standard_path(args_file))
+    {
+      val env0 =
+        Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output_standard_path,
+          (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") ->
+            File.standard_path(args_file))
+      if (is_pure(name))
+        env0 + ("ISABELLE_ML_DEBUGGER" -> info.options.bool("ML_debugger").toString)
+      else env0
+    }
 
     private val script =
       """