src/Pure/General/mailman.scala
changeset 72563 feb80142e572
parent 72559 274c9986e55b
child 72564 6d54efe5b6ee
equal deleted inserted replaced
72562:49057e93f567 72563:feb80142e572
    18   {
    18   {
    19     val text = Url.read(url)
    19     val text = Url.read(url)
    20     val hrefs = """href="([^"]+\.txt(?:\.gz)?)"""".r.findAllMatchIn(text).map(_.group(1)).toList
    20     val hrefs = """href="([^"]+\.txt(?:\.gz)?)"""".r.findAllMatchIn(text).map(_.group(1)).toList
    21     val title =
    21     val title =
    22       """<title>The ([^</>]*) Archives</title>""".r.findFirstMatchIn(text).map(_.group(1))
    22       """<title>The ([^</>]*) Archives</title>""".r.findFirstMatchIn(text).map(_.group(1))
       
    23     val list_url =
       
    24       Url(Library.take_suffix[Char](_ == '/', Url.trim_index(url).toString.toList)._1.mkString + "/")
    23     val list_name =
    25     val list_name =
    24       (proper_string(name) orElse title).getOrElse(error("Failed to determine mailing list name"))
    26       (proper_string(name) orElse title).getOrElse(error("Failed to determine mailing list name"))
    25     new Archive(Url.trim_index(url), list_name, hrefs)
    27     new Archive(list_url, list_name, hrefs)
    26   }
    28   }
    27 
    29 
    28   class Archive private[Mailman](val list_url: URL, val list_name: String, hrefs: List[String])
    30   class Archive private[Mailman](val list_url: URL, val list_name: String, hrefs: List[String])
    29   {
    31   {
    30     override def toString: String = list_name
    32     override def toString: String = list_name