val report_depth = Unsynchronized.ref 0 fun space n = if n <= 0 then""else (space (n-1))^" " fun report_space () = space (!report_depth)
in
fun timeit f = let val t1 = Timing.start () val x = f () val t2 = Timing.message (Timing.result t1) val _ = writeln ((report_space ()) ^ "--> "^t2) in
x end
fun report s f = let val _ = writeln ((report_space ())^s) val _ = report_depth := !report_depth + 1 val x = timeit f val _ = report_depth := !report_depth - 1 in
x end
end end
¤ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet)
¤
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.