# HG changeset patch
# User wenzelm
# Date 1608330629 -3600
# Node ID 19484bb038a8d442908558bbdeb660c95c9c9d5a
# Parent  9329abcdd651d7ff65a19c7af478dec4134e9e39
more robust;

diff -r 9329abcdd651 -r 19484bb038a8 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