changeset 62492 | 0e53fade87fe |
parent 61197 | b9d69001824e |
child 63020 | 02921dcc42c3 |
--- a/src/Pure/PIDE/document.scala Tue Mar 01 20:51:38 2016 +0100 +++ b/src/Pure/PIDE/document.scala Tue Mar 01 21:00:38 2016 +0100 @@ -88,7 +88,7 @@ def error(msg: String): Header = copy(errors = errors ::: List(msg)) def cat_errors(msg2: String): Header = - copy(errors = errors.map(msg1 => Library.cat_message(msg1, msg2))) + copy(errors = errors.map(msg1 => Exn.cat_message(msg1, msg2))) } val no_header = Header(Nil, Nil, Nil)