author | wenzelm |
Thu, 04 Oct 2007 21:11:06 +0200 | |
changeset 24852 | 30da58e0a483 |
parent 24851 | 4e304aac841a |
child 24853 | aab5798e5a33 |
--- a/src/Pure/ML-Systems/polyml-5.1.ML Thu Oct 04 21:10:41 2007 +0200 +++ b/src/Pure/ML-Systems/polyml-5.1.ML Thu Oct 04 21:11:06 2007 +0200 @@ -10,6 +10,16 @@ val pointer_eq = PolyML.pointerEq; +(* single-threaded profiling *) + +local val profile_orig = profile in + +fun profile 0 f x = f x + | profile n f x = NAMED_CRITICAL "profile" (fn () => profile_orig n f x); + +end; + + (* improved versions of use_text/file *) fun use_text (tune: string -> string) name (print, err) verbose txt =