tuned signature;
authorwenzelm
Mon Apr 18 20:43:37 2016 +0200 (2016-04-18)
changeset 6302002921dcc42c3
parent 63019 80ef19b51493
child 63021 905e15764bb4
tuned signature;
src/Pure/PIDE/document.scala
src/Pure/PIDE/resources.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Mon Apr 18 20:24:19 2016 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Mon Apr 18 20:43:37 2016 +0200
     1.3 @@ -81,9 +81,9 @@
     1.4      /* header and name */
     1.5  
     1.6      sealed case class Header(
     1.7 -      imports: List[(Name, Position.T)],
     1.8 -      keywords: Thy_Header.Keywords,
     1.9 -      errors: List[String])
    1.10 +      imports: List[(Name, Position.T)] = Nil,
    1.11 +      keywords: Thy_Header.Keywords = Nil,
    1.12 +      errors: List[String] = Nil)
    1.13      {
    1.14        def error(msg: String): Header = copy(errors = errors ::: List(msg))
    1.15  
    1.16 @@ -91,8 +91,8 @@
    1.17          copy(errors = errors.map(msg1 => Exn.cat_message(msg1, msg2)))
    1.18      }
    1.19  
    1.20 -    val no_header = Header(Nil, Nil, Nil)
    1.21 -    def bad_header(msg: String): Header = Header(Nil, Nil, List(msg))
    1.22 +    val no_header = Header()
    1.23 +    def bad_header(msg: String): Header = Header(errors = List(msg))
    1.24  
    1.25      object Name
    1.26      {
     2.1 --- a/src/Pure/PIDE/resources.scala	Mon Apr 18 20:24:19 2016 +0200
     2.2 +++ b/src/Pure/PIDE/resources.scala	Mon Apr 18 20:43:37 2016 +0200
     2.3 @@ -103,7 +103,7 @@
     2.4  
     2.5          val imports =
     2.6            header.imports.map({ case (s, pos) => (import_name(qualifier, node_name, s), pos) })
     2.7 -        Document.Node.Header(imports, header.keywords, Nil)
     2.8 +        Document.Node.Header(imports, header.keywords)
     2.9        }
    2.10        catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
    2.11      }