ML debugger support in Pure (again, see 3565c9f407ec);
authorwenzelm
Tue Mar 01 19:42:59 2016 +0100 (2016-03-01)
changeset 6249039d01eaf5292
parent 62489 36f11bc393a2
child 62491 7187cb7a77c5
ML debugger support in Pure (again, see 3565c9f407ec);
src/Pure/ML/ml_compiler.ML
src/Pure/Pure.thy
src/Pure/RAW/ROOT_polyml.ML
src/Pure/RAW/compiler_polyml.ML
src/Pure/RAW/use_context.ML
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/ML/ml_compiler.ML	Tue Mar 01 17:26:53 2016 +0100
     1.2 +++ b/src/Pure/ML/ml_compiler.ML	Tue Mar 01 19:42:59 2016 +0100
     1.3 @@ -9,11 +9,11 @@
     1.4    type flags =
     1.5      {SML: bool, exchange: bool, redirect: bool, verbose: bool,
     1.6        debug: bool option, writeln: string -> unit, warning: string -> unit}
     1.7 +  val debug_flags: bool option -> flags
     1.8    val flags: flags
     1.9    val verbose: bool -> flags -> flags
    1.10    val eval: flags -> Position.T -> ML_Lex.token list -> unit
    1.11 -end
    1.12 -
    1.13 +end;
    1.14  
    1.15  structure ML_Compiler: ML_COMPILER =
    1.16  struct
    1.17 @@ -24,9 +24,11 @@
    1.18    {SML: bool, exchange: bool, redirect: bool, verbose: bool,
    1.19      debug: bool option, writeln: string -> unit, warning: string -> unit};
    1.20  
    1.21 -val flags: flags =
    1.22 +fun debug_flags opt_debug : flags =
    1.23    {SML = false, exchange = false, redirect = false, verbose = false,
    1.24 -    debug = NONE, writeln = writeln, warning = warning};
    1.25 +    debug = opt_debug, writeln = writeln, warning = warning};
    1.26 +
    1.27 +val flags = debug_flags NONE;
    1.28  
    1.29  fun verbose b (flags: flags) =
    1.30    {SML = #SML flags, exchange = #exchange flags, redirect = #redirect flags,
     2.1 --- a/src/Pure/Pure.thy	Tue Mar 01 17:26:53 2016 +0100
     2.2 +++ b/src/Pure/Pure.thy	Tue Mar 01 19:42:59 2016 +0100
     2.3 @@ -107,7 +107,7 @@
     2.4  ML_file "Tools/find_theorems.ML"
     2.5  ML_file "Tools/find_consts.ML"
     2.6  ML_file "Tools/simplifier_trace.ML"
     2.7 -ML_file "Tools/debugger.ML"
     2.8 +ML_file_no_debug "Tools/debugger.ML"
     2.9  ML_file "Tools/named_theorems.ML"
    2.10  ML_file "Tools/jedit.ML"
    2.11  
     3.1 --- a/src/Pure/RAW/ROOT_polyml.ML	Tue Mar 01 17:26:53 2016 +0100
     3.2 +++ b/src/Pure/RAW/ROOT_polyml.ML	Tue Mar 01 19:42:59 2016 +0100
     3.3 @@ -164,7 +164,6 @@
     3.4  if ML_System.name = "polyml-5.6"
     3.5  then use "RAW/ml_compiler_parameters_polyml-5.6.ML" else ();
     3.6  
     3.7 -use "RAW/use_context.ML";
     3.8  use "RAW/ml_positions.ML";
     3.9  use "RAW/compiler_polyml.ML";
    3.10  
    3.11 @@ -186,5 +185,5 @@
    3.12  (* ML debugger *)
    3.13  
    3.14  if ML_System.name = "polyml-5.6"
    3.15 -then use "RAW/ml_debugger_polyml-5.6.ML"
    3.16 -else use "RAW/ml_debugger.ML";
    3.17 +then use_no_debug "RAW/ml_debugger_polyml-5.6.ML"
    3.18 +else use_no_debug "RAW/ml_debugger.ML";
     4.1 --- a/src/Pure/RAW/compiler_polyml.ML	Tue Mar 01 17:26:53 2016 +0100
     4.2 +++ b/src/Pure/RAW/compiler_polyml.ML	Tue Mar 01 19:42:59 2016 +0100
     4.3 @@ -3,8 +3,20 @@
     4.4  Basic runtime compilation for Poly/ML (cf. Pure/ML/ml_compiler_polyml.ML).
     4.5  *)
     4.6  
     4.7 +type use_context =
     4.8 + {name_space: ML_Name_Space.T,
     4.9 +  str_of_pos: int -> string -> string,
    4.10 +  print: string -> unit,
    4.11 +  error: string -> unit};
    4.12 +
    4.13  local
    4.14  
    4.15 +val boot_context: use_context =
    4.16 + {name_space = ML_Name_Space.global,
    4.17 +  str_of_pos = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")",
    4.18 +  print = fn s => (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut),
    4.19 +  error = fn s => raise Fail s};
    4.20 +
    4.21  fun drop_newline s =
    4.22    if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
    4.23    else s;
    4.24 @@ -55,8 +67,22 @@
    4.25      val text = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    4.26    in use_text context {line = 1, file = file, verbose = verbose, debug = debug} text end;
    4.27  
    4.28 -fun use file =
    4.29 -  use_file boot_context {verbose = true, debug = false} file
    4.30 +
    4.31 +fun use_debug_option NONE = OS.Process.getEnv "ISABELLE_ML_DEBUGGER" = SOME "true"
    4.32 +  | use_debug_option (SOME debug) = debug;
    4.33 +
    4.34 +local
    4.35 +
    4.36 +fun use_ opt_debug file =
    4.37 +  use_file boot_context {verbose = true, debug = use_debug_option opt_debug} file
    4.38      handle Fail msg => (#print boot_context msg; raise Fail "ML error");
    4.39  
    4.40 +in
    4.41 +
    4.42 +val use = use_ NONE;
    4.43 +val use_debug = use_ (SOME true);
    4.44 +val use_no_debug = use_ (SOME false);
    4.45 +
    4.46  end;
    4.47 +
    4.48 +end;
     5.1 --- a/src/Pure/RAW/use_context.ML	Tue Mar 01 17:26:53 2016 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,17 +0,0 @@
     5.4 -(*  Title:      Pure/RAW/use_context.ML
     5.5 -    Author:     Makarius
     5.6 -
     5.7 -Common context for "use" operations (compiler invocation).
     5.8 -*)
     5.9 -
    5.10 -type use_context =
    5.11 - {name_space: ML_Name_Space.T,
    5.12 -  str_of_pos: int -> string -> string,
    5.13 -  print: string -> unit,
    5.14 -  error: string -> unit};
    5.15 -
    5.16 -val boot_context: use_context =
    5.17 - {name_space = ML_Name_Space.global,
    5.18 -  str_of_pos = fn line => fn file => " (line " ^ Int.toString line ^ " of \"" ^ file ^ "\")",
    5.19 -  print = fn s => (TextIO.output (TextIO.stdOut, s ^ "\n"); TextIO.flushOut TextIO.stdOut),
    5.20 -  error = fn s => raise Fail s};
     6.1 --- a/src/Pure/ROOT	Tue Mar 01 17:26:53 2016 +0100
     6.2 +++ b/src/Pure/ROOT	Tue Mar 01 19:42:59 2016 +0100
     6.3 @@ -30,7 +30,6 @@
     6.4      "RAW/multithreading.ML"
     6.5      "RAW/single_assignment_polyml.ML"
     6.6      "RAW/unsynchronized.ML"
     6.7 -    "RAW/use_context.ML"
     6.8  
     6.9  session Pure =
    6.10    global_theories Pure
    6.11 @@ -62,7 +61,6 @@
    6.12      "RAW/multithreading.ML"
    6.13      "RAW/single_assignment_polyml.ML"
    6.14      "RAW/unsynchronized.ML"
    6.15 -    "RAW/use_context.ML"
    6.16  
    6.17      "Concurrent/bash.ML"
    6.18      "Concurrent/bash_windows.ML"
     7.1 --- a/src/Pure/ROOT.ML	Tue Mar 01 17:26:53 2016 +0100
     7.2 +++ b/src/Pure/ROOT.ML	Tue Mar 01 19:42:59 2016 +0100
     7.3 @@ -39,11 +39,18 @@
     7.4  val use_text = Secure.use_text;
     7.5  val use_file = Secure.use_file;
     7.6  
     7.7 -fun use file =
     7.8 -  Position.setmp_thread_data (Position.file_only file)
     7.9 -    (fn () =>
    7.10 -      Secure.use_file ML_Parse.global_context {verbose = true, debug = false} file
    7.11 +local
    7.12 +  fun use_ opt_debug file =
    7.13 +    Position.setmp_thread_data (Position.file_only file)
    7.14 +      (fn () =>
    7.15 +        Secure.use_file ML_Parse.global_context
    7.16 +          {verbose = true, debug = use_debug_option opt_debug} file
    7.17          handle ERROR msg => (writeln msg; error "ML error")) ();
    7.18 +in
    7.19 +  val use = use_ NONE;
    7.20 +  val use_debug = use_ (SOME true);
    7.21 +  val use_no_debug = use_ (SOME false);
    7.22 +end;
    7.23  
    7.24  
    7.25  
    7.26 @@ -223,9 +230,19 @@
    7.27  use "ML/ml_context.ML";
    7.28  use "ML/ml_antiquotation.ML";
    7.29  
    7.30 -fun use s =
    7.31 -  ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode s)
    7.32 -    handle ERROR msg => (writeln msg; error "ML error");
    7.33 +local
    7.34 +  fun use_ opt_debug file =
    7.35 +    let val flags = ML_Compiler.debug_flags opt_debug |> ML_Compiler.verbose true in
    7.36 +      ML_Context.eval_file flags (Path.explode file)
    7.37 +        handle ERROR msg => (writeln msg; error "ML error")
    7.38 +    end;
    7.39 +in
    7.40 +
    7.41 +val use = use_ NONE;
    7.42 +val use_debug = use_ (SOME true);
    7.43 +val use_no_debug = use_ (SOME false);
    7.44 +
    7.45 +end;
    7.46  
    7.47  
    7.48  
     8.1 --- a/src/Pure/Tools/build.scala	Tue Mar 01 17:26:53 2016 +0100
     8.2 +++ b/src/Pure/Tools/build.scala	Tue Mar 01 19:42:59 2016 +0100
     8.3 @@ -567,9 +567,15 @@
     8.4          }))
     8.5  
     8.6      private val env =
     8.7 -      Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output_standard_path,
     8.8 -        (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") ->
     8.9 -          File.standard_path(args_file))
    8.10 +    {
    8.11 +      val env0 =
    8.12 +        Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> output_standard_path,
    8.13 +          (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") ->
    8.14 +            File.standard_path(args_file))
    8.15 +      if (is_pure(name))
    8.16 +        env0 + ("ISABELLE_ML_DEBUGGER" -> info.options.bool("ML_debugger").toString)
    8.17 +      else env0
    8.18 +    }
    8.19  
    8.20      private val script =
    8.21        """