# HG changeset patch
# User wenzelm
# Date 1395770582 -3600
# Node ID 03c3d1a7c3b8acf804ac240e3ecf6420ff078c08
# Parent  f7de8392a507e3c19fad72c3676b6294058255e8
proper configuration option "ML_print_depth";
proper ML_exception_trace for HOL-TPTP;

diff -r f7de8392a507 -r 03c3d1a7c3b8 NEWS
--- 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
diff -r f7de8392a507 -r 03c3d1a7c3b8 src/Doc/IsarRef/Inner_Syntax.thy
--- 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}
diff -r f7de8392a507 -r 03c3d1a7c3b8 src/HOL/Metis.thy
--- 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 *}
 
diff -r f7de8392a507 -r 03c3d1a7c3b8 src/HOL/TPTP/TPTP_Parser/make_mlyacclib
--- 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
diff -r f7de8392a507 -r 03c3d1a7c3b8 src/HOL/TPTP/TPTP_Parser/ml_yacc_lib.ML
--- 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;
diff -r f7de8392a507 -r 03c3d1a7c3b8 src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML
--- 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"
diff -r f7de8392a507 -r 03c3d1a7c3b8 src/HOL/TPTP/TPTP_Proof_Reconstruction_Test.thy
--- 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)))
diff -r f7de8392a507 -r 03c3d1a7c3b8 src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy
--- 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 *)
 *}
 
diff -r f7de8392a507 -r 03c3d1a7c3b8 src/Pure/Isar/attrib.ML
--- 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 #>
diff -r f7de8392a507 -r 03c3d1a7c3b8 src/Pure/ML-Systems/polyml.ML
--- 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 ())))))";
 
diff -r f7de8392a507 -r 03c3d1a7c3b8 src/Pure/ML-Systems/smlnj.ML
--- 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 _ => \"?\")";
diff -r f7de8392a507 -r 03c3d1a7c3b8 src/Pure/ML/ml_compiler.ML
--- 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 =
diff -r f7de8392a507 -r 03c3d1a7c3b8 src/Pure/ML/ml_compiler_polyml.ML
--- 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 _ =
diff -r f7de8392a507 -r 03c3d1a7c3b8 src/Pure/ROOT.ML
--- 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 *)
 
diff -r f7de8392a507 -r 03c3d1a7c3b8 src/Pure/Tools/proof_general_pure.ML
--- 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";
diff -r f7de8392a507 -r 03c3d1a7c3b8 src/Tools/Metis/make_metis
--- 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
diff -r f7de8392a507 -r 03c3d1a7c3b8 src/Tools/Metis/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;