From 292c71b051ceaaebecdf2a43a81bdbcdea275f0b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Tuong?=
<tuong@users.noreply.github.com>
Date: Sun, 26 Dec 2021 17:42:40 -0800
Subject: [PATCH] fix cbb96cf3c3965e78a480ad65a41da67041dcd7fc
---
Citadelle/src/compiler/Generator_dynamic_sequential.thy | 4 ++--
.../compiler_citadelle/Generator_dynamic_export_testing.thy | 4 ++--
2 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/Citadelle/src/compiler/Generator_dynamic_sequential.thy b/Citadelle/src/compiler/Generator_dynamic_sequential.thy
index 704034f5175..8028479f78c 100644
--- a/Citadelle/src/compiler/Generator_dynamic_sequential.thy
+++ b/Citadelle/src/compiler/Generator_dynamic_sequential.thy
@@ -223,8 +223,8 @@ structure Resources' = struct
SOME dir => dir
| NONE => Resources.master_directory (Proof_Context.theory_of ctxt));
val path = dir + Path.explode name handle ERROR msg => err msg;
- val path' = Path.implode_symbolic path;
- val _ = Path.expand path handle ERROR msg => err msg;
+ val path = Path.expand path handle ERROR msg => err msg;
+ val path' = Path.implode path;
val _ = Context_Position.report ctxt pos (Markup.path path');
val _ : Path.T = check_file path handle ERROR msg => err msg;
in path' end;
diff --git a/Citadelle/src/compiler_citadelle/Generator_dynamic_export_testing.thy b/Citadelle/src/compiler_citadelle/Generator_dynamic_export_testing.thy
index 4b48c444b7a..59a009ae99b 100644
--- a/Citadelle/src/compiler_citadelle/Generator_dynamic_export_testing.thy
+++ b/Citadelle/src/compiler_citadelle/Generator_dynamic_export_testing.thy
@@ -209,8 +209,8 @@ structure Resources' = struct
SOME dir => dir
| NONE => Resources.master_directory (Proof_Context.theory_of ctxt));
val path = dir + Path.explode name handle ERROR msg => err msg;
- val path' = Path.implode_symbolic path;
- val _ = Path.expand path handle ERROR msg => err msg;
+ val path = Path.expand path handle ERROR msg => err msg;
+ val path' = Path.implode path;
val _ = Context_Position.report ctxt pos (Markup.path path');
val _ : Path.T = check_file path handle ERROR msg => err msg;
in path' end;
--
GitLab