src/Pure/PIDE/document.ML

             (fn () =>
               let
                 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
                     (parents, imports) |> ListPair.app (fn (parent, (_, pos)) =>
                       let val markup =