equal
deleted
inserted
replaced
10 import java.net.URL |
10 import java.net.URL |
11 |
11 |
12 |
12 |
13 object Mailman |
13 object Mailman |
14 { |
14 { |
|
15 /* mailing list archives */ |
|
16 |
15 def archive(url: URL, name: String = ""): Archive = |
17 def archive(url: URL, name: String = ""): Archive = |
16 { |
18 { |
17 val text = Url.read(url) |
19 val text = Url.read(url) |
18 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 |
19 val title = |
21 val title = |
55 } |
57 } |
56 finally { connection.getInputStream.close } |
58 finally { connection.getInputStream.close } |
57 }) |
59 }) |
58 } |
60 } |
59 } |
61 } |
|
62 |
|
63 |
|
64 /* Isabelle mailing lists */ |
|
65 |
|
66 def isabelle_users: Archive = |
|
67 archive(Url("https://lists.cam.ac.uk/pipermail/cl-isabelle-users"), name = "isabelle-users") |
|
68 |
|
69 def isabelle_dev: Archive = |
|
70 archive(Url("https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev")) |
60 } |
71 } |