src/Pure/PIDE/protocol.scala
changeset 52862 930ce8eacb87
parent 52849 199e9fa5a5c2
child 52931 ac6648c0c0fb
     1.1 --- a/src/Pure/PIDE/protocol.scala	Mon Aug 05 15:03:52 2013 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Aug 05 15:29:10 2013 +0200
     1.3 @@ -342,7 +342,7 @@
     1.4                  (dir, (name.theory, (imports, (keywords, header.errors)))))) },
     1.5            { case Document.Node.Perspective(a, b, c) =>
     1.6                (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
     1.7 -                list(triple(id, Encode.string, list(Encode.string)))(c.dest)) }))
     1.8 +                list(pair(id, pair(Encode.string, list(Encode.string))))(c.dest)) }))
     1.9        def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
    1.10        {
    1.11          val (name, edit) = node_edit