src/HOL/Tools/ATP/modUnix.ML
changeset 15700 970e0293dfb3
parent 15642 028059faa963
child 15782 a1863ea9052b
     1.1 --- a/src/HOL/Tools/ATP/modUnix.ML	Tue Apr 12 11:07:42 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/modUnix.ML	Tue Apr 12 11:08:25 2005 +0200
     1.3 @@ -8,33 +8,7 @@
     1.4  
     1.5  val fromStatus = Posix.Process.fromStatus
     1.6  
     1.7 -
     1.8 -
     1.9 -(* Internal function - inverse of Posix.Process.fromStatus. *)
    1.10 -local
    1.11 -	val doCall = RunCall.run_call2 RuntimeCalls.POLY_SYS_os_specific
    1.12 -	in
    1.13 -		fun toStatus W_EXITED: OS.Process.status = doCall(16, (1, 0))
    1.14 -		 |  toStatus(W_EXITSTATUS w) = doCall(16, (1, Word8.toInt w))
    1.15 -		 |  toStatus(W_SIGNALED s) =
    1.16 -		 	doCall(16, (2, SysWord.toInt(Posix.Signal.toWord s)))
    1.17 -		 |  toStatus(W_STOPPED s) = 
    1.18 -		 	doCall(16, (3, SysWord.toInt(Posix.Signal.toWord s)))
    1.19 -	end
    1.20 -
    1.21 -(*	fun reap{pid, infd, outfd} =
    1.22 -	let
    1.23 -		val u = Posix.IO.close infd;
    1.24 -		val u = Posix.IO.close outfd;
    1.25 -		val (_, status) =
    1.26 -			Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
    1.27 -	in
    1.28 -		toStatus status
    1.29 -	end
    1.30 -
    1.31 -*)
    1.32 -
    1.33 -	fun reap(pid, instr, outstr) =
    1.34 +fun reap(pid, instr, outstr) =
    1.35  	let
    1.36  		val u = TextIO.closeIn instr;
    1.37  	        val u = TextIO.closeOut outstr;
    1.38 @@ -42,14 +16,14 @@
    1.39  		val (_, status) =
    1.40  			Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
    1.41  	in
    1.42 -		toStatus status
    1.43 +		status
    1.44  	end
    1.45  
    1.46  fun fdReader (name : string, fd : Posix.IO.file_desc) =
    1.47 -	  Posix.IO.mkReader {initBlkMode = true,name = name,fd = fd };
    1.48 +	  Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
    1.49  
    1.50  fun fdWriter (name, fd) =
    1.51 -          Posix.IO.mkWriter {
    1.52 +          Posix.IO.mkTextWriter {
    1.53  	      appendMode = false,
    1.54                initBlkMode = true,
    1.55                name = name,  
    1.56 @@ -292,4 +266,4 @@
    1.57                instr = instr,
    1.58                outstr = outstr
    1.59              })::procList))
    1.60 -          end;
    1.61 \ No newline at end of file
    1.62 +          end;