# HG changeset patch
# User wenzelm
# Date 1507318413 -7200
# Node ID 0cd29455a5e8f8f66a4f26b2ff673256e9fcc9b6
# Parent  a66f11a0b5b18681e313df9bbc7a3efe41bd2ac5
tuned signature;

diff -r a66f11a0b5b1 -r 0cd29455a5e8 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Oct 06 21:23:21 2017 +0200
+++ b/src/Pure/PIDE/document.scala	Fri Oct 06 21:33:33 2017 +0200
@@ -86,7 +86,8 @@
       abbrevs: Thy_Header.Abbrevs = Nil,
       errors: List[String] = Nil)
     {
-      def error(msg: String): Header = copy(errors = errors ::: List(msg))
+      def append_errors(msgs: List[String]): Header =
+        copy(errors = errors ::: msgs)
 
       def cat_errors(msg2: String): Header =
         copy(errors = errors.map(msg1 => Exn.cat_message(msg1, msg2)))
@@ -523,8 +524,10 @@
           case None =>
             List(
               Node.Deps(
-                if (session.resources.session_base.loaded_theory(node_name))
-                  node_header.error("Cannot update finished theory " + quote(node_name.theory))
+                if (session.resources.session_base.loaded_theory(node_name)) {
+                  node_header.append_errors(
+                    List("Cannot update finished theory " + quote(node_name.theory)))
+                }
                 else node_header),
               Node.Edits(text_edits), perspective)
           case Some(blob) => List(Node.Blob(blob), Node.Edits(text_edits))