# HG changeset patch
# User wenzelm
# Date 1187465272 -7200
# Node ID f31594168d2768e80ed51b430f1ad708d3c80313
# Parent  83afe527504d6f99c6aa4cb36870f55d9e52ab7a
ML system provides get_print_depth;

diff -r 83afe527504d -r f31594168d27 src/Pure/ML-Systems/alice.ML
--- a/src/Pure/ML-Systems/alice.ML	Sat Aug 18 19:25:28 2007 +0200
+++ b/src/Pure/ML-Systems/alice.ML	Sat Aug 18 21:27:52 2007 +0200
@@ -42,6 +42,7 @@
 
 fun quit () = exit 0;
 
+fun get_print_depth () = ! Print.depth;
 fun print_depth n = Print.depth := n;
 
 
diff -r 83afe527504d -r f31594168d27 src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Sat Aug 18 19:25:28 2007 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Sat Aug 18 21:27:52 2007 +0200
@@ -75,9 +75,15 @@
 
 
 (*limit the printing depth*)
-fun print_depth n =
- (Meta.printDepth := n div 2;
-  Meta.printLength := n);
+local
+  val depth = ref 10;
+in
+  fun get_print_depth () = ! depth;
+  fun print_depth n =
+   (depth := n;
+    Meta.printDepth := n div 2;
+    Meta.printLength := n);
+end;
 
 (*interface for toplevel pretty printers, see also Pure/pure_setup.ML*)
 (*the documentation refers to an installPP but I couldn't fine it!*)
diff -r 83afe527504d -r f31594168d27 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Sat Aug 18 19:25:28 2007 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Sat Aug 18 21:27:52 2007 +0200
@@ -76,6 +76,14 @@
   pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
     fn () => brk (99999, 0), en);
 
+(*print depth*)
+local
+  val depth = ref 10;
+in
+  fun get_print_depth () = ! depth;
+  fun print_depth n = (depth := n; PolyML.print_depth n);
+end;
+
 
 (* ML command execution -- 'eval' *)
 
diff -r 83afe527504d -r f31594168d27 src/Pure/ML-Systems/poplogml.ML
--- a/src/Pure/ML-Systems/poplogml.ML	Sat Aug 18 19:25:28 2007 +0200
+++ b/src/Pure/ML-Systems/poplogml.ML	Sat Aug 18 21:27:52 2007 +0200
@@ -21,6 +21,7 @@
 fun make_pp path pprint = ();
 fun install_pp _ = ();
 
+fun get_print_depth () = 10;
 fun print_depth _ = ();
 
 fun exception_trace f = f ();
diff -r 83afe527504d -r f31594168d27 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Sat Aug 18 19:25:28 2007 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Sat Aug 18 21:27:52 2007 +0200
@@ -43,10 +43,15 @@
 fun quit () = exit 0;
 
 (*limit the printing depth -- divided by 2 for comparibility with Poly/ML*)
-fun print_depth n =
- (Control.Print.printDepth := (dest_int n) div 2;
-  Control.Print.printLength := dest_int n);
-
+local
+  val depth = ref 10;
+in
+  fun get_print_depth () = ! depth;
+  fun print_depth n =
+   (depth := n;
+    Control.Print.printDepth := dest_int n div 2;
+    Control.Print.printLength := dest_int n);
+end;
 
 (* compiler-independent timing functions *)
 
diff -r 83afe527504d -r f31594168d27 src/Pure/ProofGeneral/preferences.ML
--- a/src/Pure/ProofGeneral/preferences.ML	Sat Aug 18 19:25:28 2007 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Sat Aug 18 21:27:52 2007 +0200
@@ -5,16 +5,16 @@
 User preferences for Isabelle which are maintained by the interface.
 *)
 
-signature PREFERENCES = 
+signature PREFERENCES =
 sig
   type pgiptype = PgipTypes.pgiptype
 
   type isa_preference = { name: string,
-			  descr: string,
-			  default: string,
-			  pgiptype: pgiptype,
-			  get: unit -> string,
-			  set: string -> unit }
+                          descr: string,
+                          default: string,
+                          pgiptype: pgiptype,
+                          get: unit -> string,
+                          set: string -> unit }
 
   (* table of categories and preferences; names must be unique *)
   type isa_preference_table = (string * isa_preference list) list
