avoid hardwired values;
authorwenzelm
Sat Mar 26 12:22:15 2016 +0100 (2016-03-26)
changeset 6271109df6a51ad3c
parent 62710 e17f014775a0
child 62712 22a17cec2efe
avoid hardwired values;
etc/options
src/HOL/Metis.thy
src/Pure/ML/ml_pretty.ML
src/Pure/Tools/ml_process.scala
     1.1 --- a/etc/options	Sat Mar 26 12:17:02 2016 +0100
     1.2 +++ b/etc/options	Sat Mar 26 12:22:15 2016 +0100
     1.3 @@ -104,6 +104,9 @@
     1.4  
     1.5  section "ML System"
     1.6  
     1.7 +option ML_print_depth : int = 20
     1.8 +  -- "ML print depth for toplevel pretty-printing"
     1.9 +
    1.10  public option ML_exception_trace : bool = false
    1.11    -- "ML exception trace for toplevel command execution"
    1.12  
     2.1 --- a/src/HOL/Metis.thy	Sat Mar 26 12:17:02 2016 +0100
     2.2 +++ b/src/HOL/Metis.thy	Sat Mar 26 12:22:15 2016 +0100
     2.3 @@ -10,9 +10,7 @@
     2.4  imports ATP
     2.5  begin
     2.6  
     2.7 -declare [[ML_print_depth = 0]]
     2.8  ML_file "~~/src/Tools/Metis/metis.ML"
     2.9 -declare [[ML_print_depth = 20]]
    2.10  
    2.11  
    2.12  subsection \<open>Literal selection and lambda-lifting helpers\<close>
     3.1 --- a/src/Pure/ML/ml_pretty.ML	Sat Mar 26 12:17:02 2016 +0100
     3.2 +++ b/src/Pure/ML/ml_pretty.ML	Sat Mar 26 12:22:15 2016 +0100
     3.3 @@ -96,7 +96,6 @@
     3.4  in
     3.5    fun get_print_depth () = ! depth;
     3.6    fun print_depth n = (depth := n; PolyML.print_depth n);
     3.7 -  val _ = print_depth 20;
     3.8  end;
     3.9  
    3.10  
     4.1 --- a/src/Pure/Tools/ml_process.scala	Sat Mar 26 12:17:02 2016 +0100
     4.2 +++ b/src/Pure/Tools/ml_process.scala	Sat Mar 26 12:22:15 2016 +0100
     4.3 @@ -66,15 +66,16 @@
     4.4      val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
     4.5      val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
     4.6  
     4.7 +    val print_depth = ML_Syntax.print_int(options.int("ML_print_depth"))
     4.8      val eval_process =
     4.9        if (heaps.isEmpty)
    4.10 -        List("PolyML.print_depth 20")
    4.11 +        List("PolyML.print_depth " + print_depth)
    4.12        else
    4.13          channel match {
    4.14            case None =>
    4.15 -            List("(ML_Pretty.print_depth 20; Isabelle_Process.init_options ())")
    4.16 +            List("(ML_Pretty.print_depth " + print_depth + "; Isabelle_Process.init_options ())")
    4.17            case Some(ch) =>
    4.18 -            List("(ML_Pretty.print_depth 20; Isabelle_Process.init_protocol " +
    4.19 +            List("(ML_Pretty.print_depth " + print_depth + "; Isabelle_Process.init_protocol " +
    4.20                ML_Syntax.print_string0(ch.server_name) + ")")
    4.21          }
    4.22