Re: [isabelle] Please make OCaml and Ruby part of the Cygwin distribution



On 14-04-22 10:33, Makarius wrote:
- Load all files relatively to the implicit master directory of the
  enclosing theory.  This avoids absolute file-system references, and
  keeps your application "portable", i.e. you don't have to ask people to
  put things into a specific place.

Relative paths are desirable, so I still need that.

The problem was that I was using a "val" like this:

val thy_path = (File.platform_path(Thy_Load.master_directory @{theory}))

So it was returning the folder for the THY in which I was defining my "val" and other functions.

I now have a function which takes "@{theory}" as an argument like this:

fun thy_path thy = File.platform_path(Thy_Load.master_directory thy)

That seems to be working. Simple stuff except when it isn't.

Thanks,
GB








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.