src/Pure/PIDE/protocol.scala
changeset 52808 143f225e50f5
parent 52760 8517172b9626
child 52849 199e9fa5a5c2
     1.1 --- a/src/Pure/PIDE/protocol.scala	Wed Jul 31 10:54:37 2013 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Wed Jul 31 12:14:13 2013 +0200
     1.3 @@ -340,7 +340,8 @@
     1.4                      option(pair(pair(Encode.string, list(Encode.string)), list(Encode.string))))),
     1.5                    list(Encode.string)))))(
     1.6                  (dir, (name.theory, (imports, (keywords, header.errors)))))) },
     1.7 -          { case Document.Node.Perspective(a) => (a.commands.map(c => long_atom(c.id)), Nil) }))
     1.8 +          { case Document.Node.Perspective(a, b) =>
     1.9 +              (bool_atom(a) :: b.commands.map(c => long_atom(c.id)), Nil) }))
    1.10        def encode_edits: T[List[Document.Edit_Command]] = list((node_edit: Document.Edit_Command) =>
    1.11        {
    1.12          val (name, edit) = node_edit