ML system provides get_print_depth;
authorwenzelm
Sat Aug 18 21:27:52 2007 +0200 (2007-08-18)
changeset 24329f31594168d27
parent 24328 83afe527504d
child 24330 9cae2e2a4b70
ML system provides get_print_depth;
src/Pure/ML-Systems/alice.ML
src/Pure/ML-Systems/mosml.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/poplogml.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/ProofGeneral/preferences.ML
     1.1 --- a/src/Pure/ML-Systems/alice.ML	Sat Aug 18 19:25:28 2007 +0200
     1.2 +++ b/src/Pure/ML-Systems/alice.ML	Sat Aug 18 21:27:52 2007 +0200
     1.3 @@ -42,6 +42,7 @@
     1.4  
     1.5  fun quit () = exit 0;
     1.6  
     1.7 +fun get_print_depth () = ! Print.depth;
     1.8  fun print_depth n = Print.depth := n;
     1.9  
    1.10  
     2.1 --- a/src/Pure/ML-Systems/mosml.ML	Sat Aug 18 19:25:28 2007 +0200
     2.2 +++ b/src/Pure/ML-Systems/mosml.ML	Sat Aug 18 21:27:52 2007 +0200
     2.3 @@ -75,9 +75,15 @@
     2.4  
     2.5  
     2.6  (*limit the printing depth*)
     2.7 -fun print_depth n =
     2.8 - (Meta.printDepth := n div 2;
     2.9 -  Meta.printLength := n);
    2.10 +local
    2.11 +  val depth = ref 10;
    2.12 +in
    2.13 +  fun get_print_depth () = ! depth;
    2.14 +  fun print_depth n =
    2.15 +   (depth := n;
    2.16 +    Meta.printDepth := n div 2;
    2.17 +    Meta.printLength := n);
    2.18 +end;
    2.19  
    2.20  (*interface for toplevel pretty printers, see also Pure/pure_setup.ML*)
    2.21  (*the documentation refers to an installPP but I couldn't fine it!*)
     3.1 --- a/src/Pure/ML-Systems/polyml.ML	Sat Aug 18 19:25:28 2007 +0200
     3.2 +++ b/src/Pure/ML-Systems/polyml.ML	Sat Aug 18 21:27:52 2007 +0200
     3.3 @@ -76,6 +76,14 @@
     3.4    pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
     3.5      fn () => brk (99999, 0), en);
     3.6  
     3.7 +(*print depth*)
     3.8 +local
     3.9 +  val depth = ref 10;
    3.10 +in
    3.11 +  fun get_print_depth () = ! depth;
    3.12 +  fun print_depth n = (depth := n; PolyML.print_depth n);
    3.13 +end;
    3.14 +
    3.15  
    3.16  (* ML command execution -- 'eval' *)
    3.17  
     4.1 --- a/src/Pure/ML-Systems/poplogml.ML	Sat Aug 18 19:25:28 2007 +0200
     4.2 +++ b/src/Pure/ML-Systems/poplogml.ML	Sat Aug 18 21:27:52 2007 +0200
     4.3 @@ -21,6 +21,7 @@
     4.4  fun make_pp path pprint = ();
     4.5  fun install_pp _ = ();
     4.6  
     4.7 +fun get_print_depth () = 10;
     4.8  fun print_depth _ = ();
     4.9  
    4.10  fun exception_trace f = f ();
     5.1 --- a/src/Pure/ML-Systems/smlnj.ML	Sat Aug 18 19:25:28 2007 +0200
     5.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Sat Aug 18 21:27:52 2007 +0200
     5.3 @@ -43,10 +43,15 @@
     5.4  fun quit () = exit 0;
     5.5  
     5.6  (*limit the printing depth -- divided by 2 for comparibility with Poly/ML*)
     5.7 -fun print_depth n =
     5.8 - (Control.Print.printDepth := (dest_int n) div 2;
     5.9 -  Control.Print.printLength := dest_int n);
    5.10 -
    5.11 +local
    5.12 +  val depth = ref 10;
    5.13 +in
    5.14 +  fun get_print_depth () = ! depth;
    5.15 +  fun print_depth n =
    5.16 +   (depth := n;
    5.17 +    Control.Print.printDepth := dest_int n div 2;
    5.18 +    Control.Print.printLength := dest_int n);
    5.19 +end;
    5.20  
    5.21  (* compiler-independent timing functions *)
    5.22  
     6.1 --- a/src/Pure/ProofGeneral/preferences.ML	Sat Aug 18 19:25:28 2007 +0200
     6.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Sat Aug 18 21:27:52 2007 +0200
     6.3 @@ -5,16 +5,16 @@
     6.4  User preferences for Isabelle which are maintained by the interface.
     6.5  *)
     6.6  
     6.7 -signature PREFERENCES = 
     6.8 +signature PREFERENCES =
     6.9  sig
    6.10    type pgiptype = PgipTypes.pgiptype
    6.11  
    6.12    type isa_preference = { name: string,
    6.13 -			  descr: string,
    6.14 -			  default: string,
    6.15 -			  pgiptype: pgiptype,
    6.16 -			  get: unit -> string,
    6.17 -			  set: string -> unit }
    6.18 +                          descr: string,
    6.19 +                          default: string,
    6.20 +                          pgiptype: pgiptype,
    6.21 +                          get: unit -> string,
    6.22 +                          set: string -> unit }
    6.23  
    6.24    (* table of categories and preferences; names must be unique *)
    6.25    type isa_preference_table = (string * isa_preference list) list
    6.26 @@ -33,22 +33,22 @@
    6.27  type pgiptype = PgipTypes.pgiptype
    6.28  
    6.29  type isa_preference = { name: string,
    6.30 -			descr: string,
    6.31 -			default: string,
    6.32 -			pgiptype: pgiptype,
    6.33 -			get: unit -> string,
    6.34 -			set: string -> unit }
    6.35 +                        descr: string,
    6.36 +                        default: string,
    6.37 +                        pgiptype: pgiptype,
    6.38 +                        get: unit -> string,
    6.39 +                        set: string -> unit }
    6.40  
    6.41  
    6.42 -fun mkpref get set typ nm descr = 
    6.43 +fun mkpref get set typ nm descr =
    6.44      { name=nm, descr=descr, pgiptype=typ, get=get, set=set, default=get() } : isa_preference
    6.45  
    6.46  fun mkpref_from_ref read write typ r nm descr =
    6.47      mkpref (fn()=> read (!r)) (fn v=> r:= (write v)) typ nm descr
    6.48  
    6.49 -val int_pref = 
    6.50 +val int_pref =
    6.51      mkpref_from_ref PgipTypes.int_to_pgstring (PgipTypes.read_pgipint (NONE,NONE))
    6.52 -		    (PgipTypes.Pgipint (NONE, NONE))
    6.53 +                    (PgipTypes.Pgipint (NONE, NONE))
    6.54  val nat_pref =
    6.55      mkpref_from_ref PgipTypes.int_to_pgstring PgipTypes.read_pgipnat PgipTypes.Pgipnat
    6.56  
    6.57 @@ -56,105 +56,103 @@
    6.58      mkpref_from_ref PgipTypes.bool_to_pgstring PgipTypes.read_pgipbool PgipTypes.Pgipbool
    6.59  
    6.60  val proof_pref =
    6.61 -    let 
    6.62 -	fun get () = PgipTypes.bool_to_pgstring (! proofs >= 2)
    6.63 -	fun set s = proofs := (if PgipTypes.read_pgipbool s then 1 else 2)
    6.64 +    let
    6.65 +        fun get () = PgipTypes.bool_to_pgstring (! proofs >= 2)
    6.66 +        fun set s = proofs := (if PgipTypes.read_pgipbool s then 1 else 2)
    6.67      in
    6.68 -	mkpref get set PgipTypes.Pgipbool "full-proofs" 
    6.69 -	       "Record full proof objects internally"
    6.70 +        mkpref get set PgipTypes.Pgipbool "full-proofs"
    6.71 +               "Record full proof objects internally"
    6.72      end
    6.73  
    6.74 -val thm_deps_pref = 
    6.75 -    let 
    6.76 -	fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN)
    6.77 -	fun set s = if PgipTypes.read_pgipbool s then 
    6.78 -			change print_mode (insert (op =) thm_depsN)
    6.79 -		    else 
    6.80 -			change print_mode (remove (op =) thm_depsN) 
    6.81 +val thm_deps_pref =
    6.82 +    let
    6.83 +        fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN)
    6.84 +        fun set s = if PgipTypes.read_pgipbool s then
    6.85 +                        change print_mode (insert (op =) thm_depsN)
    6.86 +                    else
    6.87 +                        change print_mode (remove (op =) thm_depsN)
    6.88      in
    6.89 -	mkpref get set PgipTypes.Pgipbool "theorem-dependencies" 
    6.90 -	       "Track theorem dependencies within Proof General"
    6.91 +        mkpref get set PgipTypes.Pgipbool "theorem-dependencies"
    6.92 +               "Track theorem dependencies within Proof General"
    6.93      end
    6.94  
    6.95  val print_depth_pref =
    6.96 -    let 
    6.97 -	val pg_print_depth_val = ref 10
    6.98 -	fun get () = PgipTypes.int_to_pgstring (! pg_print_depth_val)
    6.99 -	fun setn n = (print_depth n; pg_print_depth_val := n)
   6.100 -	val set = setn o PgipTypes.read_pgipnat
   6.101 +    let
   6.102 +        fun get () = PgipTypes.int_to_pgstring (get_print_depth ())
   6.103 +        val set = print_depth o PgipTypes.read_pgipnat
   6.104      in
   6.105 -	mkpref get set PgipTypes.Pgipnat
   6.106 -	       "print-depth" "Setting for the ML print depth"
   6.107 +        mkpref get set PgipTypes.Pgipnat
   6.108 +               "print-depth" "Setting for the ML print depth"
   6.109      end
   6.110  
   6.111  
   6.112 -val display_preferences = 
   6.113 +val display_preferences =
   6.114      [bool_pref show_types
   6.115 -	       "show-types" 
   6.116 -	       "Include types in display of Isabelle terms",
   6.117 +               "show-types"
   6.118 +               "Include types in display of Isabelle terms",
   6.119       bool_pref show_sorts
   6.120 -	       "show-sorts"
   6.121 -	       "Include sorts in display of Isabelle terms",
   6.122 +               "show-sorts"
   6.123 +               "Include sorts in display of Isabelle terms",
   6.124       bool_pref show_consts
   6.125 -	       "show-consts"
   6.126 -	       "Show types of consts in Isabelle goal display",
   6.127 +               "show-consts"
   6.128 +               "Show types of consts in Isabelle goal display",
   6.129       bool_pref long_names
   6.130 -	       "long-names"
   6.131 -	       "Show fully qualified names in Isabelle terms",
   6.132 +               "long-names"
   6.133 +               "Show fully qualified names in Isabelle terms",
   6.134       bool_pref show_brackets
   6.135 -	       "show-brackets"
   6.136 -	       "Show full bracketing in Isabelle terms",
   6.137 +               "show-brackets"
   6.138 +               "Show full bracketing in Isabelle terms",
   6.139       bool_pref Proof.show_main_goal
   6.140 -	       "show-main-goal"
   6.141 -	       "Show main goal in proof state display",
   6.142 +               "show-main-goal"
   6.143 +               "Show main goal in proof state display",
   6.144       bool_pref Syntax.eta_contract
   6.145 -	       "eta-contract"
   6.146 -	       "Print terms eta-contracted"]
   6.147 +               "eta-contract"
   6.148 +               "Print terms eta-contracted"]
   6.149  
   6.150  val advanced_display_preferences =
   6.151      [nat_pref goals_limit
   6.152 -	      "goals-limit"
   6.153 -	      "Setting for maximum number of goals printed",
   6.154 +              "goals-limit"
   6.155 +              "Setting for maximum number of goals printed",
   6.156       int_pref ProofContext.prems_limit
   6.157 -	      "prems-limit"
   6.158 -	      "Setting for maximum number of premises printed",
   6.159 -     print_depth_pref,		
   6.160 +              "prems-limit"
   6.161 +              "Setting for maximum number of premises printed",
   6.162 +     print_depth_pref,
   6.163       bool_pref show_question_marks
   6.164 -	       "show-question-marks"
   6.165 -	       "Show leading question mark of variable name"]
   6.166 +               "show-question-marks"
   6.167 +               "Show leading question mark of variable name"]
   6.168  
   6.169 -val tracing_preferences = 
   6.170 +val tracing_preferences =
   6.171      [bool_pref trace_simp
   6.172 -	       "trace-simplifier"
   6.173 -	       "Trace simplification rules.",
   6.174 +               "trace-simplifier"
   6.175 +               "Trace simplification rules.",
   6.176       nat_pref trace_simp_depth_limit
   6.177 -	      "trace-simplifier-depth"
   6.178 -	      "Trace simplifier depth limit.",
   6.179 +              "trace-simplifier-depth"
   6.180 +              "Trace simplifier depth limit.",
   6.181       bool_pref trace_rules
   6.182 -	       "trace-rules"
   6.183 -	       "Trace application of the standard rules",
   6.184 +               "trace-rules"
   6.185 +               "Trace application of the standard rules",
   6.186       bool_pref Pattern.trace_unify_fail
   6.187 -	       "trace-unification"
   6.188 -	       "Output error diagnostics during unification",
   6.189 +               "trace-unification"
   6.190 +               "Output error diagnostics during unification",
   6.191       bool_pref Output.timing
   6.192 -	       "global-timing"
   6.193 -	       "Whether to enable timing in Isabelle.",
   6.194 +               "global-timing"
   6.195 +               "Whether to enable timing in Isabelle.",
   6.196       bool_pref Toplevel.debug
   6.197 -		"debugging"
   6.198 -		"Whether to enable debugging."]
   6.199 +                "debugging"
   6.200 +                "Whether to enable debugging."]
   6.201  
   6.202 -val proof_preferences = 
   6.203 +val proof_preferences =
   6.204      [bool_pref quick_and_dirty
   6.205 -	       "quick-and-dirty"
   6.206 -	       "Take a few short cuts",
   6.207 +               "quick-and-dirty"
   6.208 +               "Take a few short cuts",
   6.209       bool_pref Toplevel.skip_proofs
   6.210 -	       "skip-proofs"
   6.211 -	       "Skip over proofs (interactive-only)",
   6.212 +               "skip-proofs"
   6.213 +               "Skip over proofs (interactive-only)",
   6.214       nat_pref Multithreading.max_threads
   6.215 -	       "max-threads"
   6.216 -	       "Maximum number of threads"]
   6.217 +               "max-threads"
   6.218 +               "Maximum number of threads"]
   6.219  
   6.220 -val preferences = 
   6.221 +val preferences =
   6.222      [("Display", display_preferences),
   6.223       ("Advanced Display", advanced_display_preferences),
   6.224       ("Tracing", tracing_preferences),
   6.225 @@ -162,20 +160,20 @@
   6.226  
   6.227  type isa_preference_table = (string * isa_preference list) list
   6.228  
   6.229 -fun remove name (preftable : isa_preference_table)  = 
   6.230 -    map (fn (cat,prefs) => 
   6.231 -	    (cat, filter_out (curry op= name o #name) prefs))
   6.232 +fun remove name (preftable : isa_preference_table)  =
   6.233 +    map (fn (cat,prefs) =>
   6.234 +            (cat, filter_out (curry op= name o #name) prefs))
   6.235          preftable;
   6.236  
   6.237 -fun set_default (setname,newdefault) (preftable : isa_preference_table)  = 
   6.238 -    map (fn (cat,prefs) => 
   6.239 -	    (cat, map (fn (pref as {name,descr,default,pgiptype,get,set})
   6.240 -			  => if (name = setname) then 
   6.241 -				 (set newdefault;
   6.242 -				  {name=name,descr=descr,default=newdefault,
   6.243 -				  pgiptype=pgiptype,get=get,set=set})
   6.244 -			     else pref)
   6.245 -   		  prefs))
   6.246 +fun set_default (setname,newdefault) (preftable : isa_preference_table)  =
   6.247 +    map (fn (cat,prefs) =>
   6.248 +            (cat, map (fn (pref as {name,descr,default,pgiptype,get,set})
   6.249 +                          => if (name = setname) then
   6.250 +                                 (set newdefault;
   6.251 +                                  {name=name,descr=descr,default=newdefault,
   6.252 +                                  pgiptype=pgiptype,get=get,set=set})
   6.253 +                             else pref)
   6.254 +                  prefs))
   6.255          preftable;
   6.256  
   6.257  end