src/Pure/PIDE/document.ML
changeset 73187 19484bb038a8
parent 73186 9329abcdd651
child 73189 854ebb9e4eb3
equal deleted inserted replaced
73186:9329abcdd651 73187:19484bb038a8
   426             (fn () =>
   426             (fn () =>
   427               let
   427               let
   428                 val (tokens, _) = fold_map Token.make tokens (Position.id id);
   428                 val (tokens, _) = fold_map Token.make tokens (Position.id id);
   429                 val imports =
   429                 val imports =
   430                   if name = Thy_Header.theoryN then
   430                   if name = Thy_Header.theoryN then
   431                     #imports (Thy_Header.read_tokens Position.none tokens)
   431                     (#imports (Thy_Header.read_tokens Position.none tokens)
       
   432                       handle ERROR _ => [])
   432                   else [];
   433                   else [];
   433                 val _ =
   434                 val _ =
   434                   if length parents = length imports then
   435                   if length parents = length imports then
   435                     (parents, imports) |> ListPair.app (fn (parent, (_, pos)) =>
   436                     (parents, imports) |> ListPair.app (fn (parent, (_, pos)) =>
   436                       let val markup =
   437                       let val markup =