author | wenzelm |
Fri, 10 Nov 2006 00:12:28 +0100 | |
changeset 21280 | b4aa7daa506b |
parent 21176 | 5ec545dbad6f |
child 21300 | 2fbe0044edd9 |
permissions | -rw-r--r-- |
21280 | 1 |
(* Title: Pure/ML-Systems/polyml-4.9.1.ML |
20745 | 2 |
ID: $Id$ |
3 |
Author: Makarius |
|
4 |
||
5 |
Compatibility wrapper for Poly/ML 4.9.1. |
|
6 |
*) |
|
7 |
||
8 |
use "ML-Systems/polyml-4.1.4-patch.ML"; |
|
9 |
use "ML-Systems/polyml.ML"; |
|
20779 | 10 |
|
20816 | 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; |