Skip to content
Snippets Groups Projects
Commit 292c71b0 authored by Frédéric Tuong's avatar Frédéric Tuong
Browse files

fix cbb96cf3

parent cbb96cf3
Branches
No related tags found
No related merge requests found
...@@ -223,8 +223,8 @@ structure Resources' = struct ...@@ -223,8 +223,8 @@ structure Resources' = struct
SOME dir => dir SOME dir => dir
| NONE => Resources.master_directory (Proof_Context.theory_of ctxt)); | NONE => Resources.master_directory (Proof_Context.theory_of ctxt));
val path = dir + Path.explode name handle ERROR msg => err msg; val path = dir + Path.explode name handle ERROR msg => err msg;
val path' = Path.implode_symbolic path; val path = Path.expand path handle ERROR msg => err msg;
val _ = Path.expand path handle ERROR msg => err msg; val path' = Path.implode path;
val _ = Context_Position.report ctxt pos (Markup.path path'); val _ = Context_Position.report ctxt pos (Markup.path path');
val _ : Path.T = check_file path handle ERROR msg => err msg; val _ : Path.T = check_file path handle ERROR msg => err msg;
in path' end; in path' end;
......
...@@ -209,8 +209,8 @@ structure Resources' = struct ...@@ -209,8 +209,8 @@ structure Resources' = struct
SOME dir => dir SOME dir => dir
| NONE => Resources.master_directory (Proof_Context.theory_of ctxt)); | NONE => Resources.master_directory (Proof_Context.theory_of ctxt));
val path = dir + Path.explode name handle ERROR msg => err msg; val path = dir + Path.explode name handle ERROR msg => err msg;
val path' = Path.implode_symbolic path; val path = Path.expand path handle ERROR msg => err msg;
val _ = Path.expand path handle ERROR msg => err msg; val path' = Path.implode path;
val _ = Context_Position.report ctxt pos (Markup.path path'); val _ = Context_Position.report ctxt pos (Markup.path path');
val _ : Path.T = check_file path handle ERROR msg => err msg; val _ : Path.T = check_file path handle ERROR msg => err msg;
in path' end; in path' end;
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment