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 |
|
74921
|
12 |
import scala.annotation.tailrec
|
74906
|
13 |
import scala.util.matching.Regex
|
74921
|
14 |
import scala.util.matching.Regex.Match
|
74906
|
15 |
|
72558
|
16 |
|
|
17 |
object Mailman
|
|
18 |
{
|
74921
|
19 |
/* mailing list messages */
|
72559
|
20 |
|
74921
|
21 |
sealed case class Message(
|
|
22 |
name: String,
|
|
23 |
date: Date,
|
|
24 |
title: String,
|
|
25 |
author_name: String,
|
|
26 |
author_address: String,
|
|
27 |
body: String)
|
72558
|
28 |
{
|
74921
|
29 |
def print: String =
|
74922
|
30 |
name + "\n" + date + "\n" + title + "\n" +
|
|
31 |
quote(author_name) + "\n" + "<" + author_address + ">\n"
|
74921
|
32 |
}
|
74906
|
33 |
|
74921
|
34 |
def message_match(lines: List[String], re: Regex): Option[Match] =
|
|
35 |
lines.flatMap(re.findFirstMatchIn(_)).headOption
|
74905
|
36 |
|
74922
|
37 |
class Message_Chunk(bg: String = "", en: String = "")
|
74921
|
38 |
{
|
|
39 |
def unapply(lines: List[String]): Option[List[String]] =
|
74922
|
40 |
{
|
|
41 |
val res1 =
|
|
42 |
if (bg.isEmpty) Some(lines)
|
|
43 |
else {
|
|
44 |
lines.dropWhile(_ != bg) match {
|
|
45 |
case Nil => None
|
|
46 |
case _ :: rest => Some(rest)
|
74921
|
47 |
}
|
74922
|
48 |
}
|
|
49 |
if (en.isEmpty) res1
|
|
50 |
else {
|
|
51 |
res1 match {
|
|
52 |
case None => None
|
|
53 |
case Some(lines1) =>
|
|
54 |
val lines2 = lines1.takeWhile(_ != en)
|
|
55 |
if (lines1.drop(lines2.length).isEmpty) None else Some(lines2)
|
|
56 |
}
|
74921
|
57 |
}
|
74922
|
58 |
}
|
|
59 |
|
74921
|
60 |
def get(lines: List[String]): List[String] =
|
74922
|
61 |
unapply(lines) getOrElse
|
|
62 |
error("Missing delimiters:" +
|
|
63 |
(if (bg.nonEmpty) " " else "") + bg +
|
|
64 |
(if (en.nonEmpty) " " else "") + en)
|
72558
|
65 |
}
|
|
66 |
|
74921
|
67 |
object Address
|
74906
|
68 |
{
|
74921
|
69 |
def anchor(s: String): String = """<a href="[^"]*">""" + s + """</a>"""
|
|
70 |
def angl(s: String): String = """<""" + s + """>"""
|
|
71 |
def quot(s: String): String = """"""" + s + """""""
|
|
72 |
def paren(s: String): String = """\(""" + s + """\)"""
|
|
73 |
val adr = """([^<>]*? at [^<>]*?)"""
|
|
74 |
val any = """([^<>]*?)"""
|
|
75 |
val spc = """\s*"""
|
|
76 |
|
|
77 |
val Name1 = quot(anchor(any)).r
|
|
78 |
val Name2 = quot(any).r
|
|
79 |
val Name_Adr1 = (quot(anchor(any)) + spc + angl(anchor(adr))).r
|
|
80 |
val Name_Adr2 = (quot(any) + spc + angl(anchor(adr))).r
|
|
81 |
val Name_Adr3 = (anchor(any) + spc + angl(anchor(adr))).r
|
|
82 |
val Name_Adr4 = (any + spc + angl(anchor(adr))).r
|
|
83 |
val Adr_Name1 = (angl(anchor(adr)) + spc + paren(any)).r
|
|
84 |
val Adr_Name2 = (anchor(adr) + spc + paren(any)).r
|
|
85 |
val Adr1 = angl(anchor(adr)).r
|
|
86 |
val Adr2 = anchor(adr).r
|
|
87 |
|
|
88 |
def trim(s: String): String = HTML.input(s).replace(" at ", "@")
|
|
89 |
|
|
90 |
def unapply(s: String): Option[(String, String)] =
|
|
91 |
s match {
|
|
92 |
case Name1(a) => Some((trim(a), ""))
|
|
93 |
case Name2(a) => Some((trim(a), ""))
|
|
94 |
case Name_Adr1(a, b) => Some((trim(a), trim(b)))
|
|
95 |
case Name_Adr2(a, b) => Some((trim(a), trim(b)))
|
|
96 |
case Name_Adr3(a, b) => Some((trim(a), trim(b)))
|
|
97 |
case Name_Adr4(a, b) => Some((trim(a), trim(b)))
|
|
98 |
case Adr_Name1(b, a) => Some((trim(a), trim(b)))
|
|
99 |
case Adr_Name2(b, a) => Some((trim(a), trim(b)))
|
|
100 |
case Adr1(a) => Some(("", trim(a)))
|
|
101 |
case Adr2(a) => Some(("", trim(a)))
|
|
102 |
case _ => None
|
|
103 |
}
|
74906
|
104 |
}
|
|
105 |
|
74921
|
106 |
|
|
107 |
/* mailing list archives */
|
|
108 |
|
|
109 |
abstract class Archive(
|
|
110 |
url: URL,
|
|
111 |
name: String = "",
|
|
112 |
tag: String = "")
|
|
113 |
{
|
|
114 |
def message_regex: Regex
|
74923
|
115 |
def message_content(name: String, lines: List[String]): Message
|
74921
|
116 |
|
|
117 |
private val main_url: URL =
|
|
118 |
Url(Library.take_suffix[Char](_ == '/', Url.trim_index(url).toString.toList)._1.mkString + "/")
|
|
119 |
|
|
120 |
private val main_html = Url.read(main_url)
|
|
121 |
|
|
122 |
val list_name: String =
|
|
123 |
{
|
|
124 |
val title =
|
|
125 |
"""<title>The ([^</>]*) Archives</title>""".r.findFirstMatchIn(main_html).map(_.group(1))
|
|
126 |
(proper_string(name) orElse title).getOrElse(error("Failed to determine mailing list name"))
|
|
127 |
}
|
72558
|
128 |
override def toString: String = list_name
|
|
129 |
|
74923
|
130 |
def full_name(href: String): String = list_name + "/" + href
|
|
131 |
|
74921
|
132 |
def list_tag: String = proper_string(tag).getOrElse(list_name)
|
|
133 |
|
|
134 |
def read_text(href: String): String = Url.read(new URL(main_url, href))
|
|
135 |
|
|
136 |
def hrefs_text: List[String] =
|
|
137 |
"""href="([^"]+\.txt(?:\.gz)?)"""".r.findAllMatchIn(main_html).map(_.group(1)).toList
|
|
138 |
|
|
139 |
def hrefs_msg: List[String] =
|
74906
|
140 |
(for {
|
74921
|
141 |
href <- """href="([^"]+)/date.html"""".r.findAllMatchIn(main_html).map(_.group(1))
|
|
142 |
html = read_text(href + "/date.html")
|
|
143 |
msg <- message_regex.findAllMatchIn(html).map(_.group(1))
|
74906
|
144 |
} yield href + "/" + msg).toList
|
|
145 |
|
|
146 |
def get(target_dir: Path, href: String, progress: Progress = new Progress): Option[Path] =
|
72558
|
147 |
{
|
|
148 |
val dir = target_dir + Path.basic(list_name)
|
74906
|
149 |
val path = dir + Path.explode(href)
|
74921
|
150 |
val url = new URL(main_url, href)
|
74906
|
151 |
val connection = url.openConnection
|
|
152 |
try {
|
|
153 |
val length = connection.getContentLengthLong
|
|
154 |
val timestamp = connection.getLastModified
|
|
155 |
val file = path.file
|
|
156 |
if (file.isFile && file.length == length && file.lastModified == timestamp) None
|
|
157 |
else {
|
|
158 |
Isabelle_System.make_directory(path.dir)
|
|
159 |
progress.echo("Getting " + url)
|
|
160 |
val bytes =
|
|
161 |
using(connection.getInputStream)(Bytes.read_stream(_, hint = length.toInt max 1024))
|
|
162 |
Bytes.write(file, bytes)
|
|
163 |
file.setLastModified(timestamp)
|
|
164 |
Some(path)
|
|
165 |
}
|
|
166 |
}
|
|
167 |
finally { connection.getInputStream.close() }
|
|
168 |
}
|
72558
|
169 |
|
74906
|
170 |
def download_text(target_dir: Path, progress: Progress = new Progress): List[Path] =
|
|
171 |
hrefs_text.flatMap(get(target_dir, _, progress = progress))
|
|
172 |
|
|
173 |
def download_msg(target_dir: Path, progress: Progress = new Progress): List[Path] =
|
|
174 |
hrefs_msg.flatMap(get(target_dir, _, progress = progress))
|
74907
|
175 |
|
|
176 |
def download(target_dir: Path, progress: Progress = new Progress): List[Path] =
|
|
177 |
download_text(target_dir, progress = progress) :::
|
|
178 |
download_msg(target_dir, progress = progress)
|
74921
|
179 |
|
|
180 |
def trim_title(str: String): String =
|
|
181 |
{
|
|
182 |
val Trim1 = ("""\s*\Q[""" + list_tag + """]\E\s*(.*)""").r
|
|
183 |
val Trim2 = """(?i:(?:re|fw|fwd)\s*:\s*)(.*)""".r
|
|
184 |
val Trim3 = """\[\s*(.*?)\s*\]""".r
|
|
185 |
@tailrec def trim(s: String): String =
|
|
186 |
s match {
|
|
187 |
case Trim1(s1) => trim(s1)
|
|
188 |
case Trim2(s1) => trim(s1)
|
|
189 |
case Trim3(s1) => trim(s1)
|
|
190 |
case _ => s
|
|
191 |
}
|
|
192 |
trim(str)
|
|
193 |
}
|
|
194 |
|
|
195 |
def trim_name(str: String): String = str.replaceAll("""\s+""", " ")
|
|
196 |
|
|
197 |
def get_messages(): List[Message] =
|
|
198 |
for (href <- hrefs_msg) yield message_content(href, split_lines(read_text(href)))
|
|
199 |
|
|
200 |
def find_messages(dir: Path): List[Message] =
|
|
201 |
{
|
|
202 |
for {
|
|
203 |
file <- File.find_files(dir.file, file => file.getName.endsWith(".html"))
|
|
204 |
rel_path <- File.relative_path(dir, File.path(file))
|
74923
|
205 |
}
|
|
206 |
yield {
|
|
207 |
val name = full_name(rel_path.implode)
|
|
208 |
message_content(name, split_lines(File.read(file)))
|
|
209 |
}
|
74921
|
210 |
}
|
72558
|
211 |
}
|
72559
|
212 |
|
|
213 |
|
|
214 |
/* Isabelle mailing lists */
|
|
215 |
|
74921
|
216 |
object Isabelle_Users extends Archive(
|
|
217 |
Url("https://lists.cam.ac.uk/pipermail/cl-isabelle-users"),
|
|
218 |
name = "isabelle-users", tag = "isabelle")
|
|
219 |
{
|
|
220 |
override def message_regex: Regex = """<li><a name="\d+" href="(msg\d+\.html)">""".r
|
|
221 |
|
|
222 |
private object Head extends
|
74922
|
223 |
Message_Chunk(bg = "<!--X-Head-of-Message-->", en = "<!--X-Head-of-Message-End-->")
|
74921
|
224 |
|
|
225 |
private object Body extends
|
74922
|
226 |
Message_Chunk(bg = "<!--X-Body-of-Message-->", en = "<!--X-Body-of-Message-End-->")
|
|
227 |
|
|
228 |
private object Date_Format
|
|
229 |
{
|
|
230 |
private val Trim1 = """\w+,\s*(.*)""".r
|
|
231 |
private val Trim2 = """(.*?)\s*\(.*\)""".r
|
|
232 |
private val Format =
|
|
233 |
Date.Format(
|
|
234 |
"d MMM uuuu H:m:s Z",
|
|
235 |
"d MMM uuuu H:m:s z",
|
|
236 |
"d MMM yy H:m:s Z",
|
|
237 |
"d MMM yy H:m:s z")
|
|
238 |
def unapply(s: String): Option[Date] =
|
|
239 |
{
|
|
240 |
val s0 = s.replaceAll("""\s+""", " ")
|
|
241 |
val s1 =
|
|
242 |
s0 match {
|
|
243 |
case Trim1(s1) => s1
|
|
244 |
case _ => s0
|
|
245 |
}
|
|
246 |
val s2 =
|
|
247 |
s1 match {
|
|
248 |
case Trim2(s2) => s2
|
|
249 |
case _ => s1
|
|
250 |
}
|
|
251 |
Format.unapply(s2)
|
|
252 |
}
|
|
253 |
}
|
74921
|
254 |
|
|
255 |
override def trim_name(str: String): String =
|
|
256 |
{
|
|
257 |
val Trim = """(.*?)\s*via\s+Cl-isabelle-users""".r
|
|
258 |
super.trim_name(str) match {
|
|
259 |
case Trim(s) => s
|
|
260 |
case s => s
|
|
261 |
}
|
|
262 |
}
|
|
263 |
|
74923
|
264 |
override def message_content(name: String, lines: List[String]): Message =
|
74921
|
265 |
{
|
|
266 |
def err(msg: String = ""): Nothing =
|
74923
|
267 |
error("Malformed message: " + name + (if (msg.isEmpty) "" else "\n" + msg))
|
74921
|
268 |
|
|
269 |
val (head, body) =
|
|
270 |
try { (Head.get(lines), Body.get(lines)) }
|
|
271 |
catch { case ERROR(msg) => err(msg) }
|
72559
|
272 |
|
74921
|
273 |
val date =
|
|
274 |
message_match(head, """<li><em>Date</em>:\s*(.*?)\s*</li>""".r)
|
|
275 |
.map(m => HTML.input(m.group(1))) match
|
|
276 |
{
|
|
277 |
case Some(Date_Format(d)) => d
|
|
278 |
case Some(s) => err("Malformed Date: " + quote(s))
|
|
279 |
case None => err("Missing Date")
|
|
280 |
}
|
|
281 |
|
|
282 |
val title =
|
|
283 |
HTML.input(message_match(head, """<li><em>Subject</em>:\s*(.*)</li>""".r)
|
|
284 |
.getOrElse(err("Missing Subject")).group(1))
|
|
285 |
|
|
286 |
val (author_name, author_address) =
|
|
287 |
message_match(head, """<li><em>From</em>:\s*(.*?)\s*</li>""".r) match {
|
|
288 |
case None => err("Missing From")
|
|
289 |
case Some(m) => Address.unapply(m.group(1)) getOrElse err("Malformed From")
|
|
290 |
}
|
|
291 |
|
|
292 |
Message(
|
74923
|
293 |
name, date, trim_title(title),
|
74921
|
294 |
trim_name(proper_string(author_name) getOrElse author_address),
|
|
295 |
author_address,
|
|
296 |
cat_lines(body))
|
|
297 |
}
|
|
298 |
}
|
|
299 |
|
|
300 |
object Isabelle_Dev extends Archive(Url("https://mailmanbroy.in.tum.de/pipermail/isabelle-dev"))
|
|
301 |
{
|
|
302 |
override def message_regex: Regex = """<LI><A HREF="(\d+\.html)">""".r
|
|
303 |
|
74922
|
304 |
private object Head extends Message_Chunk(en = "<!--beginarticle-->")
|
|
305 |
private object Body extends Message_Chunk(bg = "<!--beginarticle-->", en = "<!--endarticle-->")
|
|
306 |
|
|
307 |
private object Date_Format
|
|
308 |
{
|
|
309 |
val Format = Date.Format("E MMM d H:m:s z uuuu")
|
|
310 |
def unapply(s: String): Option[Date] = Format.unapply(s.replaceAll("""\s+""", " "))
|
|
311 |
}
|
|
312 |
|
74923
|
313 |
override def message_content(name: String, lines: List[String]): Message =
|
74922
|
314 |
{
|
|
315 |
def err(msg: String = ""): Nothing =
|
74923
|
316 |
error("Malformed message: " + name + (if (msg.isEmpty) "" else "\n" + msg))
|
74922
|
317 |
|
|
318 |
val (head, body) =
|
|
319 |
try { (Head.get(lines), Body.get(lines)) }
|
|
320 |
catch { case ERROR(msg) => err(msg) }
|
|
321 |
|
|
322 |
val date =
|
|
323 |
message_match(head, """\s*<I>(.*)</I>""".r).map(m => HTML.input(m.group(1))) match {
|
|
324 |
case Some(Date_Format(d)) => d
|
|
325 |
case Some(s) => err("Malformed Date: " + quote(s))
|
|
326 |
case None => err("Missing Date")
|
|
327 |
}
|
|
328 |
|
|
329 |
val (title, author_address) =
|
|
330 |
{
|
|
331 |
message_match(head, """TITLE="([^"]+)">(.*)""".r) match {
|
|
332 |
case Some(m) => (HTML.input(m.group(1)), Address.trim(HTML.input(m.group(2))))
|
|
333 |
case None => err("Missing TITLE")
|
|
334 |
}
|
|
335 |
}
|
|
336 |
|
|
337 |
val author_name =
|
|
338 |
message_match(head, """\s*<B>(.*)</B>""".r) match {
|
|
339 |
case None => err("Missing author")
|
|
340 |
case Some(m) => HTML.input(m.group(1))
|
|
341 |
}
|
|
342 |
|
|
343 |
Message(
|
74923
|
344 |
name, date, trim_title(title),
|
74922
|
345 |
trim_name(proper_string(author_name) getOrElse author_address),
|
|
346 |
author_address,
|
|
347 |
cat_lines(body))
|
|
348 |
}
|
74921
|
349 |
}
|
72558
|
350 |
}
|