src/Pure/ML-Systems/polyml-4.9.1.ML
author wenzelm
Fri, 10 Nov 2006 00:12:28 +0100
changeset 21280 b4aa7daa506b
parent 21176 5ec545dbad6f
child 21300 2fbe0044edd9
permissions -rw-r--r--
tuned comments;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21280
b4aa7daa506b tuned comments;
wenzelm
parents: 21176
diff changeset
     1
(*  Title:      Pure/ML-Systems/polyml-4.9.1.ML
20745
c35b225a437e Compatibility wrapper for Poly/ML 4.9.1.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
c35b225a437e Compatibility wrapper for Poly/ML 4.9.1.
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
c35b225a437e Compatibility wrapper for Poly/ML 4.9.1.
wenzelm
parents:
diff changeset
     4
c35b225a437e Compatibility wrapper for Poly/ML 4.9.1.
wenzelm
parents:
diff changeset
     5
Compatibility wrapper for Poly/ML 4.9.1.
c35b225a437e Compatibility wrapper for Poly/ML 4.9.1.
wenzelm
parents:
diff changeset
     6
*)
c35b225a437e Compatibility wrapper for Poly/ML 4.9.1.
wenzelm
parents:
diff changeset
     7
c35b225a437e Compatibility wrapper for Poly/ML 4.9.1.
wenzelm
parents:
diff changeset
     8
use "ML-Systems/polyml-4.1.4-patch.ML";
c35b225a437e Compatibility wrapper for Poly/ML 4.9.1.
wenzelm
parents:
diff changeset
     9
use "ML-Systems/polyml.ML";
20779
4eb07237382a added share_data;
wenzelm
parents: 20745
diff changeset
    10
20816
1cf97e0bba57 removed share_data;
wenzelm
parents: 20779
diff changeset
    11
val pointer_eq = PolyML.pointerEq;
21176
5ec545dbad6f String.compare: slow version -- performance test;
wenzelm
parents: 20816
diff changeset
    12
5ec545dbad6f String.compare: slow version -- performance test;
wenzelm
parents: 20816
diff changeset
    13
(* FIXME slow version -- performance test *)
5ec545dbad6f String.compare: slow version -- performance test;
wenzelm
parents: 20816
diff changeset
    14
structure String =
5ec545dbad6f String.compare: slow version -- performance test;
wenzelm
parents: 20816
diff changeset
    15
struct
5ec545dbad6f String.compare: slow version -- performance test;
wenzelm
parents: 20816
diff changeset
    16
  open String;
5ec545dbad6f String.compare: slow version -- performance test;
wenzelm
parents: 20816
diff changeset
    17
5ec545dbad6f String.compare: slow version -- performance test;
wenzelm
parents: 20816
diff changeset
    18
  fun compare (s1: string, s2) =
5ec545dbad6f String.compare: slow version -- performance test;
wenzelm
parents: 20816
diff changeset
    19
    if s1 = s2 then General.EQUAL
5ec545dbad6f String.compare: slow version -- performance test;
wenzelm
parents: 20816
diff changeset
    20
    else if s1 < s2 then General.LESS
5ec545dbad6f String.compare: slow version -- performance test;
wenzelm
parents: 20816
diff changeset
    21
    else General.GREATER;
5ec545dbad6f String.compare: slow version -- performance test;
wenzelm
parents: 20816
diff changeset
    22
end;