src/Pure/PIDE/document.ML
changeset 60027 c42d65e11b6e
parent 59934 b65c4370f831
child 60198 8483c2883c8c
     1.1 --- a/src/Pure/PIDE/document.ML	Sun Apr 12 00:26:24 2015 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Sun Apr 12 11:23:36 2015 +0200
     1.3 @@ -388,10 +388,8 @@
     1.4                      map_filter Exn.get_exn blobs_digests
     1.5                      |> List.app (Output.error_message o Runtime.exn_message)
     1.6                    else (*auxiliary files*)
     1.7 -                    let val pos = Token.pos_of (nth tokens blobs_index) in
     1.8 -                      Position.reports
     1.9 -                        ((pos, Markup.language_path) :: maps (blob_reports pos) blobs_digests)
    1.10 -                    end;
    1.11 +                    let val pos = Token.pos_of (nth tokens blobs_index)
    1.12 +                    in Position.reports (maps (blob_reports pos) blobs_digests) end;
    1.13                in tokens end) ());
    1.14        val commands' =
    1.15          Inttab.update_new (command_id, (name, blobs_digests, blobs_index, span)) commands