author | wenzelm |
Sun, 28 Aug 2022 14:44:34 +0200 | |
changeset 76012 | ec0424a8535e |
parent 76011 | f56d239da777 |
child 76013 | 9ac09016d036 |
--- 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 _ =