[isabelle-dev] Problem with Cache_IO in Jedit

[Makarius]

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