tuned signature;
authorwenzelm
Fri Oct 06 21:33:33 2017 +0200 (20 months ago)
changeset 667730cd29455a5e8
parent 66772 a66f11a0b5b1
child 66774 f90a1370cb6a
child 66775 e8f27a35ee0f
tuned signature;
src/Pure/PIDE/document.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Fri Oct 06 21:23:21 2017 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Fri Oct 06 21:33:33 2017 +0200
     1.3 @@ -86,7 +86,8 @@
     1.4        abbrevs: Thy_Header.Abbrevs = Nil,
     1.5        errors: List[String] = Nil)
     1.6      {
     1.7 -      def error(msg: String): Header = copy(errors = errors ::: List(msg))
     1.8 +      def append_errors(msgs: List[String]): Header =
     1.9 +        copy(errors = errors ::: msgs)
    1.10  
    1.11        def cat_errors(msg2: String): Header =
    1.12          copy(errors = errors.map(msg1 => Exn.cat_message(msg1, msg2)))
    1.13 @@ -523,8 +524,10 @@
    1.14            case None =>
    1.15              List(
    1.16                Node.Deps(
    1.17 -                if (session.resources.session_base.loaded_theory(node_name))
    1.18 -                  node_header.error("Cannot update finished theory " + quote(node_name.theory))
    1.19 +                if (session.resources.session_base.loaded_theory(node_name)) {
    1.20 +                  node_header.append_errors(
    1.21 +                    List("Cannot update finished theory " + quote(node_name.theory)))
    1.22 +                }
    1.23                  else node_header),
    1.24                Node.Edits(text_edits), perspective)
    1.25            case Some(blob) => List(Node.Blob(blob), Node.Edits(text_edits))