[isabelle-dev] Using ML files in subdirectories for code generation

[Mathias Fleury]

That works,


Thank you,

Mathias

On 01/03/2021 15:42, Makarius wrote:
> On 01/03/2021 09:11, Mathias Fleury wrote:
>> MLton.thy uses compile_generated_files to generate ML files, includes
>> parser.sml, and compile all files with MLton. This pattern now produces the
>> error message
>>
>>      Illegal path specification "<absolute_path>/PAC_Checker/code/parser.sml"
>>      beyond base directory
>>
>> I tried to declare the "code" directory in the ROOT file, but this does not
>> solve the error. Is there a solution that does /not/ involve moving the ML
>> files to the ROOT directory?
> There is actually something wrong on my side (after moving
> Isabelle_System.copy_base_file from ML to Scala).
>
> It should work properly now:
>
> changeset:   73331:d045cdbdf243
> tag:         tip
> user:        wenzelm
> date:        Mon Mar 01 15:09:57 2021 +0100
> summary:     proper relative path (see also df49ca5da9d0, 5b15eee1a661, etc.);
>
>
> 	Makarius