src/Pure/ML-Systems/mosml.ML
changeset 16993 2ec0b8159e8e
parent 16681 d54dfd724b35
child 17491 2bd5a6e26e1e
--- a/src/Pure/ML-Systems/mosml.ML	Mon Aug 01 19:20:46 2005 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Mon Aug 01 19:20:47 2005 +0200
@@ -57,7 +57,7 @@
   structure Process = Process
   structure FileSys = FileSys
 end;
- 
+
 (*limit the printing depth*)
 fun print_depth n =
  (Meta.printDepth := n div 2;
@@ -114,13 +114,13 @@
 
 
 
-(** interrupts **)	(*Note: may get into race conditions*)
+(** interrupts **)      (*Note: may get into race conditions*)
 
 (* FIXME proper implementation available? *)
 
 exception Interrupt;
 
-fun ignore_interrupt f x = f x;           
+fun ignore_interrupt f x = f x;
 fun raise_interrupt f x = f x;
 
 
@@ -135,8 +135,7 @@
 fun execute command =
   let
     val tmp_name = FileSys.tmpName ();
-    val is = (Process.system (command ^ " > " ^ tmp_name); TextIO.openIn 
-tmp_name);
+    val is = (Process.system (command ^ " > " ^ tmp_name); TextIO.openIn tmp_name);
     val result = TextIO.inputAll is;
   in
     TextIO.closeIn is;