src/Pure/ML-Systems/polyml-posix.ML
author paulson
Wed, 05 Oct 2005 10:56:06 +0200
changeset 17763 6f933b702f44
parent 16375 de1ab9e8ed4f
child 23139 aa899bce7c3b
permissions -rw-r--r--
more signals
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
structure OriginalPosix = Posix;
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
     8
structure OriginalIO = Posix.IO;
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
     9
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
    10
structure Posix =
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
    11
struct
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
    12
  open OriginalPosix
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
    13
  structure IO =
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
    14
  struct
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
    15
  open OriginalIO
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
    16
  val mkTextReader = mkReader
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
    17
  val mkTextWriter = mkWriter
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
    18
  end;
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
    19
end;
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
    20
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
    21
(*This extension of the Poly/ML Signal structure is only necessary
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
    22
  because in SML/NJ, types Posix.Signal.signal and Signals.signal differ.*)
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
    23
structure IsaSignal =
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
    24
struct
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
    25
  open Signal
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
    26
  val usr1 = Posix.Signal.usr1
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
    27
  val usr2 = Posix.Signal.usr2
17763
6f933b702f44 more signals
paulson
parents: 16375
diff changeset
    28
  val alrm = Posix.Signal.alrm
6f933b702f44 more signals
paulson
parents: 16375
diff changeset
    29
  val chld = Posix.Signal.chld
6f933b702f44 more signals
paulson
parents: 16375
diff changeset
    30
  val cont = Posix.Signal.cont
6f933b702f44 more signals
paulson
parents: 16375
diff changeset
    31
  val int  = Posix.Signal.int
6f933b702f44 more signals
paulson
parents: 16375
diff changeset
    32
  val quit = Posix.Signal.quit
16375
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
    33
end;