src/Pure/ML-Systems/polyml-posix.ML
author wenzelm
Mon, 29 Aug 2005 16:18:04 +0200
changeset 17184 3d80209e9a53
parent 16375 de1ab9e8ed4f
child 17763 6f933b702f44
permissions -rw-r--r--
use AList operations;
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
de1ab9e8ed4f Posix patches (from polyml.ML);
wenzelm
parents:
diff changeset
    28
end;