|
(* Title: Pure/ML/ml_print_depth0.ML
Author: Makarius
Print depth for ML toplevel pp -- global default (unsynchronized).
*)
signature ML_PRINT_DEPTH =
sig
val set_print_depth: int -> unit
val get_print_depth: unit -> int
end;
structure ML_Print_Depth: ML_PRINT_DEPTH =
struct
val depth = Unsynchronized.ref 0;
fun set_print_depth n = (depth := n; PolyML.print_depth n);
fun get_print_depth () = ! depth;
end;
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
