more robust;
authorwenzelm
Fri, 18 Dec 2020 23:30:29 +0100
changeset 72947 19484bb038a8
parent 72946 9329abcdd651
child 72948 f3d0e4ea492d
more robust;
src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Fri Dec 18 23:19:07 2020 +0100
+++ b/src/Pure/PIDE/document.ML	Fri Dec 18 23:30:29 2020 +0100
@@ -428,7 +428,8 @@
                 val (tokens, _) = fold_map Token.make tokens (Position.id id);
                 val imports =
                   if name = Thy_Header.theoryN then
-                    #imports (Thy_Header.read_tokens Position.none tokens)
+                    (#imports (Thy_Header.read_tokens Position.none tokens)
+                      handle ERROR _ => [])
                   else [];
                 val _ =
                   if length parents = length imports then