src/Pure/ML-Systems/polyml-posix.ML
author wenzelm
Tue, 24 Jul 2007 19:44:33 +0200
changeset 23962 e0358fac0541
parent 23139 aa899bce7c3b
permissions -rw-r--r--
Runtime exceptions as values (from library.ML);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
16375
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/polyml-posix.ML
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
     3
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
     4
Posix patches for Poly/ML.
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
     5
*)
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
     6
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
     7
(*This extension of the Poly/ML Signal structure is only necessary
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
     8
  because in SML/NJ, types Posix.Signal.signal and Signals.signal differ.*)
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
     9
structure IsaSignal =
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
    10
struct
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
    11
  open Signal
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
    12
  val usr1 = Posix.Signal.usr1
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
    13
  val usr2 = Posix.Signal.usr2
17763
6f933b702f44 more signals
paulson
parents: 16375
diff changeset
    14
  val alrm = Posix.Signal.alrm
6f933b702f44 more signals
paulson
parents: 16375
diff changeset
    15
  val chld = Posix.Signal.chld
6f933b702f44 more signals
paulson
parents: 16375
diff changeset
    16
  val cont = Posix.Signal.cont
6f933b702f44 more signals
paulson
parents: 16375
diff changeset
    17
  val int  = Posix.Signal.int
6f933b702f44 more signals
paulson
parents: 16375
diff changeset
    18
  val quit = Posix.Signal.quit
16375
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
    19
end;