src/Pure/PIDE/document.ML
changeset 59934 b65c4370f831
parent 59735 24bee1b11fce
child 60027 c42d65e11b6e
     1.1 --- a/src/Pure/PIDE/document.ML	Mon Apr 06 14:09:31 2015 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Mon Apr 06 16:00:19 2015 +0200
     1.3 @@ -125,8 +125,8 @@
     1.4            NONE => I
     1.5          | SOME id => Protocol_Message.command_positions_yxml id)
     1.6          |> error;
     1.7 -    val {name = (name, _), imports, keywords} = header;
     1.8 -    val {name = (_, pos), imports = imports', ...} = Thy_Header.read_tokens span;
     1.9 +    val {name = (name, _), imports, ...} = header;
    1.10 +    val {name = (_, pos), imports = imports', keywords} = Thy_Header.read_tokens span;
    1.11    in Thy_Header.make (name, pos) (map #1 imports ~~ map #2 imports') keywords end;
    1.12  
    1.13  fun get_perspective (Node {perspective, ...}) = perspective;