[isabelle-dev] Problem with Cache_IO in Jedit

[Sree Harsha Totakura]

Hi,

I noticed that on my jedit build Cache_IO.run is not giving intended
result. I tested it with the attached theory file. From jedit output, I
get this result:

	val it = {output = [], return_code = 1, redirected_output = []}:
Cache_IO.result

However, when the same file is run in isabelle tty mode the Cache_IO.run
function seems to work fine. 

	val it =
   {output = [], return_code = 0, redirected_output = ["Hello World!"]}:
   Cache_IO.result

What could be the problem?

Regards,
Harsha
-------------- next part --------------
theory test imports Main begin

fun add :: "nat => nat => nat" where
" add x y = x + y"

ML{*
fun make_cmd infile outfile = 
      "/bin/cat " ^ (Path.print infile) ^ " > " ^ (Path.print outfile);

Cache_IO.run make_cmd ("Hello World!"); 
*}

end