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
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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
