src/Pure/ML-Systems/ml_profiling_polyml.ML
author wenzelm
Fri, 20 Nov 2015 21:52:05 +0100
changeset 61715 5dc95d957569
child 61885 acdfc76a6c33
permissions -rw-r--r--
speculative support for polyml-5.6, according to git commit 3527f4ba7b8b;

(*  Title:      Pure/ML-Systems/ml_profiling_polyml.ML
    Author:     Makarius

Profiling for Poly/ML.
*)

fun profile 0 f x = f x
  | profile n f x =
      let
        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
        val res = Exn.capture f x;
        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
      in Exn.release res end;