On Sun, 24 Jul 2011, Sree Harsha Totakura wrote:
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?
Path.print is for human-readable output in the IDE. On the TTY you happen
to get plain text only, so it works under the asumption that there are no
spaces in the file name (which is a common source of spurious break-downs
of shell scripts). In jEdit the situation is better, since the wrong
function Path.print always includes extra markup that make this attempt
fail immediately.
The proper function in this situation is File.shell_path.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
