diff --git a/src/Pure/General/mailman.scala b/src/Pure/General/mailman.scala
new file mode 100644
--- /dev/null
+++ b/src/Pure/General/mailman.scala
@@ -0,0 +1,60 @@
+/* Title: Pure/General/mailman.scala
+ Author: Makarius
+
+Support for Mailman list servers.
+*/
+
+package isabelle
+
+
+import java.net.URL
+
+
+object Mailman
+{
+ def archive(url: URL, name: String = ""): Archive =
+ {
+ val text = Url.read(url)
+ val hrefs = """href="([^"]+\.txt(?:\.gz)?)"""".r.findAllMatchIn(text).map(_.group(1)).toList
+ val title =
+ """
The ([^>]*) Archives""".r.findFirstMatchIn(text).map(_.group(1))
+ val list_name =
+ (proper_string(name) orElse title).getOrElse(error("Failed to determine mailing list name"))
+ new Archive(Url.trim_index(url), list_name, hrefs)
+ }
+
+ class Archive private[Mailman](val list_url: URL, val list_name: String, hrefs: List[String])
+ {
+ override def toString: String = list_name
+
+ def download(
+ target_dir: Path = Path.current,
+ progress: Progress = new Progress): List[Path] =
+ {
+ val dir = target_dir + Path.basic(list_name)
+ Isabelle_System.make_directory(dir)
+
+ hrefs.flatMap(name =>
+ {
+ val path = dir + Path.basic(name)
+ val url = new URL(list_url, name)
+ val connection = url.openConnection
+ try {
+ val length = connection.getContentLengthLong
+ val timestamp = connection.getLastModified
+ val file = path.file
+ if (file.isFile && file.length == length && file.lastModified == timestamp) None
+ else {
+ progress.echo("Getting " + url)
+ val bytes =
+ using(connection.getInputStream)(Bytes.read_stream(_, hint = length.toInt max 1024))
+ Bytes.write(file, bytes)
+ file.setLastModified(timestamp)
+ Some(path)
+ }
+ }
+ finally { connection.getInputStream.close }
+ })
+ }
+ }
+}
diff --git a/src/Pure/General/url.scala b/src/Pure/General/url.scala
--- a/src/Pure/General/url.scala
+++ b/src/Pure/General/url.scala
@@ -1,95 +1,110 @@
/* Title: Pure/General/url.scala
Author: Makarius
Basic URL operations.
*/
package isabelle
import java.io.{File => JFile}
import java.nio.file.{Paths, FileSystemNotFoundException}
import java.net.{URI, URISyntaxException, URL, MalformedURLException, URLDecoder, URLEncoder}
import java.util.Locale
import java.util.zip.GZIPInputStream
object Url
{
/* special characters */
def escape_special(c: Char): String =
if ("!#$&'()*+,/:;=?@[]".contains(c)) {
String.format(Locale.ROOT, "%%%02X", Integer.valueOf(c.toInt))
}
else c.toString
def escape_special(s: String): String = s.iterator.map(escape_special).mkString
def escape_name(name: String): String =
name.iterator.map({ case '\'' => "%27" case c => c.toString }).mkString
/* make and check URLs */
def apply(name: String): URL =
{
try { new URL(name) }
catch { case _: MalformedURLException => error("Malformed URL " + quote(name)) }
}
def is_wellformed(name: String): Boolean =
try { Url(name); true }
catch { case ERROR(_) => false }
def is_readable(name: String): Boolean =
try { Url(name).openStream.close; true }
catch { case ERROR(_) => false }
+ /* trim index */
+
+ def trim_index(url: URL): URL =
+ {
+ Library.try_unprefix("/index.html", url.toString) match {
+ case Some(u) => Url(u)
+ case None =>
+ Library.try_unprefix("/index.php", url.toString) match {
+ case Some(u) => Url(u)
+ case None => url
+ }
+ }
+ }
+
+
/* strings */
def decode(s: String): String = URLDecoder.decode(s, UTF8.charset_name)
def encode(s: String): String = URLEncoder.encode(s, UTF8.charset_name)
/* read */
private def read(url: URL, gzip: Boolean): String =
using(url.openStream)(stream =>
File.read_stream(if (gzip) new GZIPInputStream(stream) else stream))
def read(url: URL): String = read(url, false)
def read_gzip(url: URL): String = read(url, true)
def read(name: String): String = read(Url(name), false)
def read_gzip(name: String): String = read(Url(name), true)
def read_bytes(url: URL): Bytes =
{
val connection = url.openConnection
val length = connection.getContentLength
using(connection.getInputStream)(Bytes.read_stream(_, hint = length))
}
/* file URIs */
def print_file(file: JFile): String = File.absolute(file).toPath.toUri.toString
def print_file_name(name: String): String = print_file(new JFile(name))
def parse_file(uri: String): JFile = Paths.get(new URI(uri)).toFile
def is_wellformed_file(uri: String): Boolean =
try { parse_file(uri); true }
catch {
case _: URISyntaxException | _: IllegalArgumentException | _: FileSystemNotFoundException =>
false
}
def absolute_file(uri: String): JFile = File.absolute(parse_file(uri))
def absolute_file_name(uri: String): String = absolute_file(uri).getPath
def canonical_file(uri: String): JFile = File.canonical(parse_file(uri))
def canonical_file_name(uri: String): String = canonical_file(uri).getPath
}
diff --git a/src/Pure/build-jars b/src/Pure/build-jars
--- a/src/Pure/build-jars
+++ b/src/Pure/build-jars
@@ -1,317 +1,318 @@
#!/usr/bin/env bash
#
# Author: Makarius
#
# build-jars - build Isabelle/Scala
#
# Requires proper Isabelle settings environment.
## sources
declare -a SOURCES=(
src/HOL/Tools/Nitpick/kodkod.scala
src/Pure/Admin/afp.scala
src/Pure/Admin/build_csdp.scala
src/Pure/Admin/build_cygwin.scala
src/Pure/Admin/build_doc.scala
src/Pure/Admin/build_e.scala
src/Pure/Admin/build_fonts.scala
src/Pure/Admin/build_history.scala
src/Pure/Admin/build_jdk.scala
src/Pure/Admin/build_log.scala
src/Pure/Admin/build_polyml.scala
src/Pure/Admin/build_release.scala
src/Pure/Admin/build_spass.scala
src/Pure/Admin/build_sqlite.scala
src/Pure/Admin/build_status.scala
src/Pure/Admin/build_verit.scala
src/Pure/Admin/build_zipperposition.scala
src/Pure/Admin/check_sources.scala
src/Pure/Admin/ci_profile.scala
src/Pure/Admin/components.scala
src/Pure/Admin/isabelle_cronjob.scala
src/Pure/Admin/isabelle_devel.scala
src/Pure/Admin/jenkins.scala
src/Pure/Admin/other_isabelle.scala
src/Pure/Concurrent/consumer_thread.scala
src/Pure/Concurrent/counter.scala
src/Pure/Concurrent/delay.scala
src/Pure/Concurrent/event_timer.scala
src/Pure/Concurrent/future.scala
src/Pure/Concurrent/isabelle_thread.scala
src/Pure/Concurrent/mailbox.scala
src/Pure/Concurrent/par_list.scala
src/Pure/Concurrent/synchronized.scala
src/Pure/GUI/color_value.scala
src/Pure/GUI/gui.scala
src/Pure/GUI/gui_thread.scala
src/Pure/GUI/popup.scala
src/Pure/GUI/wrap_panel.scala
src/Pure/General/antiquote.scala
src/Pure/General/bytes.scala
src/Pure/General/cache.scala
src/Pure/General/codepoint.scala
src/Pure/General/comment.scala
src/Pure/General/completion.scala
src/Pure/General/csv.scala
src/Pure/General/date.scala
src/Pure/General/exn.scala
src/Pure/General/file.scala
src/Pure/General/file_watcher.scala
src/Pure/General/graph.scala
src/Pure/General/graph_display.scala
src/Pure/General/graphics_file.scala
src/Pure/General/http.scala
src/Pure/General/json.scala
src/Pure/General/linear_set.scala
src/Pure/General/logger.scala
src/Pure/General/long_name.scala
+ src/Pure/General/mailman.scala
src/Pure/General/mercurial.scala
src/Pure/General/multi_map.scala
src/Pure/General/output.scala
src/Pure/General/path.scala
src/Pure/General/position.scala
src/Pure/General/pretty.scala
src/Pure/General/properties.scala
src/Pure/General/rdf.scala
src/Pure/General/scan.scala
src/Pure/General/sha1.scala
src/Pure/General/sql.scala
src/Pure/General/ssh.scala
src/Pure/General/symbol.scala
src/Pure/General/time.scala
src/Pure/General/timing.scala
src/Pure/General/untyped.scala
src/Pure/General/url.scala
src/Pure/General/utf8.scala
src/Pure/General/uuid.scala
src/Pure/General/value.scala
src/Pure/General/word.scala
src/Pure/General/xz.scala
src/Pure/Isar/document_structure.scala
src/Pure/Isar/keyword.scala
src/Pure/Isar/line_structure.scala
src/Pure/Isar/outer_syntax.scala
src/Pure/Isar/parse.scala
src/Pure/Isar/token.scala
src/Pure/ML/ml_console.scala
src/Pure/ML/ml_lex.scala
src/Pure/ML/ml_process.scala
src/Pure/ML/ml_statistics.scala
src/Pure/ML/ml_syntax.scala
src/Pure/PIDE/byte_message.scala
src/Pure/PIDE/command.scala
src/Pure/PIDE/command_span.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/document_id.scala
src/Pure/PIDE/document_status.scala
src/Pure/PIDE/editor.scala
src/Pure/PIDE/headless.scala
src/Pure/PIDE/line.scala
src/Pure/PIDE/markup.scala
src/Pure/PIDE/markup_tree.scala
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/protocol_handlers.scala
src/Pure/PIDE/protocol_message.scala
src/Pure/PIDE/prover.scala
src/Pure/PIDE/query_operation.scala
src/Pure/PIDE/rendering.scala
src/Pure/PIDE/resources.scala
src/Pure/PIDE/session.scala
src/Pure/PIDE/text.scala
src/Pure/PIDE/xml.scala
src/Pure/PIDE/yxml.scala
src/Pure/ROOT.scala
src/Pure/System/bash.scala
src/Pure/System/command_line.scala
src/Pure/System/cygwin.scala
src/Pure/System/distribution.scala
src/Pure/System/executable.scala
src/Pure/System/getopts.scala
src/Pure/System/isabelle_charset.scala
src/Pure/System/isabelle_fonts.scala
src/Pure/System/isabelle_platform.scala
src/Pure/System/isabelle_process.scala
src/Pure/System/isabelle_system.scala
src/Pure/System/isabelle_tool.scala
src/Pure/System/java_statistics.scala
src/Pure/System/linux.scala
src/Pure/System/mingw.scala
src/Pure/System/numa.scala
src/Pure/System/options.scala
src/Pure/System/platform.scala
src/Pure/System/posix_interrupt.scala
src/Pure/System/process_result.scala
src/Pure/System/progress.scala
src/Pure/System/scala.scala
src/Pure/System/system_channel.scala
src/Pure/System/tty_loop.scala
src/Pure/Thy/bibtex.scala
src/Pure/Thy/export.scala
src/Pure/Thy/export_theory.scala
src/Pure/Thy/file_format.scala
src/Pure/Thy/html.scala
src/Pure/Thy/latex.scala
src/Pure/Thy/present.scala
src/Pure/Thy/sessions.scala
src/Pure/Thy/thy_element.scala
src/Pure/Thy/thy_header.scala
src/Pure/Thy/thy_syntax.scala
src/Pure/Tools/build.scala
src/Pure/Tools/build_docker.scala
src/Pure/Tools/check_keywords.scala
src/Pure/Tools/debugger.scala
src/Pure/Tools/doc.scala
src/Pure/Tools/dump.scala
src/Pure/Tools/fontforge.scala
src/Pure/Tools/main.scala
src/Pure/Tools/mkroot.scala
src/Pure/Tools/phabricator.scala
src/Pure/Tools/print_operation.scala
src/Pure/Tools/profiling_report.scala
src/Pure/Tools/scala_project.scala
src/Pure/Tools/server.scala
src/Pure/Tools/server_commands.scala
src/Pure/Tools/simplifier_trace.scala
src/Pure/Tools/spell_checker.scala
src/Pure/Tools/task_statistics.scala
src/Pure/Tools/update.scala
src/Pure/Tools/update_cartouches.scala
src/Pure/Tools/update_comments.scala
src/Pure/Tools/update_header.scala
src/Pure/Tools/update_then.scala
src/Pure/Tools/update_theorems.scala
src/Pure/library.scala
src/Pure/pure_thy.scala
src/Pure/term.scala
src/Pure/term_xml.scala
src/Pure/thm_name.scala
src/Tools/Graphview/graph_file.scala
src/Tools/Graphview/graph_panel.scala
src/Tools/Graphview/graphview.scala
src/Tools/Graphview/layout.scala
src/Tools/Graphview/main_panel.scala
src/Tools/Graphview/metrics.scala
src/Tools/Graphview/model.scala
src/Tools/Graphview/mutator.scala
src/Tools/Graphview/mutator_dialog.scala
src/Tools/Graphview/mutator_event.scala
src/Tools/Graphview/popups.scala
src/Tools/Graphview/shapes.scala
src/Tools/Graphview/tree_panel.scala
src/Tools/VSCode/src/build_vscode.scala
src/Tools/VSCode/src/channel.scala
src/Tools/VSCode/src/document_model.scala
src/Tools/VSCode/src/dynamic_output.scala
src/Tools/VSCode/src/grammar.scala
src/Tools/VSCode/src/preview_panel.scala
src/Tools/VSCode/src/protocol.scala
src/Tools/VSCode/src/server.scala
src/Tools/VSCode/src/state_panel.scala
src/Tools/VSCode/src/vscode_rendering.scala
src/Tools/VSCode/src/vscode_resources.scala
src/Tools/VSCode/src/vscode_spell_checker.scala
)
## diagnostics
PRG="$(basename "$0")"
function usage()
{
echo
echo "Usage: isabelle $PRG [OPTIONS]"
echo
echo " Options are:"
echo " -f fresh build"
echo
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
[ -z "$ISABELLE_HOME" ] && fail "Missing Isabelle settings environment"
## process command line
# options
FRESH=""
while getopts "f" OPT
do
case "$OPT" in
f)
FRESH=true
;;
\?)
usage
;;
esac
done
shift $(($OPTIND - 1))
# args
[ "$#" -ne 0 ] && usage
## target
TARGET_DIR="lib/classes"
TARGET_JAR="$TARGET_DIR/Pure.jar"
TARGET_SHASUM="$TARGET_DIR/Pure.shasum"
function target_shasum()
{
shasum -a1 -b "$TARGET_JAR" "${SOURCES[@]}" 2>/dev/null
}
function target_clean()
{
rm -rf "$TARGET_DIR"
}
[ -n "$FRESH" ] && target_clean
## build
target_shasum | cmp "$TARGET_SHASUM" >/dev/null 2>/dev/null
if [ "$?" -ne 0 ]; then
echo "### Building Isabelle/Scala ..."
target_clean
BUILD_DIR="$TARGET_DIR/build"
mkdir -p "$BUILD_DIR"
(
export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")"
isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS \
-d "$BUILD_DIR" "${SOURCES[@]}"
) || fail "Failed to compile sources"
CHARSET_SERVICE="META-INF/services/java.nio.charset.spi.CharsetProvider"
mkdir -p "$BUILD_DIR/$(dirname "$CHARSET_SERVICE")"
echo isabelle.Isabelle_Charset_Provider > "$BUILD_DIR/$CHARSET_SERVICE"
cp "$ISABELLE_HOME/lib/logo/isabelle_transparent-32.gif" "$BUILD_DIR/isabelle/."
cp "$ISABELLE_HOME/lib/logo/isabelle_transparent.gif" "$BUILD_DIR/isabelle/."
isabelle_jdk jar -c -f "$(platform_path "$TARGET_JAR")" -e isabelle.Main \
-C "$BUILD_DIR" META-INF \
-C "$BUILD_DIR" isabelle || fail "Failed to produce $TARGET_JAR"
rm -rf "$BUILD_DIR"
target_shasum > "$TARGET_SHASUM"
fi