@@ -33,22 +33,22 @@
 type pgiptype = PgipTypes.pgiptype
 
 type isa_preference = { name: string,
-			descr: string,
-			default: string,
-			pgiptype: pgiptype,
-			get: unit -> string,
-			set: string -> unit }
+                        descr: string,
+                        default: string,
+                        pgiptype: pgiptype,
+                        get: unit -> string,
+                        set: string -> unit }
 
 
-fun mkpref get set typ nm descr = 
+fun mkpref get set typ nm descr =
     { name=nm, descr=descr, pgiptype=typ, get=get, set=set, default=get() } : isa_preference
 
 fun mkpref_from_ref read write typ r nm descr =
     mkpref (fn()=> read (!r)) (fn v=> r:= (write v)) typ nm descr
 
-val int_pref = 
+val int_pref =
     mkpref_from_ref PgipTypes.int_to_pgstring (PgipTypes.read_pgipint (NONE,NONE))
-		    (PgipTypes.Pgipint (NONE, NONE))
+                    (PgipTypes.Pgipint (NONE, NONE))
 val nat_pref =
     mkpref_from_ref PgipTypes.int_to_pgstring PgipTypes.read_pgipnat PgipTypes.Pgipnat
 
@@ -56,105 +56,103 @@
     mkpref_from_ref PgipTypes.bool_to_pgstring PgipTypes.read_pgipbool PgipTypes.Pgipbool
 
 val proof_pref =
-    let 
-	fun get () = PgipTypes.bool_to_pgstring (! proofs >= 2)
-	fun set s = proofs := (if PgipTypes.read_pgipbool s then 1 else 2)
+    let
+        fun get () = PgipTypes.bool_to_pgstring (! proofs >= 2)
+        fun set s = proofs := (if PgipTypes.read_pgipbool s then 1 else 2)
     in
-	mkpref get set PgipTypes.Pgipbool "full-proofs" 
-	       "Record full proof objects internally"
+        mkpref get set PgipTypes.Pgipbool "full-proofs"
+               "Record full proof objects internally"
     end
 
-val thm_deps_pref = 
-    let 
-	fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN)
-	fun set s = if PgipTypes.read_pgipbool s then 
-			change print_mode (insert (op =) thm_depsN)
-		    else 
-			change print_mode (remove (op =) thm_depsN) 
+val thm_deps_pref =
+    let
+        fun get () = PgipTypes.bool_to_pgstring (print_mode_active thm_depsN)
+        fun set s = if PgipTypes.read_pgipbool s then
+                        change print_mode (insert (op =) thm_depsN)
+                    else
+                        change print_mode (remove (op =) thm_depsN)
     in
-	mkpref get set PgipTypes.Pgipbool "theorem-dependencies" 
-	       "Track theorem dependencies within Proof General"
+        mkpref get set PgipTypes.Pgipbool "theorem-dependencies"
+               "Track theorem dependencies within Proof General"
     end
 
 val print_depth_pref =
-    let 
-	val pg_print_depth_val = ref 10
-	fun get () = PgipTypes.int_to_pgstring (! pg_print_depth_val)
-	fun setn n = (print_depth n; pg_print_depth_val := n)
-	val set = setn o PgipTypes.read_pgipnat
+    let
+        fun get () = PgipTypes.int_to_pgstring (get_print_depth ())
+        val set = print_depth o PgipTypes.read_pgipnat
     in
-	mkpref get set PgipTypes.Pgipnat
-	       "print-depth" "Setting for the ML print depth"
+        mkpref get set PgipTypes.Pgipnat
+               "print-depth" "Setting for the ML print depth"
     end
 
 
