proper configuration option "ML_print_depth";
authorwenzelm
Tue Mar 25 19:03:02 2014 +0100 (2014-03-25)
changeset 5628103c3d1a7c3b8
parent 56280 f7de8392a507
child 56282 13f33298caa9
proper configuration option "ML_print_depth";
proper ML_exception_trace for HOL-TPTP;
NEWS
src/Doc/IsarRef/Inner_Syntax.thy
src/HOL/Metis.thy
src/HOL/TPTP/TPTP_Parser/make_mlyacclib
src/HOL/TPTP/TPTP_Parser/ml_yacc_lib.ML
src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML
src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy
src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy
src/Pure/Isar/attrib.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/ML/ml_compiler.ML
src/Pure/ML/ml_compiler_polyml.ML
src/Pure/ROOT.ML
src/Pure/Tools/proof_general_pure.ML
src/Tools/Metis/make_metis
src/Tools/Metis/metis.ML
     1.1 --- a/NEWS	Tue Mar 25 17:59:34 2014 +0100
     1.2 +++ b/NEWS	Tue Mar 25 19:03:02 2014 +0100
     1.3 @@ -545,8 +545,13 @@
     1.4  "ML_exception_trace", which may be also declared within the context via
     1.5  "declare [[ML_exception_trace = true]]".  Minor INCOMPATIBILITY.
     1.6  
     1.7 -* Renamed option "ML_trace" to "ML_source_trace". Minor
     1.8 -INCOMPATIBILITY.
     1.9 +* Renamed configuration option "ML_trace" to "ML_source_trace". Minor
    1.10 +INCOMPATIBILITY.
    1.11 +
    1.12 +* Configuration option "ML_print_depth" controls the pretty-printing
    1.13 +depth of the ML compiler within the context.  The old print_depth in
    1.14 +ML is still available as put_default_print_depth, but rarely used.
    1.15 +Minor INCOMPATIBILITY.
    1.16  
    1.17  * Proper context discipline for read_instantiate and instantiate_tac:
    1.18  variables that are meant to become schematic need to be given as
     2.1 --- a/src/Doc/IsarRef/Inner_Syntax.thy	Tue Mar 25 17:59:34 2014 +0100
     2.2 +++ b/src/Doc/IsarRef/Inner_Syntax.thy	Tue Mar 25 19:03:02 2014 +0100
     2.3 @@ -320,10 +320,11 @@
     2.4  text {*
     2.5    \begin{mldecls}
     2.6      @{index_ML Pretty.margin_default: "int Unsynchronized.ref"} \\
     2.7 -    @{index_ML print_depth: "int -> unit"} \\
     2.8    \end{mldecls}
     2.9  
    2.10 -  These ML functions set limits for pretty printed text.
    2.11 +  \begin{tabular}{rcll}
    2.12 +    @{attribute_def ML_print_depth} & : & @{text attribute} & default 10 \\ %FIXME move?
    2.13 +  \end{tabular}
    2.14  
    2.15    \begin{description}
    2.16  
    2.17 @@ -334,9 +335,9 @@
    2.18    engine of Isabelle/ML altogether and do it within the front end via
    2.19    Isabelle/Scala.
    2.20  
    2.21 -  \item @{ML print_depth}~@{text n} limits the printing depth of the
    2.22 +  \item @{attribute ML_print_depth} limits the printing depth of the
    2.23    ML toplevel pretty printer; the precise effect depends on the ML
    2.24 -  compiler and run-time system.  Typically @{text n} should be less
    2.25 +  compiler and run-time system.  Typically the limit should be less
    2.26    than 10.  Bigger values such as 100--1000 are useful for debugging.
    2.27  
    2.28    \end{description}
     3.1 --- a/src/HOL/Metis.thy	Tue Mar 25 17:59:34 2014 +0100
     3.2 +++ b/src/HOL/Metis.thy	Tue Mar 25 19:03:02 2014 +0100
     3.3 @@ -10,7 +10,9 @@
     3.4  imports ATP
     3.5  begin
     3.6  
     3.7 +declare [[ML_print_depth = 0]]
     3.8  ML_file "~~/src/Tools/Metis/metis.ML"
     3.9 +declare [[ML_print_depth = 10]]
    3.10  
    3.11  subsection {* Literal selection and lambda-lifting helpers *}
    3.12  
     4.1 --- a/src/HOL/TPTP/TPTP_Parser/make_mlyacclib	Tue Mar 25 17:59:34 2014 +0100
     4.2 +++ b/src/HOL/TPTP/TPTP_Parser/make_mlyacclib	Tue Mar 25 19:03:02 2014 +0100
     4.3 @@ -20,8 +20,6 @@
     4.4  (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
     4.5  (******************************************************************)
     4.6  
     4.7 -print_depth 0;
     4.8 -
     4.9  (*
    4.10    This file is generated from the contents of ML-Yacc's lib directory.
    4.11    ML-Yacc's COPYRIGHT-file contents follow:
    4.12 @@ -48,7 +46,6 @@
    4.13  
    4.14    cat <<EOF
    4.15  ;
    4.16 -print_depth 10;
    4.17  EOF
    4.18  
    4.19  ) > ml_yacc_lib.ML
    4.20 \ No newline at end of file
     5.1 --- a/src/HOL/TPTP/TPTP_Parser/ml_yacc_lib.ML	Tue Mar 25 17:59:34 2014 +0100
     5.2 +++ b/src/HOL/TPTP/TPTP_Parser/ml_yacc_lib.ML	Tue Mar 25 19:03:02 2014 +0100
     5.3 @@ -5,8 +5,6 @@
     5.4  (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
     5.5  (******************************************************************)
     5.6  
     5.7 -print_depth 0;
     5.8 -
     5.9  (*
    5.10    This file is generated from the contents of ML-Yacc's lib directory.
    5.11    ML-Yacc's COPYRIGHT-file contents follow:
    5.12 @@ -1061,4 +1059,3 @@
    5.13   end;
    5.14  
    5.15  ;
    5.16 -print_depth 10;
     6.1 --- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Tue Mar 25 17:59:34 2014 +0100
     6.2 +++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML	Tue Mar 25 19:03:02 2014 +0100
     6.3 @@ -285,7 +285,7 @@
     6.4  
     6.5  type tptp_problem = tptp_line list
     6.6  
     6.7 -fun debug f x = if Options.default_bool @{option exception_trace} then (f x; ()) else ()
     6.8 +fun debug f x = if Options.default_bool @{option ML_exception_trace} then (f x; ()) else ()
     6.9  
    6.10  fun nameof_tff_atom_type (Atom_type str) = str
    6.11    | nameof_tff_atom_type _ = raise TPTP_SYNTAX "nameof_tff_atom_type called on non-atom type"
     7.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Tue Mar 25 17:59:34 2014 +0100
     7.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy	Tue Mar 25 19:03:02 2014 +0100
     7.3 @@ -42,8 +42,8 @@
     7.4  ML {*
     7.5    if test_all @{context} then ()
     7.6    else
     7.7 -    (Options.default_put_bool @{option exception_trace} true;
     7.8 -     PolyML.print_depth 200;
     7.9 +    (Options.default_put_bool @{option ML_exception_trace} true;
    7.10 +     put_default_print_depth 200;  (* FIXME proper ML_print_depth within context!? *)
    7.11       PolyML.Compiler.maxInlineSize := 0)
    7.12  *}
    7.13  
    7.14 @@ -186,8 +186,9 @@
    7.15       prob_names;
    7.16  *}
    7.17  
    7.18 +declare [[ML_print_depth = 2000]]
    7.19 +
    7.20  ML {*
    7.21 -print_depth 2000;
    7.22  the_tactics
    7.23  |> map (filter (fn (_, _, x) => is_none x)
    7.24          #> map (fn (x, SOME y, _) => (x, cterm_of @{theory} y)))
     8.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy	Tue Mar 25 17:59:34 2014 +0100
     8.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy	Tue Mar 25 19:03:02 2014 +0100
     8.3 @@ -11,9 +11,8 @@
     8.4  imports TPTP_Test TPTP_Proof_Reconstruction
     8.5  begin
     8.6  
     8.7 -declare [[exception_trace]]
     8.8 +declare [[ML_exception_trace, ML_print_depth = 200]]
     8.9  ML {*
    8.10 -print_depth 200;
    8.11  PolyML.Compiler.maxInlineSize := 0;
    8.12  (* FIXME doesn't work with Isabelle?
    8.13     PolyML.Compiler.debug := true *)
    8.14 @@ -2025,8 +2024,7 @@
    8.15  
    8.16  (*SYN044^4*)
    8.17  (*
    8.18 -ML {*
    8.19 -print_depth 1400;
    8.20 +declare [[ML_print_depth = 1400]]
    8.21  (* the_tactics *)
    8.22  *}
    8.23  
     9.1 --- a/src/Pure/Isar/attrib.ML	Tue Mar 25 17:59:34 2014 +0100
     9.2 +++ b/src/Pure/Isar/attrib.ML	Tue Mar 25 19:03:02 2014 +0100
     9.3 @@ -458,6 +458,7 @@
     9.4    register_config Name_Space.names_short_raw #>
     9.5    register_config Name_Space.names_unique_raw #>
     9.6    register_config ML_Context.source_trace_raw #>
     9.7 +  register_config ML_Compiler.print_depth_raw #>
     9.8    register_config Runtime.exception_trace_raw #>
     9.9    register_config Proof_Context.show_abbrevs_raw #>
    9.10    register_config Goal_Display.goals_limit_raw #>
    10.1 --- a/src/Pure/ML-Systems/polyml.ML	Tue Mar 25 17:59:34 2014 +0100
    10.2 +++ b/src/Pure/ML-Systems/polyml.ML	Tue Mar 25 19:03:02 2014 +0100
    10.3 @@ -130,8 +130,9 @@
    10.4  local
    10.5    val depth = Unsynchronized.ref 10;
    10.6  in
    10.7 -  fun get_print_depth () = ! depth;
    10.8 -  fun print_depth n = (depth := n; PolyML.print_depth n);
    10.9 +  fun get_default_print_depth () = ! depth;
   10.10 +  fun put_default_print_depth n = (depth := n; PolyML.print_depth n);
   10.11 +  val _ = put_default_print_depth 10;
   10.12  end;
   10.13  
   10.14  val error_depth = PolyML.error_depth;
   10.15 @@ -175,5 +176,5 @@
   10.16      ("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
   10.17  
   10.18  val ml_make_string =
   10.19 -  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, get_print_depth ())))))";
   10.20 +  "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, ML_Compiler.get_print_depth ())))))";
   10.21  
    11.1 --- a/src/Pure/ML-Systems/smlnj.ML	Tue Mar 25 17:59:34 2014 +0100
    11.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Tue Mar 25 19:03:02 2014 +0100
    11.3 @@ -56,11 +56,12 @@
    11.4  local
    11.5    val depth = ref (10: int);
    11.6  in
    11.7 -  fun get_print_depth () = ! depth;
    11.8 -  fun print_depth n =
    11.9 +  fun get_default_print_depth () = ! depth;
   11.10 +  fun put_default_print_depth n =
   11.11     (depth := n;
   11.12      Control.Print.printDepth := dest_int n div 2;
   11.13      Control.Print.printLength := dest_int n);
   11.14 +  val _ = put_default_print_depth 10;
   11.15  end;
   11.16  
   11.17  val ml_make_string = "(fn _ => \"?\")";
    12.1 --- a/src/Pure/ML/ml_compiler.ML	Tue Mar 25 17:59:34 2014 +0100
    12.2 +++ b/src/Pure/ML/ml_compiler.ML	Tue Mar 25 19:03:02 2014 +0100
    12.3 @@ -11,6 +11,9 @@
    12.4    val exn_message: exn -> string
    12.5    val exn_error_message: exn -> unit
    12.6    val exn_trace: (unit -> 'a) -> 'a
    12.7 +  val print_depth_raw: Config.raw
    12.8 +  val print_depth: int Config.T
    12.9 +  val get_print_depth: unit -> int
   12.10    type flags = {SML: bool, verbose: bool}
   12.11    val eval: flags -> Position.T -> ML_Lex.token list -> unit
   12.12  end
   12.13 @@ -18,6 +21,8 @@
   12.14  structure ML_Compiler: ML_COMPILER =
   12.15  struct
   12.16  
   12.17 +(* exceptions *)
   12.18 +
   12.19  val exn_info =
   12.20   {exn_position = fn _: exn => Position.none,
   12.21    pretty_exn = Pretty.str o General.exnMessage};
   12.22 @@ -29,6 +34,21 @@
   12.23  val exn_error_message = Output.error_message o exn_message;
   12.24  fun exn_trace e = print_exception_trace exn_message e;
   12.25  
   12.26 +
   12.27 +(* print depth *)
   12.28 +
   12.29 +val print_depth_raw =
   12.30 +  Config.declare "ML_print_depth" (fn _ => Config.Int (get_default_print_depth ()));
   12.31 +val print_depth = Config.int print_depth_raw;
   12.32 +
   12.33 +fun get_print_depth () =
   12.34 +  (case Context.thread_data () of
   12.35 +    NONE => get_default_print_depth ()
   12.36 +  | SOME context => Config.get_generic context print_depth);
   12.37 +
   12.38 +
   12.39 +(* eval *)
   12.40 +
   12.41  type flags = {SML: bool, verbose: bool};
   12.42  
   12.43  fun eval {SML, verbose} pos toks =
    13.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Tue Mar 25 17:59:34 2014 +0100
    13.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Tue Mar 25 19:03:02 2014 +0100
    13.3 @@ -7,6 +7,9 @@
    13.4  structure ML_Compiler: ML_COMPILER =
    13.5  struct
    13.6  
    13.7 +open ML_Compiler;
    13.8 +
    13.9 +
   13.10  (* source locations *)
   13.11  
   13.12  fun position_of (loc: PolyML.location) =
   13.13 @@ -74,8 +77,6 @@
   13.14  
   13.15  (* eval ML source tokens *)
   13.16  
   13.17 -type flags = {SML: bool, verbose: bool};
   13.18 -
   13.19  fun eval {SML, verbose} pos toks =
   13.20    let
   13.21      val _ = Secure.secure_mltext ();
   13.22 @@ -184,6 +185,7 @@
   13.23        PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
   13.24        PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
   13.25        PolyML.Compiler.CPFileName location_props,
   13.26 +      PolyML.Compiler.CPPrintDepth get_print_depth,
   13.27        PolyML.Compiler.CPCompilerResultFun result_fun,
   13.28        PolyML.Compiler.CPPrintInAlphabeticalOrder false];
   13.29      val _ =
    14.1 --- a/src/Pure/ROOT.ML	Tue Mar 25 17:59:34 2014 +0100
    14.2 +++ b/src/Pure/ROOT.ML	Tue Mar 25 19:03:02 2014 +0100
    14.3 @@ -6,8 +6,6 @@
    14.4    val is_official = false;
    14.5  end;
    14.6  
    14.7 -print_depth 10;
    14.8 -
    14.9  
   14.10  (* library of general tools *)
   14.11  
    15.1 --- a/src/Pure/Tools/proof_general_pure.ML	Tue Mar 25 17:59:34 2014 +0100
    15.2 +++ b/src/Pure/Tools/proof_general_pure.ML	Tue Mar 25 19:03:02 2014 +0100
    15.3 @@ -76,8 +76,8 @@
    15.4  val _ =
    15.5    ProofGeneral.preference ProofGeneral.category_advanced_display
    15.6      NONE
    15.7 -    (Markup.print_int o get_print_depth)
    15.8 -    (print_depth o Markup.parse_int)
    15.9 +    (Markup.print_int o get_default_print_depth)
   15.10 +    (put_default_print_depth o Markup.parse_int)
   15.11      ProofGeneral.pgipint
   15.12      "print-depth"
   15.13      "Setting for the ML print depth";
    16.1 --- a/src/Tools/Metis/make_metis	Tue Mar 25 17:59:34 2014 +0100
    16.2 +++ b/src/Tools/Metis/make_metis	Tue Mar 25 19:03:02 2014 +0100
    16.3 @@ -28,8 +28,6 @@
    16.4  (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
    16.5  (******************************************************************)
    16.6  
    16.7 -print_depth 0;
    16.8 -
    16.9  EOF
   16.10  
   16.11    for FILE in $FILES
   16.12 @@ -51,7 +49,6 @@
   16.13  
   16.14    cat <<EOF
   16.15  ;
   16.16 -print_depth 10;
   16.17  EOF
   16.18  
   16.19  ) > metis.ML
    17.1 --- a/src/Tools/Metis/metis.ML	Tue Mar 25 17:59:34 2014 +0100
    17.2 +++ b/src/Tools/Metis/metis.ML	Tue Mar 25 19:03:02 2014 +0100
    17.3 @@ -14,8 +14,6 @@
    17.4  (* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
    17.5  (******************************************************************)
    17.6  
    17.7 -print_depth 0;
    17.8 -
    17.9  
   17.10  (**** Original file: src/Random.sig ****)
   17.11  
   17.12 @@ -21462,4 +21460,3 @@
   17.13  
   17.14  end
   17.15  ;
   17.16 -print_depth 10;