--- 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))