-val display_preferences = 
+val display_preferences =
     [bool_pref show_types
-	       "show-types" 
-	       "Include types in display of Isabelle terms",
+               "show-types"
+               "Include types in display of Isabelle terms",
      bool_pref show_sorts
-	       "show-sorts"
-	       "Include sorts in display of Isabelle terms",
+               "show-sorts"
+               "Include sorts in display of Isabelle terms",
      bool_pref show_consts
-	       "show-consts"
-	       "Show types of consts in Isabelle goal display",
+               "show-consts"
+               "Show types of consts in Isabelle goal display",
      bool_pref long_names
-	       "long-names"
-	       "Show fully qualified names in Isabelle terms",
+               "long-names"
+               "Show fully qualified names in Isabelle terms",
      bool_pref show_brackets
-	       "show-brackets"
-	       "Show full bracketing in Isabelle terms",
+               "show-brackets"
+               "Show full bracketing in Isabelle terms",
      bool_pref Proof.show_main_goal
-	       "show-main-goal"
-	       "Show main goal in proof state display",
+               "show-main-goal"
+               "Show main goal in proof state display",
      bool_pref Syntax.eta_contract
-	       "eta-contract"
-	       "Print terms eta-contracted"]
+               "eta-contract"
+               "Print terms eta-contracted"]
 
 val advanced_display_preferences =
     [nat_pref goals_limit
-	      "goals-limit"
-	      "Setting for maximum number of goals printed",
+              "goals-limit"
+              "Setting for maximum number of goals printed",
      int_pref ProofContext.prems_limit
-	      "prems-limit"
-	      "Setting for maximum number of premises printed",
-     print_depth_pref,		
+              "prems-limit"
+              "Setting for maximum number of premises printed",
+     print_depth_pref,
      bool_pref show_question_marks
-	       "show-question-marks"
-	       "Show leading question mark of variable name"]
+               "show-question-marks"
+               "Show leading question mark of variable name"]
 
-val tracing_preferences = 
+val tracing_preferences =
     [bool_pref trace_simp
-	       "trace-simplifier"
-	       "Trace simplification rules.",
+               "trace-simplifier"
+               "Trace simplification rules.",
      nat_pref trace_simp_depth_limit
-	      "trace-simplifier-depth"
-	      "Trace simplifier depth limit.",
+              "trace-simplifier-depth"
+              "Trace simplifier depth limit.",
      bool_pref trace_rules
-	       "trace-rules"
-	       "Trace application of the standard rules",
+               "trace-rules"
+               "Trace application of the standard rules",
      bool_pref Pattern.trace_unify_fail
-	       "trace-unification"
-	       "Output error diagnostics during unification",
+               "trace-unification"
+               "Output error diagnostics during unification",
      bool_pref Output.timing
-	       "global-timing"
-	       "Whether to enable timing in Isabelle.",
+               "global-timing"
+               "Whether to enable timing in Isabelle.",
      bool_pref Toplevel.debug
-		"debugging"
-		"Whether to enable debugging."]
+                "debugging"
+                "Whether to enable debugging."]
 
-val proof_preferences = 
+val proof_preferences =
     [bool_pref quick_and_dirty
-	       "quick-and-dirty"
-	       "Take a few short cuts",
+               "quick-and-dirty"
+               "Take a few short cuts",
      bool_pref Toplevel.skip_proofs
-	       "skip-proofs"
-	       "Skip over proofs (interactive-only)",
+               "skip-proofs"
+               "Skip over proofs (interactive-only)",
      nat_pref Multithreading.max_threads
-	       "max-threads"
-	       "Maximum number of threads"]
+               "max-threads"
+               "Maximum number of threads"]
 
-val preferences = 
+val preferences =
     [("Display", display_preferences),
      ("Advanced Display", advanced_display_preferences),
      ("Tracing", tracing_preferences),
@@ -162,20 +160,20 @@
 
 type isa_preference_table = (string * isa_preference list) list
 
-fun remove name (preftable : isa_preference_table)  = 
-    map (fn (cat,prefs) => 
-	    (cat, filter_out (curry op= name o #name) prefs))
+fun remove name (preftable : isa_preference_table)  =
+    map (fn (cat,prefs) =>
+            (cat, filter_out (curry op= name o #name) prefs))
         preftable;
 
-fun set_default (setname,newdefault) (preftable : isa_preference_table)  = 
-    map (fn (cat,prefs) => 
-	    (cat, map (fn (pref as {name,descr,default,pgiptype,get,set})
-			  => if (name = setname) then 
-				 (set newdefault;
-				  {name=name,descr=descr,default=newdefault,
-				  pgiptype=pgiptype,get=get,set=set})
-			     else pref)
-   		  prefs))
+fun set_default (setname,newdefault) (preftable : isa_preference_table)  =
+    map (fn (cat,prefs) =>
+            (cat, map (fn (pref as {name,descr,default,pgiptype,get,set})
+                          => if (name = setname) then
+                                 (set newdefault;
+                                  {name=name,descr=descr,default=newdefault,
+                                  pgiptype=pgiptype,get=get,set=set})
+                             else pref)
+                  prefs))
         preftable;
 
 end