tuned;
authorwenzelm
Wed, 28 Dec 2022 14:40:39 +0100
changeset 76800 9662c1aa35f6
parent 76799 6e786a09a4bb
child 76801 f425e0fda79c
tuned;
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;