support for ML files with/without debugger information;
authorwenzelm
Mon Aug 17 19:34:15 2015 +0200 (2015-08-17)
changeset 60957574254152856
parent 60956 10d463883dc2
child 60958 5d70b5c509f8
support for ML files with/without debugger information;
src/Pure/Isar/isar_syn.ML
src/Pure/ML/ml_file.ML
src/Pure/Pure.thy
src/Pure/ROOT.ML
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_header.scala
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Aug 17 16:27:12 2015 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Aug 17 19:34:15 2015 +0200
     1.3 @@ -203,19 +203,31 @@
     1.4  
     1.5  (* use ML text *)
     1.6  
     1.7 +fun SML_file_cmd debug files = Toplevel.theory (fn thy =>
     1.8 +  let
     1.9 +    val ([{lines, pos, ...}: Token.file], thy') = files thy;
    1.10 +    val source = Input.source true (cat_lines lines) (pos, pos);
    1.11 +    val flags: ML_Compiler.flags =
    1.12 +      {SML = true, exchange = false, redirect = true, verbose = true,
    1.13 +        debug = debug, writeln = writeln, warning = warning};
    1.14 +  in
    1.15 +    thy' |> Context.theory_map
    1.16 +      (ML_Context.exec (fn () => ML_Context.eval_source flags source))
    1.17 +  end);
    1.18 +
    1.19  val _ =
    1.20    Outer_Syntax.command @{command_keyword SML_file} "read and evaluate Standard ML file"
    1.21 -    (Resources.provide_parse_files "SML_file" >> (fn files => Toplevel.theory (fn thy =>
    1.22 -        let
    1.23 -          val ([{lines, pos, ...}], thy') = files thy;
    1.24 -          val source = Input.source true (cat_lines lines) (pos, pos);
    1.25 -          val flags: ML_Compiler.flags =
    1.26 -            {SML = true, exchange = false, redirect = true, verbose = true,
    1.27 -              debug = NONE, writeln = writeln, warning = warning};
    1.28 -        in
    1.29 -          thy' |> Context.theory_map
    1.30 -            (ML_Context.exec (fn () => ML_Context.eval_source flags source))
    1.31 -        end)));
    1.32 +    (Resources.provide_parse_files "SML_file" >> SML_file_cmd NONE);
    1.33 +
    1.34 +val _ =
    1.35 +  Outer_Syntax.command @{command_keyword SML_file_debug}
    1.36 +    "read and evaluate Standard ML file (with debugger information)"
    1.37 +    (Resources.provide_parse_files "SML_file_debug" >> SML_file_cmd (SOME true));
    1.38 +
    1.39 +val _ =
    1.40 +  Outer_Syntax.command @{command_keyword SML_file_no_debug}
    1.41 +    "read and evaluate Standard ML file (no debugger information)"
    1.42 +    (Resources.provide_parse_files "SML_file_no_debug" >> SML_file_cmd (SOME false));
    1.43  
    1.44  val _ =
    1.45    Outer_Syntax.command @{command_keyword SML_export} "evaluate SML within Isabelle/ML environment"
     2.1 --- a/src/Pure/ML/ml_file.ML	Mon Aug 17 16:27:12 2015 +0200
     2.2 +++ b/src/Pure/ML/ml_file.ML	Mon Aug 17 19:34:15 2015 +0200
     2.3 @@ -7,21 +7,33 @@
     2.4  structure ML_File: sig end =
     2.5  struct
     2.6  
     2.7 +fun ML_file_cmd debug files = Toplevel.generic_theory (fn gthy =>
     2.8 +  let
     2.9 +    val [{src_path, lines, digest, pos}: Token.file] = files (Context.theory_of gthy);
    2.10 +    val provide = Resources.provide (src_path, digest);
    2.11 +    val source = Input.source true (cat_lines lines) (pos, pos);
    2.12 +    val flags: ML_Compiler.flags =
    2.13 +      {SML = false, exchange = false, redirect = true, verbose = true,
    2.14 +        debug = debug, writeln = writeln, warning = warning};
    2.15 +  in
    2.16 +    gthy
    2.17 +    |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
    2.18 +    |> Local_Theory.propagate_ml_env
    2.19 +    |> Context.mapping provide (Local_Theory.background_theory provide)
    2.20 +  end);
    2.21 +
    2.22  val _ =
    2.23 -  Outer_Syntax.command ("ML_file", @{here}) "ML text from file"
    2.24 -    (Resources.parse_files "ML_file" >> (fn files => Toplevel.generic_theory (fn gthy =>
    2.25 -        let
    2.26 -          val [{src_path, lines, digest, pos}] = files (Context.theory_of gthy);
    2.27 -          val provide = Resources.provide (src_path, digest);
    2.28 -          val source = Input.source true (cat_lines lines) (pos, pos);
    2.29 -          val flags: ML_Compiler.flags =
    2.30 -            {SML = false, exchange = false, redirect = true, verbose = true,
    2.31 -              debug = NONE, writeln = writeln, warning = warning};
    2.32 -        in
    2.33 -          gthy
    2.34 -          |> ML_Context.exec (fn () => ML_Context.eval_source flags source)
    2.35 -          |> Local_Theory.propagate_ml_env
    2.36 -          |> Context.mapping provide (Local_Theory.background_theory provide)
    2.37 -        end)));
    2.38 +  Outer_Syntax.command ("ML_file", @{here}) "read and evaluate Isabelle/ML file"
    2.39 +    (Resources.parse_files "ML_file" >> ML_file_cmd NONE);
    2.40 +
    2.41 +val _ =
    2.42 +  Outer_Syntax.command ("ML_file_debug", @{here})
    2.43 +    "read and evaluate Isabelle/ML file (with debugger information)"
    2.44 +    (Resources.parse_files "ML_file_debug" >> ML_file_cmd (SOME true));
    2.45 +
    2.46 +val _ =
    2.47 +  Outer_Syntax.command ("ML_file_no_debug", @{here})
    2.48 +    "read and evaluate Isabelle/ML file (no debugger information)"
    2.49 +    (Resources.parse_files "ML_file_no_debug" >> ML_file_cmd (SOME false));
    2.50  
    2.51  end;
     3.1 --- a/src/Pure/Pure.thy	Mon Aug 17 16:27:12 2015 +0200
     3.2 +++ b/src/Pure/Pure.thy	Mon Aug 17 19:34:15 2015 +0200
     3.3 @@ -21,7 +21,7 @@
     3.4      "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
     3.5      "no_notation" "axiomatization" "theorems" "lemmas" "declare"
     3.6      "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
     3.7 -  and "SML_file" :: thy_load % "ML"
     3.8 +  and "SML_file" "SML_file_debug" "SML_file_no_debug" :: thy_load % "ML"
     3.9    and "SML_import" "SML_export" :: thy_decl % "ML"
    3.10    and "ML" :: thy_decl % "ML"
    3.11    and "ML_prf" :: prf_decl % "proof"  (* FIXME % "ML" ?? *)
     4.1 --- a/src/Pure/ROOT.ML	Mon Aug 17 16:27:12 2015 +0200
     4.2 +++ b/src/Pure/ROOT.ML	Mon Aug 17 19:34:15 2015 +0200
     4.3 @@ -41,11 +41,23 @@
     4.4  val use_text = Secure.use_text;
     4.5  val use_file = Secure.use_file;
     4.6  
     4.7 -fun use file =
     4.8 -  Position.setmp_thread_data (Position.file_only file)
     4.9 -    (fn () =>
    4.10 -      Secure.use_file ML_Parse.global_context {verbose = true, debug = false} file
    4.11 -        handle ERROR msg => (writeln msg; error "ML error")) ();
    4.12 +fun use_fns default_debug_option =
    4.13 +  let
    4.14 +    fun use_ debug_option file =
    4.15 +      let
    4.16 +        val debug =
    4.17 +          (case debug_option of
    4.18 +            SOME debug => debug
    4.19 +          | NONE => default_debug_option ());
    4.20 +      in
    4.21 +        Position.setmp_thread_data (Position.file_only file)
    4.22 +          (fn () =>
    4.23 +            Secure.use_file ML_Parse.global_context {verbose = true, debug = debug} file
    4.24 +              handle ERROR msg => (writeln msg; error "ML error")) ()
    4.25 +      end;
    4.26 +  in {use = use_ NONE, use_debug = use_ (SOME true), use_no_debug = use_ (SOME false)} end;
    4.27 +
    4.28 +val {use, use_debug, use_no_debug} = use_fns (K false);
    4.29  
    4.30  val toplevel_pp = Secure.toplevel_pp;
    4.31  
    4.32 @@ -95,6 +107,8 @@
    4.33  use "System/options.ML";
    4.34  use "config.ML";
    4.35  
    4.36 +val {use, use_debug, use_no_debug} = use_fns (fn () => Options.default_bool "ML_debugger");
    4.37 +
    4.38  
    4.39  (* concurrency within the ML runtime *)
    4.40  
    4.41 @@ -204,6 +218,10 @@
    4.42  use "ML/ml_syntax.ML";
    4.43  use "ML/ml_env.ML";
    4.44  use "ML/ml_options.ML";
    4.45 +
    4.46 +val {use, use_debug, use_no_debug} =
    4.47 +  use_fns (fn () => ML_Options.debugger_enabled (Context.thread_data ()));
    4.48 +
    4.49  use "ML/exn_output.ML";
    4.50  if ML_System.is_polyml then use "ML/exn_output_polyml.ML" else ();
    4.51  use "ML/ml_options.ML";
    4.52 @@ -244,9 +262,21 @@
    4.53  use "ML/ml_context.ML";
    4.54  use "ML/ml_antiquotation.ML";
    4.55  
    4.56 -fun use s =
    4.57 -  ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode s)
    4.58 -    handle ERROR msg => (writeln msg; error "ML error");
    4.59 +local
    4.60 +  fun use_ debug file =
    4.61 +    let
    4.62 +      val flags =
    4.63 +        {SML = false, exchange = false, redirect = false, verbose = true,
    4.64 +          debug = debug, writeln = writeln, warning = warning};
    4.65 +    in
    4.66 +      ML_Context.eval_file (ML_Compiler.verbose true ML_Compiler.flags) (Path.explode file)
    4.67 +        handle ERROR msg => (writeln msg; error "ML error")
    4.68 +    end
    4.69 +in
    4.70 +  val use = use_ NONE;
    4.71 +  val use_debug = use_ (SOME true);
    4.72 +  val use_no_debug = use_ (SOME false);
    4.73 +end;
    4.74  
    4.75  
    4.76  
    4.77 @@ -377,4 +407,3 @@
    4.78  val cd = File.cd o Path.explode;
    4.79  
    4.80  Proofterm.proofs := 0;
    4.81 -
     5.1 --- a/src/Pure/Thy/thy_header.ML	Mon Aug 17 16:27:12 2015 +0200
     5.2 +++ b/src/Pure/Thy/thy_header.ML	Mon Aug 17 19:34:15 2015 +0200
     5.3 @@ -78,7 +78,9 @@
     5.4       ((txtN, @{here}), SOME ((Keyword.document_body, []), [])),
     5.5       ((text_rawN, @{here}), SOME ((Keyword.document_raw, []), [])),
     5.6       ((theoryN, @{here}), SOME ((Keyword.thy_begin, []), ["theory"])),
     5.7 -     (("ML_file", @{here}), SOME ((Keyword.thy_load, []), ["ML"]))];
     5.8 +     (("ML_file", @{here}), SOME ((Keyword.thy_load, []), ["ML"])),
     5.9 +     (("ML_file_debug", @{here}), SOME ((Keyword.thy_load, []), ["ML"])),
    5.10 +     (("ML_file_no_debug", @{here}), SOME ((Keyword.thy_load, []), ["ML"]))];
    5.11  
    5.12  
    5.13  (* theory data *)
     6.1 --- a/src/Pure/Thy/thy_header.scala	Mon Aug 17 16:27:12 2015 +0200
     6.2 +++ b/src/Pure/Thy/thy_header.scala	Mon Aug 17 19:34:15 2015 +0200
     6.3 @@ -55,7 +55,9 @@
     6.4        (TXT, Some(((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
     6.5        (TEXT_RAW, Some(((Keyword.DOCUMENT_RAW, Nil), Nil)), None),
     6.6        (THEORY, Some((Keyword.THY_BEGIN, Nil), List("theory")), None),
     6.7 -      ("ML_file", Some((Keyword.THY_LOAD, Nil), List("ML")), None))
     6.8 +      ("ML_file", Some((Keyword.THY_LOAD, Nil), List("ML")), None),
     6.9 +      ("ML_file_debug", Some((Keyword.THY_LOAD, Nil), List("ML")), None),
    6.10 +      ("ML_file_no_debug", Some((Keyword.THY_LOAD, Nil), List("ML")), None))
    6.11  
    6.12    private val bootstrap_keywords =
    6.13      Keyword.Keywords.empty.add_keywords(bootstrap_header)