Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned signature;
authorwenzelm
Fri, 06 Oct 2017 21:33:33 +0200
changeset 66773 0cd29455a5e8
parent 66772 a66f11a0b5b1
child 66774 f90a1370cb6a
child 66775 e8f27a35ee0f
tuned signature;
src/Pure/PIDE/document.scala file | annotate | diff | comparison | revisions 
--- 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))
isabelle