tuned;
authorwenzelm
Sun, 28 Aug 2022 14:44:34 +0200
changeset 76012 ec0424a8535e
parent 76011 f56d239da777
child 76013 9ac09016d036
tuned;
src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Sun Aug 28 13:03:37 2022 +0200
+++ b/src/Pure/PIDE/document.ML	Sun Aug 28 14:44:34 2022 +0200
@@ -439,9 +439,8 @@
                           SOME thy => Theory.get_markup thy
                         | NONE =>
                             (case try Url.explode parent of
-                              NONE => Markup.path parent
-                            | SOME (Url.File path) => Markup.path (Path.implode path)
-                            | SOME _ => Markup.path parent))
+                              SOME (Url.File path) => Markup.path (Path.implode path)
+                            | _ => Markup.path parent))
                       in Position.report pos markup end)
                   else ();
                 val _ =