# HG changeset patch
# User wenzelm
# Date 1491216553 -7200
# Node ID b96cf915de754439577672cbdb24534022aba01a
# Parent  403eabd73c9a8326182f2e10f0ec84893e288626
tuned;

diff -r 403eabd73c9a -r b96cf915de75 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Apr 03 12:41:06 2017 +0200
+++ b/src/Pure/PIDE/document.scala	Mon Apr 03 12:49:13 2017 +0200
@@ -486,12 +486,12 @@
     def is_stable: Boolean
     def snapshot(): Snapshot
 
-    def node_name: Document.Node.Name
+    def node_name: Node.Name
     def is_theory: Boolean = node_name.is_theory
     override def toString: String = node_name.toString
 
     def node_required: Boolean
-    def get_blob: Option[Document.Blob]
+    def get_blob: Option[Blob]
 
     def node_edits(
       node_header: Node.Header,
@@ -502,13 +502,12 @@
         get_blob match {
           case None =>
             List(
-              Document.Node.Deps(
+              Node.Deps(
                 if (session.resources.base.loaded_theory(node_name))
                   node_header.error("Cannot update finished theory " + quote(node_name.theory))
                 else node_header),
-              Document.Node.Edits(text_edits), perspective)
-          case Some(blob) =>
-            List(Document.Node.Blob(blob), Document.Node.Edits(text_edits))
+              Node.Edits(text_edits), perspective)
+          case Some(blob) => List(Node.Blob(blob), Node.Edits(text_edits))
         }
       edits.flatMap(edit => if (edit.is_void) None else Some(node_name -> edit))
     }