no ML_debugger support in Pure -- too complicated;
authorwenzelm
Mon Aug 17 21:32:41 2015 +0200 (2015-08-17)
changeset 609593565c9f407ec
parent 60958 5d70b5c509f8
child 60960 1fd5db0e2b34
no ML_debugger support in Pure -- too complicated;
src/Pure/ROOT.ML
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/ROOT.ML	Mon Aug 17 21:22:55 2015 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Mon Aug 17 21:32:41 2015 +0200
     1.3 @@ -41,24 +41,11 @@
     1.4  val use_text = Secure.use_text;
     1.5  val use_file = Secure.use_file;
     1.6  
     1.7 -local
     1.8 -  fun use_ debug_option file =
     1.9 -    let
    1.10 -      val debug =
    1.11 -        (case debug_option of
    1.12 -          SOME debug => debug
    1.13 -        | NONE => getenv "ISABELLE_ML_DEBUGGER" = "true");
    1.14 -    in
    1.15 -      Position.setmp_thread_data (Position.file_only file)
    1.16 -        (fn () =>
    1.17 -          Secure.use_file ML_Parse.global_context {verbose = true, debug = debug} file
    1.18 -            handle ERROR msg => (writeln msg; error "ML error")) ()
    1.19 -    end;
    1.20 -in
    1.21 -  val use = use_ NONE;
    1.22 -  val use_debug = use_ (SOME true);
    1.23 -  val use_no_debug = use_ (SOME false);
    1.24 -end;
    1.25 +fun use file =
    1.26 +  Position.setmp_thread_data (Position.file_only file)
    1.27 +    (fn () =>
    1.28 +      Secure.use_file ML_Parse.global_context {verbose = true, debug = false} file
    1.29 +        handle ERROR msg => (writeln msg; error "ML error")) ();
    1.30  
    1.31  val toplevel_pp = Secure.toplevel_pp;
    1.32  
    1.33 @@ -257,21 +244,9 @@
    1.34  use "ML/ml_context.ML";
    1.35  use "ML/ml_antiquotation.ML";
    1.36  
    1.37 -local
    1.38 -  fun use_ debug file =
    1.39 -    let
    1.40 -      val flags: ML_Compiler.flags =
    1.41 -        {SML = false, exchange = false, redirect = false, verbose = true,
    1.42 -          debug = debug, writeln = writeln, warning = warning};
    1.43 -    in
    1.44 -      ML_Context.eval_file flags (Path.explode file)
    1.45 -        handle ERROR msg => (writeln msg; error "ML error")
    1.46 -    end;
    1.47 -in
    1.48 -  val use = use_ NONE;
    1.49 -  val use_debug = use_ (SOME true);
    1.50 -  val use_no_debug = use_ (SOME false);
    1.51 -end;
    1.52 +fun use s =
    1.53 +  ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode s)
    1.54 +    handle ERROR msg => (writeln msg; error "ML error");
    1.55  
    1.56  
    1.57  
     2.1 --- a/src/Pure/Tools/build.scala	Mon Aug 17 21:22:55 2015 +0200
     2.2 +++ b/src/Pure/Tools/build.scala	Mon Aug 17 21:32:41 2015 +0200
     2.3 @@ -590,16 +590,11 @@
     2.4                  (info.chapter, (name, theories)))))))))))
     2.5          }))
     2.6  
     2.7 -    private val env0 =
     2.8 +    private val env =
     2.9        Map("INPUT" -> parent, "TARGET" -> name, "OUTPUT" -> Isabelle_System.standard_path(output),
    2.10          (if (is_pure(name)) "ISABELLE_PROCESS_OPTIONS" else "ARGS_FILE") ->
    2.11            Isabelle_System.posix_path(args_file))
    2.12  
    2.13 -    private val env =
    2.14 -      if (is_pure(name))
    2.15 -        env0 + ("ISABELLE_ML_DEBUGGER" -> info.options.bool("ML_debugger").toString)
    2.16 -      else env0
    2.17 -
    2.18      private val script =
    2.19        if (is_pure(name)) {
    2.20          if (do_output) "./build " + name + " \"$OUTPUT\""