pointer equality for sml/nj
authorpaulson
Wed Jun 22 11:20:45 2005 +0200 (2005-06-22)
changeset 1652825a7459d4d4a
parent 16527 80ac7ac3733c
child 16529 d4de40568ab1
pointer equality for sml/nj
src/Pure/IsaMakefile
src/Pure/ML-Systems/smlnj-ptreql.ML
src/Pure/ML-Systems/smlnj.ML
     1.1 --- a/src/Pure/IsaMakefile	Wed Jun 22 11:09:14 2005 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Wed Jun 22 11:20:45 2005 +0200
     1.3 @@ -47,7 +47,7 @@
     1.4    ML-Systems/polyml-time-limit.ML ML-Systems/polyml.ML			\
     1.5    ML-Systems/polyml-posix.ML 						\
     1.6    ML-Systems/smlnj-basis-compat.ML ML-Systems/smlnj-compiler.ML		\
     1.7 -  ML-Systems/smlnj-pp-new.ML ML-Systems/smlnj-pp-old.ML			\
     1.8 +  ML-Systems/smlnj-ptreql.ML ML-Systems/smlnj-pp-new.ML ML-Systems/smlnj-pp-old.ML			\
     1.9    ML-Systems/smlnj.ML Proof/extraction.ML Proof/proof_rewrite_rules.ML	\
    1.10    Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML	\
    1.11    Pure.thy ROOT.ML Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML	\
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/ML-Systems/smlnj-ptreql.ML	Wed Jun 22 11:20:45 2005 +0200
     2.3 @@ -0,0 +1,10 @@
     2.4 +(*  Title:      $Id$
     2.5 +    Author:     Lawrence C Paulson
     2.6 +
     2.7 +Pointer Equality: for Standard ML of New Jersey 110.49 or later.
     2.8 +
     2.9 +Thanks to Matthias Blume for providing InlineT.ptreql!
    2.10 +*)
    2.11 +
    2.12 +CM.autoload "$smlnj/init/init.cmi";
    2.13 +val pointer_eq = InlineT.ptreql;
     3.1 --- a/src/Pure/ML-Systems/smlnj.ML	Wed Jun 22 11:09:14 2005 +0200
     3.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Wed Jun 22 11:20:45 2005 +0200
     3.3 @@ -13,9 +13,13 @@
     3.4  
     3.5  (* low-level pointer equality *)
     3.6  
     3.7 -(*proper implementation available?*)
     3.8 +(*proper implementation available? This declaration may get overridden below.*)
     3.9  fun pointer_eq (x:''a, y) = false;
    3.10  
    3.11 +(case #version_id (Compiler.version) of
    3.12 +  [110, x] => if x >= 49 then use "ML-Systems/smlnj-ptreql.ML" else ()
    3.13 +| _ => ());
    3.14 +
    3.15  
    3.16  (* restore old-style character / string functions *)
    3.17