src/Pure/PIDE/document.ML
changeset 67500 dfde99d59f6e
parent 67380 8bef51521f21
child 68184 6c693b2700b3
     1.1 --- a/src/Pure/PIDE/document.ML	Wed Jan 24 18:54:53 2018 +0100
     1.2 +++ b/src/Pure/PIDE/document.ML	Wed Jan 24 19:50:00 2018 +0100
     1.3 @@ -131,7 +131,8 @@
     1.4          | SOME id => Protocol_Message.command_positions_yxml id)
     1.5          |> error;
     1.6      val {name = (name, _), imports, ...} = header;
     1.7 -    val {name = (_, pos), imports = imports', keywords} = Thy_Header.read_tokens span;
     1.8 +    val {name = (_, pos), imports = imports', keywords} =
     1.9 +      Thy_Header.read_tokens Position.none span;
    1.10      val imports'' = (map #1 imports ~~ map #2 imports') handle ListPair.UnequalLengths => imports;
    1.11    in Thy_Header.make (name, pos) imports'' keywords end;
    1.12