changeset 52887 | 98eac7b7eec3 |
parent 52861 | e93d73b51fd0 |
child 52901 | 8be75f53db82 |
--- a/src/Pure/Thy/thy_syntax.scala Wed Aug 07 11:17:06 2013 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Wed Aug 07 11:44:17 2013 +0200 @@ -95,7 +95,7 @@ def command_perspective( node: Document.Node, perspective: Text.Perspective, - overlays: Document.Overlays): (Command.Perspective, Command.Perspective) = + overlays: Document.Node.Overlays): (Command.Perspective, Command.Perspective) = { if (perspective.is_empty && overlays.is_empty) (Command.Perspective.empty, Command.Perspective.empty)