# HG changeset patch # User paulson # Date 1089364416 -7200 # Node ID f6a22afe0134c98fde7b0b4ed42e628cfb778ce2 # Parent d23887300b9672abc19a4c979351460e0d547947 new profiling function diff -r d23887300b96 -r f6a22afe0134 src/Pure/ML-Systems/polyml.ML --- a/src/Pure/ML-Systems/polyml.ML Thu Jul 08 19:34:56 2004 +0200 +++ b/src/Pure/ML-Systems/polyml.ML Fri Jul 09 11:13:36 2004 +0200 @@ -155,3 +155,13 @@ (case OS.Process.getEnv var of NONE => "" | SOME txt => txt); + + +(* profiling: version that works even with +ML{*profiling 1*} +apply \\ +ML{*profiling 0*} +*) + +val profiling: int->unit = + RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler;