72558
|
1 |
/* Title: Pure/General/mailman.scala
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Support for Mailman list servers.
|
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle
|
|
8 |
|
|
9 |
|
|
10 |
import java.net.URL
|
|
11 |
|
|
12 |
|
|
13 |
object Mailman
|
|
14 |
{
|
72559
|
15 |
/* mailing list archives */
|
|
16 |
|
72558
|
17 |
def archive(url: URL, name: String = ""): Archive =
|
|
18 |
{
|
|
19 |
val text = Url.read(url)
|
|
20 |
val hrefs = """href="([^"]+\.txt(?:\.gz)?)"""".r.findAllMatchIn(text).map(_.group(1)).toList
|
|
21 |
val title =
|
|
22 |
"""<title>The ([^</>]*) Archives</title>""".r.findFirstMatchIn(text).map(_.group(1))
|
72563
|
23 |
val list_url =
|
|
24 |
Url(Library.take_suffix[Char](_ == '/', Url.trim_index(url).toString.toList)._1.mkString + "/")
|
72558
|
25 |
val list_name =
|
|
26 |
(proper_string(name) orElse title).getOrElse(error("Failed to determine mailing list name"))
|
72563
|
27 |
new Archive(list_url, list_name, hrefs)
|
72558
|
28 |
}
|
|
29 |
|
|
30 |
class Archive private[Mailman](val list_url: URL, val list_name: String, hrefs: List[String])
|
|
31 |
{
|
|
32 |
override def toString: String = list_name
|
|
33 |
|
72564
|
34 |
def download(target_dir: Path, progress: Progress = new Progress): List[Path] =
|
72558
|
35 |
{
|
|
36 |
val dir = target_dir + Path.basic(list_name)
|
|
37 |
Isabelle_System.make_directory(dir)
|
|
38 |
|
|
39 |
hrefs.flatMap(name =>
|
|
40 |
{
|
|
41 |
val path = dir + Path.basic(name)
|
|
42 |
val url = new URL(list_url, name)
|
|
43 |
val connection = url.openConnection
|
|
44 |
try {
|
|
45 |
val length = connection.getContentLengthLong
|
|
46 |
val timestamp = connection.getLastModified
|
|
47 |
val file = path.file
|
|
48 |
if (file.isFile && file.length == length && file.lastModified == timestamp) None
|
|
49 |
else {
|
|
50 |
progress.echo("Getting " + url)
|
|
51 |
val bytes =
|
|
52 |
using(connection.getInputStream)(Bytes.read_stream(_, hint = length.toInt max 1024))
|
|
53 |
Bytes.write(file, bytes)
|
|
54 |
file.setLastModified(timestamp)
|
|
55 |
Some(path)
|
|
56 |
}
|
|
57 |
}
|
73367
|
58 |
finally { connection.getInputStream.close() }
|
72558
|
59 |
})
|
|
60 |
}
|
|
61 |
}
|
72559
|
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"))
|
72558
|
71 |
}
|