added forget_structure;
authorwenzelm
Fri, 28 Mar 2008 22:39:47 +0100
changeset 26474 94735cff132c
parent 26473 2266e5fd7b63
child 26475 3cc1e48d0ce1
added forget_structure;
src/Pure/ML-Systems/alice.ML
src/Pure/ML-Systems/mosml.ML
src/Pure/ML-Systems/polyml_common.ML
src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/alice.ML	Fri Mar 28 22:39:45 2008 +0100
+++ b/src/Pure/ML-Systems/alice.ML	Fri Mar 28 22:39:47 2008 +0100
@@ -19,6 +19,8 @@
 
 val ml_system_fix_ints = false;
 
+fun forget_structure _ = ();
+
 fun exit 0 = (OS.Process.exit OS.Process.success): unit
   | exit _ = OS.Process.exit OS.Process.failure;
 
--- a/src/Pure/ML-Systems/mosml.ML	Fri Mar 28 22:39:45 2008 +0100
+++ b/src/Pure/ML-Systems/mosml.ML	Fri Mar 28 22:39:47 2008 +0100
@@ -24,6 +24,8 @@
 
 val ml_system_fix_ints = false;
 
+fun forget_structure _ = ();
+
 load "Obj";
 load "Bool";
 load "Int";
--- a/src/Pure/ML-Systems/polyml_common.ML	Fri Mar 28 22:39:45 2008 +0100
+++ b/src/Pure/ML-Systems/polyml_common.ML	Fri Mar 28 22:39:47 2008 +0100
@@ -15,6 +15,9 @@
 
 (** ML system and platform related **)
 
+val forget_structure = PolyML.Compiler.forgetStructure;
+
+
 (* Compiler options *)
 
 val ml_system_fix_ints = false;
--- a/src/Pure/ML-Systems/smlnj.ML	Fri Mar 28 22:39:45 2008 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Fri Mar 28 22:39:47 2008 +0100
@@ -52,6 +52,7 @@
     Control.Print.printLength := dest_int n);
 end;
 
+
 (* compiler-independent timing functions *)
 
 fun start_timing () =
@@ -134,6 +135,10 @@
     val txt = TextIO.inputAll instream before TextIO.closeIn instream;
   in use_text tune (1, name) output verbose txt end;
 
+fun forget_structure name =
+  use_text (fn x => x) (1, "ML") (TextIO.print, fn s => raise Fail s) false
+    ("structure " ^ name ^ " = struct end");
+
 
 
 (** interrupts **)