# HG changeset patch
# User wenzelm
# Date 1672234839 -3600
# Node ID 9662c1aa35f6073944723235b243760690330e83
# Parent  6e786a09a4bbb8101c5c673c8dff0cc9a662fe07
tuned;

diff -r 6e786a09a4bb -r 9662c1aa35f6 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Wed Dec 28 14:08:00 2022 +0100
+++ b/src/Pure/PIDE/resources.ML	Wed Dec 28 14:40:39 2022 +0100
@@ -383,7 +383,7 @@
 
 (* formal check *)
 
-fun formal_check check_file ctxt opt_dir source =
+fun formal_check (check: Path.T -> Path.T) ctxt opt_dir source =
   let
     val name = Input.string_of source;
     val pos = Input.pos_of source;
@@ -399,7 +399,7 @@
     val path = dir + Path.explode name handle ERROR msg => err msg;
     val _ = Path.expand path handle ERROR msg => err msg;
     val _ = Context_Position.report ctxt pos (Markup.path (Path.implode_symbolic path));
-    val _ : Path.T = check_file path handle ERROR msg => err msg;
+    val _ = check path handle ERROR msg => err msg;
   in path end;
 
 val check_path = formal_check I;