# 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 \\<dots>
+ML{*profiling 0*}
+*)
+
+val profiling: int->unit =
+     RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler;