author | wenzelm |
Fri, 18 Dec 2020 23:30:29 +0100 | |
changeset 72947 | 19484bb038a8 |
parent 72946 | 9329abcdd651 |
child 72948 | f3d0e4ea492d |
--- 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