From 99c79b50dfff0700462be21599c2c275adb45f0f Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 27 Jan 2024 07:47:54 +0000 Subject: [PATCH] Ensure that umm_types.txt is saved relative to theory file. (#674) Signed-off-by: Achim D. Brucker --- tools/c-parser/calculate_state.ML | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/tools/c-parser/calculate_state.ML b/tools/c-parser/calculate_state.ML index 7fcb9f56e9..74d45d739a 100644 --- a/tools/c-parser/calculate_state.ML +++ b/tools/c-parser/calculate_state.ML @@ -480,8 +480,12 @@ fun mk_thy_types cse install thy = let val thy = List.foldl rcddecls_phase0 thy sorted_structs + val abs_outfilnameN = (if Path.is_absolute (Path.explode outfilnameN) + then outfilnameN + else (Path.implode o Path.expand) + (Path.append (Resources.master_directory thy) (Path.explode outfilnameN))) (* Yuck, sorry *) - val _ = gen_umm_types_file cse outfilnameN + val _ = gen_umm_types_file cse abs_outfilnameN val arrays = List.filter (fn (_, sz) => sz <> 0) (Binaryset.listItems (get_array_mentions cse))