src/Pure/ML-Systems/ml_profiling_polyml-5.6.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-5.6.ML
    Author:     Makarius

Profiling for Poly/ML 5.6.
*)

fun profile 0 f x = f x
  | profile n f x =
      let
        val mode =
          (case n of
            1 => PolyML.Profiling.ProfileTime
          | 2 => PolyML.Profiling.ProfileAllocations
          | 3 => PolyML.Profiling.ProfileLongIntEmulation
          | 6 => PolyML.Profiling.ProfileTimeThisThread
          | _ => raise Fail ("Bad profile mode: " ^ Int.toString n));
      in PolyML.Profiling.profile mode f x end;