# HG changeset patch
# User wenzelm
# Date 1120221724 -7200
# Node ID 76613dff2c9a8e4a37066d3a95021321f1a3c031
# Parent  1cf39eba29fe4c099231d620a6822d174ef9e5c0
added profiler interface (dummy);

diff -r 1cf39eba29fe -r 76613dff2c9a src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Fri Jul 01 14:42:03 2005 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Fri Jul 01 14:42:04 2005 +0200
@@ -68,8 +68,10 @@
 fun make_pp path pprint = ();
 fun install_pp _ = ();
 
-(*prompts*)
-(*n.a.??*)
+(*profiling -- dummy implementation*)
+fun profile (n: int) f x = f x;
+
+(*prompts -- dummy impelemtation*)
 fun ml_prompts p1 p2 = ();
 
 
diff -r 1cf39eba29fe -r 76613dff2c9a src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Fri Jul 01 14:42:03 2005 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Fri Jul 01 14:42:04 2005 +0200
@@ -59,8 +59,10 @@
 | _ => use "ML-Systems/cpu-timer-gc.ML");
 
 
-(* prompts *)
+(*profiling -- dummy implementation*)
+fun profile (n: int) f x = f x;
 
+(*prompts*)
 fun ml_prompts p1 p2 =
   (Compiler.Control.primaryPrompt := p1; Compiler.Control.secondaryPrompt := p2);