proper configuration option "ML_print_depth";
proper ML_exception_trace for HOL-TPTP;
--- a/NEWS Tue Mar 25 17:59:34 2014 +0100
+++ b/NEWS Tue Mar 25 19:03:02 2014 +0100
@@ -545,8 +545,13 @@
"ML_exception_trace", which may be also declared within the context via
"declare [[ML_exception_trace = true]]". Minor INCOMPATIBILITY.
-* Renamed option "ML_trace" to "ML_source_trace". Minor
-INCOMPATIBILITY.
+* Renamed configuration option "ML_trace" to "ML_source_trace". Minor
+INCOMPATIBILITY.
+
+* Configuration option "ML_print_depth" controls the pretty-printing
+depth of the ML compiler within the context. The old print_depth in
+ML is still available as put_default_print_depth, but rarely used.
+Minor INCOMPATIBILITY.
* Proper context discipline for read_instantiate and instantiate_tac:
variables that are meant to become schematic need to be given as
--- a/src/Doc/IsarRef/Inner_Syntax.thy Tue Mar 25 17:59:34 2014 +0100
+++ b/src/Doc/IsarRef/Inner_Syntax.thy Tue Mar 25 19:03:02 2014 +0100
@@ -320,10 +320,11 @@
text {*
\begin{mldecls}
@{index_ML Pretty.margin_default: "int Unsynchronized.ref"} \\
- @{index_ML print_depth: "int -> unit"} \\
\end{mldecls}
- These ML functions set limits for pretty printed text.
+ \begin{tabular}{rcll}
+ @{attribute_def ML_print_depth} & : & @{text attribute} & default 10 \\ %FIXME move?
+ \end{tabular}
\begin{description}
@@ -334,9 +335,9 @@
engine of Isabelle/ML altogether and do it within the front end via
Isabelle/Scala.
- \item @{ML print_depth}~@{text n} limits the printing depth of the
+ \item @{attribute ML_print_depth} limits the printing depth of the
ML toplevel pretty printer; the precise effect depends on the ML
- compiler and run-time system. Typically @{text n} should be less
+ compiler and run-time system. Typically the limit should be less
than 10. Bigger values such as 100--1000 are useful for debugging.
\end{description}
--- a/src/HOL/Metis.thy Tue Mar 25 17:59:34 2014 +0100
+++ b/src/HOL/Metis.thy Tue Mar 25 19:03:02 2014 +0100
@@ -10,7 +10,9 @@
imports ATP
begin
+declare [[ML_print_depth = 0]]
ML_file "~~/src/Tools/Metis/metis.ML"
+declare [[ML_print_depth = 10]]
subsection {* Literal selection and lambda-lifting helpers *}
--- a/src/HOL/TPTP/TPTP_Parser/make_mlyacclib Tue Mar 25 17:59:34 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/make_mlyacclib Tue Mar 25 19:03:02 2014 +0100
@@ -20,8 +20,6 @@
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
(******************************************************************)
-print_depth 0;
-
(*
This file is generated from the contents of ML-Yacc's lib directory.
ML-Yacc's COPYRIGHT-file contents follow:
@@ -48,7 +46,6 @@
cat <<EOF
;
-print_depth 10;
EOF
) > ml_yacc_lib.ML
\ No newline at end of file
--- a/src/HOL/TPTP/TPTP_Parser/ml_yacc_lib.ML Tue Mar 25 17:59:34 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/ml_yacc_lib.ML Tue Mar 25 19:03:02 2014 +0100
@@ -5,8 +5,6 @@
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
(******************************************************************)
-print_depth 0;
-
(*
This file is generated from the contents of ML-Yacc's lib directory.
ML-Yacc's COPYRIGHT-file contents follow:
@@ -1061,4 +1059,3 @@
end;
;
-print_depth 10;
--- a/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML Tue Mar 25 17:59:34 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML Tue Mar 25 19:03:02 2014 +0100
@@ -285,7 +285,7 @@
type tptp_problem = tptp_line list
-fun debug f x = if Options.default_bool @{option exception_trace} then (f x; ()) else ()
+fun debug f x = if Options.default_bool @{option ML_exception_trace} then (f x; ()) else ()
fun nameof_tff_atom_type (Atom_type str) = str
| nameof_tff_atom_type _ = raise TPTP_SYNTAX "nameof_tff_atom_type called on non-atom type"
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy Tue Mar 25 17:59:34 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy Tue Mar 25 19:03:02 2014 +0100
@@ -42,8 +42,8 @@
ML {*
if test_all @{context} then ()
else
- (Options.default_put_bool @{option exception_trace} true;
- PolyML.print_depth 200;
+ (Options.default_put_bool @{option ML_exception_trace} true;
+ put_default_print_depth 200; (* FIXME proper ML_print_depth within context!? *)
PolyML.Compiler.maxInlineSize := 0)
*}
@@ -186,8 +186,9 @@
prob_names;
*}
+declare [[ML_print_depth = 2000]]
+
ML {*
-print_depth 2000;
the_tactics
|> map (filter (fn (_, _, x) => is_none x)
#> map (fn (x, SOME y, _) => (x, cterm_of @{theory} y)))
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy Tue Mar 25 17:59:34 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy Tue Mar 25 19:03:02 2014 +0100
@@ -11,9 +11,8 @@
imports TPTP_Test TPTP_Proof_Reconstruction
begin
-declare [[exception_trace]]
+declare [[ML_exception_trace, ML_print_depth = 200]]
ML {*
-print_depth 200;
PolyML.Compiler.maxInlineSize := 0;
(* FIXME doesn't work with Isabelle?
PolyML.Compiler.debug := true *)
@@ -2025,8 +2024,7 @@
(*SYN044^4*)
(*
-ML {*
-print_depth 1400;
+declare [[ML_print_depth = 1400]]
(* the_tactics *)
*}
--- a/src/Pure/Isar/attrib.ML Tue Mar 25 17:59:34 2014 +0100
+++ b/src/Pure/Isar/attrib.ML Tue Mar 25 19:03:02 2014 +0100
@@ -458,6 +458,7 @@
register_config Name_Space.names_short_raw #>
register_config Name_Space.names_unique_raw #>
register_config ML_Context.source_trace_raw #>
+ register_config ML_Compiler.print_depth_raw #>
register_config Runtime.exception_trace_raw #>
register_config Proof_Context.show_abbrevs_raw #>
register_config Goal_Display.goals_limit_raw #>
--- a/src/Pure/ML-Systems/polyml.ML Tue Mar 25 17:59:34 2014 +0100
+++ b/src/Pure/ML-Systems/polyml.ML Tue Mar 25 19:03:02 2014 +0100
@@ -130,8 +130,9 @@
local
val depth = Unsynchronized.ref 10;
in
- fun get_print_depth () = ! depth;
- fun print_depth n = (depth := n; PolyML.print_depth n);
+ fun get_default_print_depth () = ! depth;
+ fun put_default_print_depth n = (depth := n; PolyML.print_depth n);
+ val _ = put_default_print_depth 10;
end;
val error_depth = PolyML.error_depth;
@@ -175,5 +176,5 @@
("PolyML.addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
val ml_make_string =
- "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, get_print_depth ())))))";
+ "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, ML_Compiler.get_print_depth ())))))";
--- a/src/Pure/ML-Systems/smlnj.ML Tue Mar 25 17:59:34 2014 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML Tue Mar 25 19:03:02 2014 +0100
@@ -56,11 +56,12 @@
local
val depth = ref (10: int);
in
- fun get_print_depth () = ! depth;
- fun print_depth n =
+ fun get_default_print_depth () = ! depth;
+ fun put_default_print_depth n =
(depth := n;
Control.Print.printDepth := dest_int n div 2;
Control.Print.printLength := dest_int n);
+ val _ = put_default_print_depth 10;
end;
val ml_make_string = "(fn _ => \"?\")";
--- a/src/Pure/ML/ml_compiler.ML Tue Mar 25 17:59:34 2014 +0100
+++ b/src/Pure/ML/ml_compiler.ML Tue Mar 25 19:03:02 2014 +0100
@@ -11,6 +11,9 @@
val exn_message: exn -> string
val exn_error_message: exn -> unit
val exn_trace: (unit -> 'a) -> 'a
+ val print_depth_raw: Config.raw
+ val print_depth: int Config.T
+ val get_print_depth: unit -> int
type flags = {SML: bool, verbose: bool}
val eval: flags -> Position.T -> ML_Lex.token list -> unit
end
@@ -18,6 +21,8 @@
structure ML_Compiler: ML_COMPILER =
struct
+(* exceptions *)
+
val exn_info =
{exn_position = fn _: exn => Position.none,
pretty_exn = Pretty.str o General.exnMessage};
@@ -29,6 +34,21 @@
val exn_error_message = Output.error_message o exn_message;
fun exn_trace e = print_exception_trace exn_message e;
+
+(* print depth *)
+
+val print_depth_raw =
+ Config.declare "ML_print_depth" (fn _ => Config.Int (get_default_print_depth ()));
+val print_depth = Config.int print_depth_raw;
+
+fun get_print_depth () =
+ (case Context.thread_data () of
+ NONE => get_default_print_depth ()
+ | SOME context => Config.get_generic context print_depth);
+
+
+(* eval *)
+
type flags = {SML: bool, verbose: bool};
fun eval {SML, verbose} pos toks =
--- a/src/Pure/ML/ml_compiler_polyml.ML Tue Mar 25 17:59:34 2014 +0100
+++ b/src/Pure/ML/ml_compiler_polyml.ML Tue Mar 25 19:03:02 2014 +0100
@@ -7,6 +7,9 @@
structure ML_Compiler: ML_COMPILER =
struct
+open ML_Compiler;
+
+
(* source locations *)
fun position_of (loc: PolyML.location) =
@@ -74,8 +77,6 @@
(* eval ML source tokens *)
-type flags = {SML: bool, verbose: bool};
-
fun eval {SML, verbose} pos toks =
let
val _ = Secure.secure_mltext ();
@@ -184,6 +185,7 @@
PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
PolyML.Compiler.CPFileName location_props,
+ PolyML.Compiler.CPPrintDepth get_print_depth,
PolyML.Compiler.CPCompilerResultFun result_fun,
PolyML.Compiler.CPPrintInAlphabeticalOrder false];
val _ =
--- a/src/Pure/ROOT.ML Tue Mar 25 17:59:34 2014 +0100
+++ b/src/Pure/ROOT.ML Tue Mar 25 19:03:02 2014 +0100
@@ -6,8 +6,6 @@
val is_official = false;
end;
-print_depth 10;
-
(* library of general tools *)
--- a/src/Pure/Tools/proof_general_pure.ML Tue Mar 25 17:59:34 2014 +0100
+++ b/src/Pure/Tools/proof_general_pure.ML Tue Mar 25 19:03:02 2014 +0100
@@ -76,8 +76,8 @@
val _ =
ProofGeneral.preference ProofGeneral.category_advanced_display
NONE
- (Markup.print_int o get_print_depth)
- (print_depth o Markup.parse_int)
+ (Markup.print_int o get_default_print_depth)
+ (put_default_print_depth o Markup.parse_int)
ProofGeneral.pgipint
"print-depth"
"Setting for the ML print depth";
--- a/src/Tools/Metis/make_metis Tue Mar 25 17:59:34 2014 +0100
+++ b/src/Tools/Metis/make_metis Tue Mar 25 19:03:02 2014 +0100
@@ -28,8 +28,6 @@
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
(******************************************************************)
-print_depth 0;
-
EOF
for FILE in $FILES
@@ -51,7 +49,6 @@
cat <<EOF
;
-print_depth 10;
EOF
) > metis.ML
--- a/src/Tools/Metis/metis.ML Tue Mar 25 17:59:34 2014 +0100
+++ b/src/Tools/Metis/metis.ML Tue Mar 25 19:03:02 2014 +0100
@@ -14,8 +14,6 @@
(* GENERATED FILE -- DO NOT EDIT -- GENERATED FILE -- DO NOT EDIT *)
(******************************************************************)
-print_depth 0;
-
(**** Original file: src/Random.sig ****)
@@ -21462,4 +21460,3 @@
end
;
-print_depth 10;