src/Pure/ML-Systems/polyml-5.5.3.ML
author wenzelm
Mon, 29 Sep 2014 09:57:34 +0200
changeset 58470 890d8286fd4e
parent 54726 src/Pure/ML-Systems/polyml-5.5.2.ML@5285805af26c
permissions -rw-r--r--
pro-forma support for polyml-5.5.3 (presently SVN 1960);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
58470
890d8286fd4e pro-forma support for polyml-5.5.3 (presently SVN 1960);
wenzelm
parents: 54726
diff changeset
     1
(*  Title:      Pure/ML-Systems/polyml-5.5.3.ML
54726
5285805af26c added missing file (cf. 124432e77ecf);
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
5285805af26c added missing file (cf. 124432e77ecf);
wenzelm
parents:
diff changeset
     3
58470
890d8286fd4e pro-forma support for polyml-5.5.3 (presently SVN 1960);
wenzelm
parents: 54726
diff changeset
     4
Compatibility wrapper for Poly/ML 5.5.3.
54726
5285805af26c added missing file (cf. 124432e77ecf);
wenzelm
parents:
diff changeset
     5
*)
5285805af26c added missing file (cf. 124432e77ecf);
wenzelm
parents:
diff changeset
     6
5285805af26c added missing file (cf. 124432e77ecf);
wenzelm
parents:
diff changeset
     7
structure Thread =
5285805af26c added missing file (cf. 124432e77ecf);
wenzelm
parents:
diff changeset
     8
struct
5285805af26c added missing file (cf. 124432e77ecf);
wenzelm
parents:
diff changeset
     9
  open Thread;
5285805af26c added missing file (cf. 124432e77ecf);
wenzelm
parents:
diff changeset
    10
5285805af26c added missing file (cf. 124432e77ecf);
wenzelm
parents:
diff changeset
    11
  structure Thread =
5285805af26c added missing file (cf. 124432e77ecf);
wenzelm
parents:
diff changeset
    12
  struct
5285805af26c added missing file (cf. 124432e77ecf);
wenzelm
parents:
diff changeset
    13
    open Thread;
5285805af26c added missing file (cf. 124432e77ecf);
wenzelm
parents:
diff changeset
    14
5285805af26c added missing file (cf. 124432e77ecf);
wenzelm
parents:
diff changeset
    15
    fun numProcessors () =
5285805af26c added missing file (cf. 124432e77ecf);
wenzelm
parents:
diff changeset
    16
      (case Thread.numPhysicalProcessors () of
5285805af26c added missing file (cf. 124432e77ecf);
wenzelm
parents:
diff changeset
    17
        SOME n => n
5285805af26c added missing file (cf. 124432e77ecf);
wenzelm
parents:
diff changeset
    18
      | NONE => Thread.numProcessors ());
5285805af26c added missing file (cf. 124432e77ecf);
wenzelm
parents:
diff changeset
    19
  end;
5285805af26c added missing file (cf. 124432e77ecf);
wenzelm
parents:
diff changeset
    20
end;
5285805af26c added missing file (cf. 124432e77ecf);
wenzelm
parents:
diff changeset
    21
5285805af26c added missing file (cf. 124432e77ecf);
wenzelm
parents:
diff changeset
    22
use "ML-Systems/polyml.ML";
5285805af26c added missing file (cf. 124432e77ecf);
wenzelm
parents:
diff changeset
    23