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

[Makarius]

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