# HG changeset patch # User wenzelm # Date 1163113948 -3600 # Node ID b4aa7daa506be091628a787ffe9981e103d26adc # Parent 2cb5f1621bcf400ac2e6f8f206c0dfff754a8617 tuned comments; diff -r 2cb5f1621bcf -r b4aa7daa506b src/Pure/ML-Systems/mosml.ML --- a/src/Pure/ML-Systems/mosml.ML Thu Nov 09 23:40:19 2006 +0100 +++ b/src/Pure/ML-Systems/mosml.ML Fri Nov 10 00:12:28 2006 +0100 @@ -97,10 +97,11 @@ (* bounded time execution *) -(* FIXME proper implementation available? *) +(*dummy implementation*) fun interrupt_timeout time f x = f x; + (* ML command execution *) (*Can one redirect 'use' directly to an instream?*) diff -r 2cb5f1621bcf -r b4aa7daa506b src/Pure/ML-Systems/polyml-4.9.1.ML --- a/src/Pure/ML-Systems/polyml-4.9.1.ML Thu Nov 09 23:40:19 2006 +0100 +++ b/src/Pure/ML-Systems/polyml-4.9.1.ML Fri Nov 10 00:12:28 2006 +0100 @@ -1,4 +1,4 @@ -(* Title: Pure/ML-Systems/polyml-4.2.0.ML +(* Title: Pure/ML-Systems/polyml-4.9.1.ML ID: $Id$ Author: Makarius