Admin/Isabelle2005-polyml-5.0/src/Pure/ML-Systems/polyml-5.0.ML
author haftmann
Thu, 04 Oct 2007 19:41:55 +0200
changeset 24841 df8448bc7a8b
parent 21688 e5287f12f1e1
permissions -rw-r--r--
concept for exceptions
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21688
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/ML-Systems/polyml-5.0.ML
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
     3
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
     4
Compatibility wrapper for Poly/ML 5.0 -- version for Isabelle2005.
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
     5
*)
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
     6
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
     7
structure Posix =
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
     8
struct
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
     9
  open Posix;
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
    10
  structure IO =
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
    11
  struct
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
    12
    open IO;
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
    13
    val mkReader = mkTextReader;
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
    14
    val mkWriter = mkTextWriter;
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
    15
  end;
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
    16
end;
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
    17
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
    18
structure TextIO =
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
    19
struct
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
    20
  open TextIO;
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
    21
  fun inputLine is = Option.getOpt (TextIO.inputLine is, "");
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
    22
end;
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
    23
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
    24
structure Substring =
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
    25
struct
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
    26
  open Substring;
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
    27
  val all = full;
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
    28
end;
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
    29
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
    30
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
    31
use "ML-Systems/polyml.ML";
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
    32
e5287f12f1e1 Poly/ML 5.0 setup for Isabelle2005.
wenzelm
parents:
diff changeset
    33
val pointer_eq = PolyML.pointerEq;