src/Pure/ML-Systems/polyml-5.1.ML
author wenzelm
Mon Mar 24 18:35:47 2008 +0100 (2008-03-24)
changeset 26381 509a1ca9d35c
child 26389 3835c431e141
permissions -rw-r--r--
Compatibility wrapper for Poly/ML 5.1.
wenzelm@26381
     1
(*  Title:      Pure/ML-Systems/polyml-5.1.ML
wenzelm@26381
     2
    ID:         $Id$
wenzelm@26381
     3
wenzelm@26381
     4
Compatibility wrapper for Poly/ML 5.1.
wenzelm@26381
     5
*)
wenzelm@26381
     6
wenzelm@26381
     7
use "ML-Systems/polyml_common.ML";
wenzelm@26381
     8
use "ML-Systems/multithreading_polyml.ML";
wenzelm@26381
     9
wenzelm@26381
    10
val pointer_eq = PolyML.pointerEq;
wenzelm@26381
    11
wenzelm@26381
    12
wenzelm@26381
    13
(* single-threaded profiling *)
wenzelm@26381
    14
wenzelm@26381
    15
local val profile_orig = profile in
wenzelm@26381
    16
wenzelm@26381
    17
fun profile 0 f x = f x
wenzelm@26381
    18
  | profile n f x = NAMED_CRITICAL "profile" (fn () => profile_orig n f x);
wenzelm@26381
    19
wenzelm@26381
    20
end;
wenzelm@26381
    21