--- a/src/Pure/PIDE/document.scala Tue Aug 02 18:44:37 2016 +0200
+++ b/src/Pure/PIDE/document.scala Tue Aug 02 18:45:34 2016 +0200
@@ -245,7 +245,7 @@
final class Node private(
val get_blob: Option[Document.Blob] = None,
val header: Node.Header = Node.no_header,
- val syntax: Option[Prover.Syntax] = None,
+ val syntax: Option[Outer_Syntax] = None,
val text_perspective: Text.Perspective = Text.Perspective.empty,
val perspective: Node.Perspective_Command = Node.no_perspective_command,
_commands: Node.Commands = Node.Commands.empty)
@@ -269,7 +269,7 @@
def update_header(new_header: Node.Header): Node =
new Node(get_blob, new_header, syntax, text_perspective, perspective, _commands)
- def update_syntax(new_syntax: Option[Prover.Syntax]): Node =
+ def update_syntax(new_syntax: Option[Outer_Syntax]): Node =
new Node(get_blob, header, new_syntax, text_perspective, perspective, _commands)
def update_perspective(