diff --git a/tools/afp_build.scala b/tools/afp_build.scala
--- a/tools/afp_build.scala
+++ b/tools/afp_build.scala
@@ -1,345 +1,342 @@
/* Author: Lars Hupel and Fabian Huch, TU Muenchen
Unified AFP CI integration.
*/
package afp
import isabelle.*
-import isabelle.CI_Build.{hg_id, print_section, Build_Config, Failed, Job, Profile, Result, Status}
-import afp.Metadata.{Email, Entry, Entries}
-
-import java.time.{Instant, ZoneId}
+import java.time.ZoneId
import java.time.format.DateTimeFormatter
-import java.util.{Map => JMap, Properties => JProperties}
object AFP_Build {
/* mailing */
object Mailer {
- def failed_subject(name: Entry.Name): String = s"Build of AFP entry $name failed"
+ def failed_subject(name: Metadata.Entry.Name): String = s"Build of AFP entry $name failed"
- def failed_text(session_name: String, entry: Entry.Name, isabelle_id: String,
+ def failed_text(session_name: String, entry: Metadata.Entry.Name, isabelle_id: String,
afp_id: String, result: Process_Result): String = s"""
The build for the session
$session_name,
belonging to the AFP entry
$entry
failed.
You are receiving this mail because you are the maintainer of that AFP
entry.
The following information might help you with resolving the problem.
Build log: ${Isabelle_System.getenv("BUILD_URL")}
Isabelle ID: $isabelle_id
AFP ID: $afp_id
Timeout? ${result.timeout}
Exit code: ${result.rc}
Last 50 lines from stdout (if available):
${result.out_lines.takeRight(50).mkString("\n")}
Last 50 lines from stderr (if available):
${result.err_lines.takeRight(50).mkString("\n")}
"""
}
/* metadata tooling */
class Metadata_Tools private(
val structure: AFP_Structure,
val server: Mail.Server,
- val entries: Entries
+ val entries: Metadata.Entries
) {
- def maintainers(name: Entry.Name): List[Email] = {
+ def maintainers(name: Metadata.Entry.Name): List[Metadata.Email] = {
entries.get(name) match {
case None => Nil
case Some(entry) => entry.notifies
}
}
- val sessions: Map[Entry.Name, List[String]] =
+ val sessions: Map[Metadata.Entry.Name, List[String]] =
entries.values.map(entry =>
entry.name -> structure.entry_sessions(entry.name).map(_.name)).toMap
- def session_entry(session_name: String): Option[Entry.Name] = {
+ def session_entry(session_name: String): Option[Metadata.Entry.Name] = {
val entry = sessions.find { case (_, sessions) => sessions.contains(session_name) }
entry.map { case (name, _) => name }
}
- def by_entry(sessions: List[String]): Map[Option[Entry.Name], List[String]] =
+ def by_entry(sessions: List[String]): Map[Option[Metadata.Entry.Name], List[String]] =
sessions.groupBy(session_entry)
- def notify(name: Entry.Name, subject: String, text: String): Boolean = {
+ def notify(name: Metadata.Entry.Name, subject: String, text: String): Boolean = {
val recipients = entries.get(name).map(_.notifies).getOrElse(Nil)
if (recipients.nonEmpty) {
val from = Some(Mail.address("ci@isabelle.systems"))
val to = recipients.map(mail => Mail.address(mail.address))
val mail = Mail(subject, to, text, from, "Jenkins Admin")
server.send(mail)
}
recipients.nonEmpty
}
}
object Metadata_Tools {
def load(afp: AFP_Structure, options: Options): Metadata_Tools =
new Metadata_Tools(afp, CI_Build.mail_server(options), afp.load())
}
/* utilities */
def status_as_json(isabelle_id: String, afp_id: String, start_time: String,
- status: Map[Option[String], Status]): String = {
+ status: Map[Option[String], CI_Build.Status]): String = {
val entries_strings = status.collect {
case (Some(entry), status) =>
s"""{"entry": "$entry", "status": "${status.str}"}"""
}
val entries_string = entries_strings.mkString("[", ",\n", "]")
s"""
{"build_data":
{"isabelle_id": "$isabelle_id",
"afp_id": "$afp_id",
"time": "$start_time",
"url": "${Isabelle_System.getenv("BUILD_URL")}",
"job": "${Isabelle_System.getenv("JOB_NAME")}"
},
"entries":
$entries_string
}
"""
}
- def status_as_html(status: Map[Option[String], Status]): String = {
+ def status_as_html(status: Map[Option[String], CI_Build.Status]): String = {
val entries_strings = status.collect {
- case (None, Failed) =>
+ case (None, CI_Build.Failed) =>
s"Distribution"
- case (Some(entry), Failed) =>
+ case (Some(entry), CI_Build.Failed) =>
s"""$entry"""
}
if (entries_strings.isEmpty)
""
else
entries_strings.mkString("Failed entries: ")
}
/* ci build jobs */
val afp =
- Job("afp", "builds the AFP, without slow sessions", Profile.from_host,
+ CI_Build.Job("afp", "builds the AFP, without slow sessions", CI_Build.Profile.from_host,
{
val afp = AFP_Structure()
val status_file = Path.explode("$ISABELLE_HOME/status.json").file
val deps_file = Path.explode("$ISABELLE_HOME/dependencies.json").file
- def pre_hook(options: Options): Result = {
+ def pre_hook(options: Options): CI_Build.Result = {
println(s"AFP id ${ afp.hg_id }")
if (status_file.exists())
status_file.delete()
- Result.ok
+ CI_Build.Result.ok
}
- def post_hook(results: Build.Results, options: Options, start_time: Time): Result = {
- print_section("DEPENDENCIES")
+ def post_hook(results: Build.Results, options: Options, start_time: Time): CI_Build.Result = {
+ CI_Build.print_section("DEPENDENCIES")
println("Generating dependencies file ...")
val result = Isabelle_System.bash("isabelle afp_dependencies")
result.check
println("Writing dependencies file ...")
File.write(deps_file, result.out)
- print_section("COMPLETED")
- Result.ok
+ CI_Build.print_section("COMPLETED")
+ CI_Build.Result.ok
}
- Build_Config(
+ CI_Build.Build_Config(
clean = false, include = List(afp.thys_dir), pre_hook = pre_hook,
post_hook = post_hook, selection = Sessions.Selection(
session_groups = List("AFP"),
exclude_session_groups = List("slow")))
})
val all =
- Job("all", "builds Isabelle + AFP (without slow)", Profile.from_host,
+ CI_Build.Job("all", "builds Isabelle + AFP (without slow)", CI_Build.Profile.from_host,
{
val afp = AFP_Structure()
val isabelle_home = Path.explode(Isabelle_System.getenv_strict("ISABELLE_HOME"))
- val isabelle_id = hg_id(isabelle_home)
+ val isabelle_id = CI_Build.hg_id(isabelle_home)
val status_file = Path.explode("$ISABELLE_HOME/status.json").file
val report_file = Path.explode("$ISABELLE_HOME/report.html").file
val deps_file = Path.explode("$ISABELLE_HOME/dependencies.json").file
- def pre_hook(options: Options): Result = {
+ def pre_hook(options: Options): CI_Build.Result = {
println(s"AFP id ${ afp.hg_id }")
if (status_file.exists())
status_file.delete()
if (report_file.exists())
report_file.delete()
File.write(report_file, "")
val server = CI_Build.mail_server(options)
if (!server.defined) {
println(s"Mail configuration not found.")
- Result.error
+ CI_Build.Result.error
}
else {
server.check()
- Result.ok
+ CI_Build.Result.ok
}
}
- def post_hook(results: Build.Results, options: Options, start_time: Time): Result = {
- print_section("DEPENDENCIES")
+ def post_hook(results: Build.Results, options: Options, start_time: Time): CI_Build.Result = {
+ CI_Build.print_section("DEPENDENCIES")
println("Generating dependencies file ...")
val result = Isabelle_System.bash("isabelle afp_dependencies")
result.check
println("Writing dependencies file ...")
File.write(deps_file, result.out)
val metadata = Metadata_Tools.load(afp, options)
val status = metadata.by_entry(results.sessions.toList).view.mapValues { sessions =>
- Status.merge(sessions.map(Status.from_results(results, _)))
+ CI_Build.Status.merge(sessions.map(CI_Build.Status.from_results(results, _)))
}.toMap
- print_section("REPORT")
+ CI_Build.print_section("REPORT")
println("Writing report file ...")
File.write(report_file, status_as_html(status))
- print_section("SITEGEN")
+ CI_Build.print_section("SITEGEN")
println("Writing status file ...")
val formatted_time =
start_time.instant.atZone(ZoneId.systemDefault)
.format(DateTimeFormatter.RFC_1123_DATE_TIME)
File.write(status_file, status_as_json(isabelle_id, afp.hg_id, formatted_time, status))
println("Running sitegen ...")
val script = afp.base_dir + Path.explode("admin/sitegen-devel")
val sitegen_cmd =
Bash.strings(List(script.file.toString, status_file.toString, deps_file.toString))
val sitegen_res =
Isabelle_System.bash(sitegen_cmd, progress_stdout = println, progress_stderr = println)
if (!sitegen_res.ok) {
println("sitegen failed")
}
if (!results.ok) {
- print_section("NOTIFICATIONS")
+ CI_Build.print_section("NOTIFICATIONS")
for (session_name <- results.sessions) {
val result = results(session_name)
if (!result.ok && !results.cancelled(session_name) && metadata.server.defined) {
metadata.session_entry(session_name).foreach { entry =>
val subject = Mailer.failed_subject(entry)
val text = Mailer.failed_text(session_name, entry, isabelle_id, afp.hg_id, result)
val notified = metadata.notify(entry, subject, text)
if (!notified) println(s"Entry $entry: WARNING no maintainers specified")
}
}
}
}
- print_section("COMPLETED")
- Result(sitegen_res.rc)
+ CI_Build.print_section("COMPLETED")
+ CI_Build.Result(sitegen_res.rc)
}
- Build_Config(
+ CI_Build.Build_Config(
clean = false, include = List(afp.thys_dir), pre_hook = pre_hook,
post_hook = post_hook, selection = Sessions.Selection(
all_sessions = true,
exclude_session_groups = List("slow")))
})
val mac =
- Job("mac", "builds the AFP (without some sessions) on Mac Os",
- Profile.from_host.copy(threads = 8, jobs = 1),
+ CI_Build.Job("mac", "builds the AFP (without some sessions) on Mac Os",
+ CI_Build.Profile.from_host.copy(threads = 8, jobs = 1),
{
val afp = AFP_Structure()
- def pre_hook(options: Options): Result = {
+ def pre_hook(options: Options): CI_Build.Result = {
println(s"Build for AFP id ${ afp.hg_id }")
- Result.ok
+ CI_Build.Result.ok
}
- Build_Config(
+ CI_Build.Build_Config(
include = List(afp.thys_dir), pre_hook = pre_hook, selection =
Sessions.Selection(
all_sessions = true,
exclude_sessions = List("HOL-Proofs", "HOL-ODE-Numerics", "Linear_Programming", "HOL-Nominal-Examples", "HOL-Analysis"),
exclude_session_groups = List("slow")))
})
val slow =
- Job("slow", "builds the AFP slow sessions", Profile.from_host.copy(threads = 8, jobs = 1),
+ CI_Build.Job("slow", "builds the AFP slow sessions",
+ CI_Build.Profile.from_host.copy(threads = 8, jobs = 1),
{
val afp = AFP_Structure()
- def pre_hook(options: Options): Result = {
+ def pre_hook(options: Options): CI_Build.Result = {
println(s"Build for AFP id ${ afp.hg_id }")
- Result.ok
+ CI_Build.Result.ok
}
- Build_Config(
+ CI_Build.Build_Config(
include = List(afp.thys_dir), pre_hook = pre_hook,
selection = Sessions.Selection(session_groups = List("slow")))
})
val testboard =
- Job("testboard", "builds the AFP testboard", Profile.from_host,
+ CI_Build.Job("testboard", "builds the AFP testboard", CI_Build.Profile.from_host,
{
val afp = AFP_Structure()
val report_file = Path.explode("$ISABELLE_HOME/report.html").file
- def pre_hook(options: Options): Result = {
+ def pre_hook(options: Options): CI_Build.Result = {
println(s"AFP id ${ afp.hg_id }")
if (report_file.exists())
report_file.delete()
File.write(report_file, "")
- Result.ok
+ CI_Build.Result.ok
}
- def post_hook(results: Build.Results, options: Options, start_time: Time): Result = {
+ def post_hook(results: Build.Results, options: Options, start_time: Time): CI_Build.Result = {
val metadata = Metadata_Tools.load(afp, options)
val status = metadata.by_entry(results.sessions.toList).view.mapValues { sessions =>
- Status.merge(sessions.map(Status.from_results(results, _)))
+ CI_Build.Status.merge(sessions.map(CI_Build.Status.from_results(results, _)))
}.toMap
- print_section("REPORT")
+ CI_Build.print_section("REPORT")
println("Writing report file ...")
File.write(report_file, status_as_html(status))
- print_section("COMPLETED")
- Result.ok
+ CI_Build.print_section("COMPLETED")
+ CI_Build.Result.ok
}
- Build_Config(
+ CI_Build.Build_Config(
clean = false, include = List(afp.thys_dir), pre_hook = pre_hook,
post_hook = post_hook, selection =
Sessions.Selection(
all_sessions = true,
exclude_session_groups = List("slow")))
})
}
class CI_Builds extends Isabelle_CI_Builds(
AFP_Build.afp,
AFP_Build.all,
AFP_Build.slow,
AFP_Build.mac,
AFP_Build.testboard)
diff --git a/tools/afp_check_metadata.scala b/tools/afp_check_metadata.scala
--- a/tools/afp_check_metadata.scala
+++ b/tools/afp_check_metadata.scala
@@ -1,198 +1,198 @@
/* Author: Fabian Huch, TU Muenchen
Tool to check metadata consistency.
*/
package afp
import isabelle.*
-import afp.Metadata.{Author, DOI, Email, Homepage, TOML, Topic}
+import afp.Metadata.TOML
import isabelle.TOML.{parse, Format, Key, Table}
object AFP_Check_Metadata {
def diff(t1: Table, t2: Table): List[Key] =
(t1.domain diff t2.domain).toList ++ t1.table.values.flatMap {
case (k, tr1) => t2.table.get(k).toList.flatMap(diff(tr1, _))
}
def afp_check_metadata(
afp_structure: AFP_Structure,
strict: Boolean = false,
reformat: Boolean = false,
format_all: Boolean = false,
slow: Boolean = false,
verbose: Boolean = false,
progress: Progress = new Progress
): Unit = {
def warn(msg: String): Unit = if (strict) error(msg) else progress.echo_warning(msg)
progress.echo_if(verbose, "Loading metadata...")
val authors = afp_structure.load_authors
val topics = afp_structure.load_topics
val licenses = afp_structure.load_licenses
val releases = afp_structure.load_releases
val entries = afp_structure.entries.map(name =>
afp_structure.load_entry(name, authors, topics, licenses, releases))
/* TOML encoding/decoding */
def check_toml[A](kind: String, a: A, from: A => Table, to: Table => A): Unit =
if (to(from(a)) != a) error("Inconsistent toml encode/decode: " + kind)
progress.echo_if(verbose, "Checking toml conversions...")
check_toml("authors", authors.values.toList, TOML.from_authors, TOML.to_authors)
check_toml("topics", Metadata.Topics.root_topics(topics), TOML.from_topics, TOML.to_topics)
check_toml("licenses", licenses.values.toList, TOML.from_licenses, TOML.to_licenses)
check_toml("releases", releases.values.flatten.toList, TOML.from_releases, TOML.to_releases)
entries.foreach(entry => check_toml("entry " + entry.name, entry, TOML.from_entry, t =>
TOML.to_entry(entry.name, t, authors, topics, licenses, releases.getOrElse(entry.name, Nil))))
/* duplicate ids */
var seen_ids = Set.empty[String]
def check_id(id: String): Unit =
if (seen_ids.contains(id)) error("Duplicate id: " + id) else seen_ids += id
progress.echo_if(verbose, "Checking for duplicate ids...")
authors.values.foreach { author =>
check_id(author.id)
author.emails.map(_.id).foreach(check_id)
author.homepages.map(_.id).foreach(check_id)
}
topics.values.map(_.id).foreach(check_id)
licenses.values.map(_.id).foreach(check_id)
entries.map(_.name).foreach(check_id)
/* unread fields */
progress.echo_if(verbose, "Checking for unused fields...")
def check_unused_toml[A](file: Path, to: Table => A, from: A => Table): Unit = {
val toml = parse(File.read(file))
val recoded = from(to(toml))
val diff_keys = diff(parse(File.read(file)), recoded)
if (diff_keys.nonEmpty) warn("Unused fields: " + commas_quote(diff_keys))
}
check_unused_toml(afp_structure.authors_file, TOML.to_authors, TOML.from_authors)
check_unused_toml(afp_structure.topics_file, TOML.to_topics, TOML.from_topics)
check_unused_toml(afp_structure.licenses_file, TOML.to_licenses, TOML.from_licenses)
check_unused_toml(afp_structure.releases_file, TOML.to_releases, TOML.from_releases)
entries.foreach(entry => check_unused_toml(afp_structure.entry_file(entry.name), t =>
TOML.to_entry(entry.name, t, authors, topics, licenses, releases.getOrElse(entry.name, Nil)),
TOML.from_entry))
/* unused values */
def warn_unused(name: String, unused: Set[String]): Unit =
if (unused.nonEmpty) warn("Extra (unused) " + name + ": " + commas_quote(unused.toList))
progress.echo_if(verbose, "Checking for unused values...")
val all_affils = entries.flatMap(entry => entry.authors ++ entry.contributors ++ entry.notifies)
warn_unused("authors", authors.keySet diff all_affils.map(_.author).toSet)
- def author_affil_id(author: Author.ID, affil: String): String = author + " " + affil
+ def author_affil_id(author: Metadata.Author.ID, affil: String): String = author + " " + affil
val affils = authors.values.flatMap(author =>
(author.emails.map(_.id) ++ author.homepages.map(_.id)).map(author_affil_id(author.id, _)))
val used_affils = all_affils.collect {
- case Email(author, id, _) => author_affil_id(author, id)
- case Homepage(author, id, _) => author_affil_id(author, id)
+ case Metadata.Email(author, id, _) => author_affil_id(author, id)
+ case Metadata.Homepage(author, id, _) => author_affil_id(author, id)
}
warn_unused("affiliations", affils.toSet diff used_affils.toSet)
val leaf_topics = topics.values.filter(_.sub_topics.isEmpty).map(_.id)
warn_unused("topics", leaf_topics.toSet diff entries.flatMap(_.topics).map(_.id).toSet)
warn_unused("licenses", licenses.keySet diff entries.map(_.license.id).toSet)
/* formatting of commonly patched files */
if (reformat) {
afp_structure.save_authors(authors.values.toList)
if (format_all) {
afp_structure.save_topics(Metadata.Topics.root_topics(topics))
afp_structure.save_licenses(licenses.values.toList)
afp_structure.save_releases(releases.values.toList.flatten)
entries.foreach(afp_structure.save_entry)
}
}
else {
def check_toml_format(toml: Table, file: Path): Unit = {
val present = File.read(file)
val formatted = Format(toml)
if (present != formatted) progress.echo_warning("Badly formatted toml: " + file)
}
progress.echo_if(verbose, "Checking formatting...")
check_toml_format(TOML.from_authors(authors.values.toList), afp_structure.authors_file)
if (format_all) {
check_toml_format(TOML.from_topics(topics.values.toList), afp_structure.topics_file)
check_toml_format(TOML.from_licenses(licenses.values.toList), afp_structure.licenses_file)
check_toml_format(TOML.from_releases(releases.values.toList.flatten),
afp_structure.releases_file)
entries.foreach(entry =>
check_toml_format(TOML.from_entry(entry), afp_structure.entry_file(entry.name)))
}
}
/* extra */
if (slow) {
progress.echo_if(verbose, "Checking DOIs...")
- entries.flatMap(entry => entry.related).collect { case d: DOI => d.formatted() }
+ entries.flatMap(entry => entry.related).collect { case d: Metadata.DOI => d.formatted() }
}
progress.echo_if(verbose, "Checked " + authors.size + " authors with " + affils.size +
" affiliations, " + topics.size + " topics, " + releases.values.flatten.size + " releases, " +
licenses.size + " licenses, and " + entries.size + " entries.")
}
val isabelle_tool = Isabelle_Tool("afp_check_metadata", "Checks the AFP metadata files",
Scala_Project.here,
{ args =>
var slow = false
var reformat = false
var format_all = false
var strict = false
var verbose = false
val getopts = Getopts("""
Usage: isabelle afp_check_metadata [OPTIONS]
Options are:
-a check formatting of all metadata
-s activate slow checks
-v verbose
-R reformat metadata files
-S strict mode (fail on warnings)
Check AFP metadata files for consistency.
""",
"a" -> (_ => format_all = true),
"s" -> (_ => slow = true),
"v" -> (_ => verbose = true),
"R" -> (_ => reformat = true),
"S" -> (_ => strict = true))
getopts(args)
val progress = new Console_Progress()
val afp_structure = AFP_Structure()
afp_check_metadata(afp_structure, strict = strict, reformat = reformat, format_all = format_all,
slow = slow, verbose = verbose, progress = progress)
})
}
diff --git a/tools/afp_dependencies.scala b/tools/afp_dependencies.scala
--- a/tools/afp_dependencies.scala
+++ b/tools/afp_dependencies.scala
@@ -1,85 +1,86 @@
/* Author: Fabian Huch, TU Muenchen
Tool to extract dependencies of AFP entries.
*/
package afp
import isabelle._
-import Metadata.Entry
-
object AFP_Dependencies {
- case class Dependency(entry: Entry.Name, distrib_deps: List[Entry.Name], afp_deps: List[Entry.Name])
+ case class Dependency(
+ entry: Metadata.Entry.Name,
+ distrib_deps: List[Metadata.Entry.Name],
+ afp_deps: List[Metadata.Entry.Name])
object JSON {
private def from_dep(dependency: Dependency): (String, isabelle.JSON.T) =
dependency.entry ->
isabelle.JSON.Object(
"distrib_deps" -> dependency.distrib_deps,
"afp_deps" -> dependency.afp_deps
)
def from_dependency(dep: Dependency): isabelle.JSON.T =
isabelle.JSON.Object(from_dep(dep))
def from_dependencies(deps: List[Dependency]): isabelle.JSON.T =
deps.map(from_dep).toMap
}
def afp_dependencies(afp_dir: Path): List[Dependency] = {
val tree = Sessions.load_structure(Options.init(), Nil, List(afp_dir))
val selected = tree.selection(Sessions.Selection(false, false, Nil, Nil, Nil, Nil))
.build_graph.keys
def get_entry(name: String): Option[String] =
{
val info = tree(name)
val dir = info.dir
if (selected.contains(dir.dir.expand))
None
else
Some(dir.base.implode)
}
selected.groupBy(get_entry).toList.collect {
case (Some(e), sessions) =>
val dependencies = sessions.flatMap(tree.imports_graph.imm_preds)
.map(d => (d, get_entry(d)))
val distrib_deps = dependencies.collect { case (d, None) => d }.distinct
val afp_deps = dependencies.collect { case (_, Some(d)) if d != e => d }.distinct
Dependency(e, distrib_deps, afp_deps)
}
}
val isabelle_tool = Isabelle_Tool("afp_dependencies", "extract dependencies between AFP entries",
Scala_Project.here,
{ args =>
var output_file: Option[Path] = None
val getopts = Getopts("""
Usage: isabelle afp_dependencies [OPTIONS]
Options are:
-o FILE output file name
Extract dependencies between AFP entries.
""",
"o:" -> (arg => output_file = Some(Path.explode(arg))))
getopts(args)
val afp_dir = Path.explode("$AFP").expand
val progress = new Console_Progress()
val res = afp_dependencies(afp_dir).map(JSON.from_dependency)
val json = isabelle.JSON.Format(res)
output_file match {
case Some(file) => File.write(file, json)
case None => progress.echo(json)
}
})
}
diff --git a/tools/afp_release.scala b/tools/afp_release.scala
--- a/tools/afp_release.scala
+++ b/tools/afp_release.scala
@@ -1,108 +1,106 @@
/* Author: Fabian Huch, TU Muenchen
Tooling to manage AFP releases.
*/
package afp
import isabelle.*
-import afp.Metadata.{Entry, Isabelle, Release}
-
import java.time.LocalDate
object AFP_Release {
def afp_import_releases(
user: String,
host: String,
releases_dir: Path,
base_dir: Path,
options: Options
): Unit = {
val Release_Tar = """afp-(.+)-(\d{4}-\d{2}-\d{2})\.tar\.gz""".r
val afp_structure = AFP_Structure(base_dir)
val isabelle_releases =
split_lines(File.read(afp_structure.metadata_dir + Path.basic("release-dates")))
val Isa_Release = """(.+) = (.+)""".r
val release_dates = isabelle_releases.filterNot(_.isBlank).map {
case Isa_Release(isabelle_version, date) => LocalDate.parse(date) -> isabelle_version
case line => error("Could not parse: " + quote(line))
}
using(SSH.open_session(options, host, user = user)) { ssh =>
val releases = ssh.read_dir(releases_dir).collect {
case Release_Tar(entry, date_str) =>
val date = LocalDate.parse(date_str)
release_dates.findLast { case (isa_date, _) => !isa_date.isAfter(date) } match {
- case Some(_, isabelle) => Release(entry, date, isabelle)
+ case Some(_, isabelle) => Metadata.Release(entry, date, isabelle)
case None => error("No Isabelle version found for " + date_str)
}
}
afp_structure.save_releases(releases)
}
}
- def afp_release(date: LocalDate, isabelle: Isabelle.Version, base_dir: Path): Unit = {
- def add_release(entry: Entry): Entry =
- entry.copy(releases = entry.releases :+ Release(entry.name, date, isabelle))
+ def afp_release(date: LocalDate, isabelle: Metadata.Isabelle.Version, base_dir: Path): Unit = {
+ def add_release(entry: Metadata.Entry): Metadata.Entry =
+ entry.copy(releases = entry.releases :+ Metadata.Release(entry.name, date, isabelle))
val afp_structure = AFP_Structure(base_dir)
val releases = afp_structure.load().values.toList.map(add_release).flatMap(_.releases)
afp_structure.save_releases(releases)
}
val isabelle_tool = Isabelle_Tool("afp_release", "Create an AFP release",
Scala_Project.here,
{ args =>
var isabelle = Isabelle_System.isabelle_identifier().getOrElse("")
var date = LocalDate.now()
var options = Options.init()
var releases: String = "afpweb@isa-afp.org:/srv/afp/release"
var import_releases = false
val getopts = Getopts("""
Usage: isabelle afp_release [OPTIONS]
Options are:
-i ID Isabelle id (default: """ + quote(isabelle) + """)
-d DATE release date (default: """ + quote(date.toString) + """)
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
-r REMOTE remote location of releases (default: """ + quote(releases) + """)"
-I import releases from directory instead
Register releases for old Isabelle version (when creating a new AFP release),
or import all releases from release dir.
""",
"i:" -> (arg => isabelle = arg),
"d:" -> (arg => date = LocalDate.parse(arg)),
"o:" -> (arg => options = options + arg),
"r:" -> (arg => releases = arg),
"I" -> (_ => import_releases = true))
getopts(args)
val base_dir = Path.explode("$AFP_BASE")
if (import_releases) {
val Remote = """([^@]+)@([^:]+):(.*)""".r
releases match {
case Remote(user, host, dir) =>
afp_import_releases(user = user, host = host, releases_dir = Path.explode(dir),
base_dir = base_dir, options = options)
case _ => error("Invalid remote: " + quote(releases))
}
}
else {
if (isabelle.isEmpty) getopts.usage()
afp_release(date, isabelle, base_dir)
}
})
}
diff --git a/tools/afp_submit.scala b/tools/afp_submit.scala
--- a/tools/afp_submit.scala
+++ b/tools/afp_submit.scala
@@ -1,1613 +1,1610 @@
/* Author: Fabian Huch, TU Muenchen
AFP submission system backend.
*/
package afp
import isabelle.*
import isabelle.HTML.*
import afp.Web_App.{ACTION, API, FILE, Params}
import afp.Web_App.Params.{List_Key, Nest_Key, empty}
import afp.Web_App.More_HTML.*
import afp.Metadata.{Affiliation, Author, Authors, DOI, Email, Entry, Formatted, Homepage, License, Licenses, Orcid, Reference, Release, Releases, Topic, Topics, Unaffiliated}
import java.text.Normalizer
import java.time.LocalDate
-import scala.collection.immutable.{ListMap, StringView}
-import scala.util.matching.Regex
-
object AFP_Submit {
object Val_Opt {
def ok[A](value: A): Val_Opt[A] = Val_Opt(Some(value), None)
def user_err[A](msg: String): Val_Opt[A] = Val_Opt(None, Some(msg))
def error[A]: Val_Opt[A] = Val_Opt(None, None)
}
case class Val_Opt[A] private(opt: Option[A], err: Option[String]) {
def is_empty: Boolean = opt.isEmpty
}
object Val {
def ok[A](value: A): Val[A] = Val(value, None)
def err[A](value: A, msg: String): Val[A] = Val(value, Some(msg))
}
case class Val[A] private(v: A, err: Option[String]) {
def with_err(err: String): Val[A] = Val.err(v, err)
def perhaps_err(opt: Val_Opt[_]): Val[A] = opt.err.map(with_err).getOrElse(this)
}
/* data model */
object Model {
object Related extends Enumeration {
val DOI, Plaintext = Value
def from_string(s: String): Option[Value] = values.find(_.toString == s)
def get(r: Reference): Value = r match {
case afp.Metadata.DOI(_) => DOI
case afp.Metadata.Formatted(_) => Plaintext
}
}
case class Create_Entry(
name: Val[String] = Val.ok(""),
title: Val[String] = Val.ok(""),
affils: Val[List[Affiliation]] = Val.ok(Nil),
notifies: Val[List[Email]] = Val.ok(Nil),
author_input: Option[Author] = None,
notify_input: Option[Author] = None,
topics: Val[List[Topic]] = Val.ok(Nil),
topic_input: Option[Topic] = None,
license: License,
`abstract`: Val[String] = Val.ok(""),
related: List[Reference] = Nil,
related_kind: Option[Related.Value] = None,
related_input: Val[String] = Val.ok("")
) {
def used_affils: Set[Affiliation] = (affils.v ++ notifies.v).toSet
def used_authors: Set[Author.ID] = used_affils.map(_.author)
}
case class Create(
entries: Val[List[Create_Entry]] = Val.ok(Nil),
new_authors: Val[List[Author]] = Val.ok(Nil),
new_author_input: String = "",
new_author_orcid: String = "",
new_affils: Val[List[Affiliation]] = Val.ok(Nil),
new_affils_author: Option[Author] = None,
new_affils_input: String = "",
) extends T {
def update_entry(num: Int, entry: Create_Entry): Create =
copy(entries = Val.ok(entries.v.updated(num, entry)))
def updated_authors(old_authors: Authors): Authors =
(old_authors ++ new_authors.v.map(author => author.id -> author)).map {
case (id, author) =>
val emails =
author.emails ++ new_affils.v.collect { case e: Email if e.author == id => e }
val homepages =
author.homepages ++ new_affils.v.collect { case h: Homepage if h.author == id => h }
id -> author.copy(emails = emails.distinct, homepages = homepages.distinct)
}
def used_affils: Set[Affiliation] = entries.v.toSet.flatMap(_.used_affils)
def used_authors: Set[Author.ID] =
new_affils.v.map(_.author).toSet ++ entries.v.flatMap(_.used_authors)
def create(authors: Authors): (Authors, List[Entry]) =
(updated_authors(authors), entries.v.map(entry =>
Entry(
name = entry.name.v,
title = entry.title.v,
authors = entry.affils.v,
date = LocalDate.now(),
topics = entry.topics.v,
`abstract` = entry.`abstract`.v.trim,
notifies = entry.notifies.v,
license = entry.license,
note = "",
related = entry.related)))
}
object Build extends Enumeration {
val Pending, Running, Aborted, Failed, Success = Value
}
object Status extends Enumeration {
val Submitted, Review, Added, Rejected = Value
def from_string(s: String): Option[Value] = values.find(_.toString == s)
}
case class Overview(id: String, date: LocalDate, name: String, status: Status.Value)
case class Metadata(authors: Authors, entries: List[Entry]) {
def new_authors(old_authors: Authors): Set[Author] =
entries.flatMap(_.authors).map(_.author).filterNot(old_authors.contains).toSet.map(authors)
def new_affils(old_authors: Authors): Set[Affiliation] =
entries.flatMap(entry => entry.authors ++ entry.notifies).toSet.filter {
case _: Unaffiliated => false
case e: Email => !old_authors.get(e.author).exists(_.emails.contains(e))
case h: Homepage => !old_authors.get(h.author).exists(_.homepages.contains(h))
}
}
sealed trait T
case object Invalid extends T
case class Upload(meta: Metadata, message: String, error: String = "") extends T
case class Created(id: String) extends T
case class Submission(
id: Handler.ID,
meta: Metadata,
message: String,
build: Build.Value,
status: Option[Status.Value],
log: String) extends T
case class Submission_List(submissions: List[Overview]) extends T
}
/* Physical submission handling */
trait Handler {
def create(
date: Date,
meta: Model.Metadata,
message: String,
archive: Bytes,
ext: String
): Handler.ID
def list(): Model.Submission_List
def get(id: Handler.ID, topics: Topics, licenses: Licenses): Option[Model.Submission]
def submit(id: Handler.ID): Unit
def set_status(id: Handler.ID, status: Model.Status.Value): Unit
def abort_build(id: Handler.ID): Unit
def get_patch(id: Handler.ID): Option[Path]
def get_archive(id: Handler.ID): Option[Path]
}
object Handler {
import Model._
type ID = String
object ID {
private val format = Date.Format.make(
List(
Date.Formatter.pattern("uuuu-MM-dd_HH-mm-ss_SSS"),
Date.Formatter.pattern("uuuu-MM-dd_HH-mm-ss_SSS_VV")),
_ + "_" + Date.timezone().getId)
def apply(submission_time: Date): ID = format(submission_time)
def unapply(id: ID): Option[Date] = format.unapply(id)
def check(id: ID): Option[ID] = unapply(id).map(apply)
}
/* Handler for local edits */
class Edit(afp_structure: AFP_Structure) extends Handler {
val authors = afp_structure.load_authors
val topics = afp_structure.load_topics
val licenses = afp_structure.load_licenses
val releases = afp_structure.load_releases
val dates = afp_structure.load().view.mapValues(_.date).toMap
def create(
date: Date,
meta: Metadata,
message: String,
archive: Bytes,
ext: String
): ID = {
val entry =
meta.entries match {
case e :: Nil => e
case _ => isabelle.error("Must be a single entry")
}
val old = afp_structure.load_entry(entry.name, authors, topics, licenses, releases)
val updated =
old.copy(
title = entry.title,
authors = entry.authors,
topics = entry.topics,
`abstract` = entry.`abstract`,
notifies = entry.notifies,
license = entry.license,
related = entry.related)
afp_structure.save_entry(updated)
// TODO what happens to the authors
entry.name
}
def list(): Submission_List =
Submission_List(afp_structure.entries.sortBy(dates.get).reverse.map { entry =>
Overview(entry, dates(entry), entry, Status.Added)
})
def get(id: ID, topics: Topics, licenses: Licenses): Option[Submission] =
if (!afp_structure.entries.contains(id)) None
else {
val entry = afp_structure.load_entry(id, authors, topics, licenses, releases)
val meta = Metadata(authors, List(entry))
Some(Submission(id, meta, "", Model.Build.Success, Some(Status.Added), ""))
}
def submit(id: ID): Unit = ()
def set_status(id: ID, status: Model.Status.Value): Unit = ()
def abort_build(id: ID): Unit = ()
def get_patch(id: ID): Option[Path] = None
def get_archive(id: ID): Option[Path] = None
}
/* Adapter to existing submission system */
class Adapter(submission_dir: Path, afp_structure: AFP_Structure) extends Handler {
private val up: Path = submission_dir + Path.basic("up")
private def up(id: ID): Path = up + Path.basic(id)
private def down(id: ID): Path = submission_dir + Path.basic("down") + Path.basic(id)
private def signal(id: ID, s: String): Unit =
File.write(up(id) + Path.basic(s), s.toUpperCase)
private def is_signal(id: ID, s: String): Boolean = (up(id) + Path.basic(s)).file.exists()
private def read_build(id: ID): Build.Value = {
val build = down(id) + Path.basic("result")
if (!build.file.exists) Build.Pending
else File.read(build).trim match {
case "" => Build.Running
case "NOT_FINISHED" => Build.Running
case "FAILED" => if (is_signal(id, "kill")) Build.Aborted else Build.Failed
case "SUCCESS" => Build.Success
case s => isabelle.error("Unkown build status: " + quote(s))
}
}
private def status_file(id: ID): Path = up(id) + Path.basic("AFP_STATUS")
private def read_status(id: ID): Option[Status.Value] = {
val status = status_file(id)
if (!status.file.exists()) None
else File.read(status).trim match {
case "SUBMITTED" => Some(Status.Submitted)
case "PROCESSING" => Some(Status.Review)
case "REJECTED" => Some(Status.Rejected)
case "ADDED" => Some(Status.Added)
case s => isabelle.error("Unknown status: " + quote(s))
}
}
private def info_file(id: ID): Path = up(id) + Path.basic("info.json")
private def patch_file(id: ID): Path = up(id) + Path.basic("patch")
private val archive_name: String = "archive"
def make_partial_patch(base_dir: Path, src: Path, dst: Path): String = {
val patch = Isabelle_System.make_patch(base_dir, src, dst, "--unidirectional-new-file")
split_lines(patch).filterNot(_.startsWith("Only in")).mkString("\n")
}
def create(date: Date, meta: Metadata, message: String, archive: Bytes, ext: String): ID = {
val id = ID(date)
val dir = up(id)
dir.file.mkdirs()
val structure = AFP_Structure(dir)
structure.save_authors(meta.authors.values.toList.sortBy(_.id))
meta.entries.foreach(structure.save_entry)
val archive_file = dir + Path.basic(archive_name + ext)
Bytes.write(archive_file, archive)
val metadata_rel =
File.relative_path(afp_structure.base_dir, afp_structure.metadata_dir).getOrElse(
afp_structure.metadata_dir)
val metadata_patch =
make_partial_patch(afp_structure.base_dir, metadata_rel, structure.metadata_dir)
File.write(patch_file(id), metadata_patch)
val info =
JSON.Format(JSON.Object(
"comment" -> message,
"entries" -> meta.entries.map(_.name),
"notify" -> meta.entries.flatMap(_.notifies).map(_.address).distinct))
File.write(info_file(id), info)
signal(id, "done")
id
}
def list(): Submission_List =
Submission_List(
File.read_dir(up).flatMap(ID.unapply).reverse.flatMap { date =>
val id = ID(date)
val day = date.rep.toLocalDate
read_status(id).map(Overview(id, day, AFP_Structure(up(id)).entries_unchecked.head, _))
})
def get(id: ID, topics: Topics, licenses: Licenses): Option[Submission] =
ID.check(id).filter(up(_).file.exists).map { id =>
val structure = AFP_Structure(up(id))
val authors = structure.load_authors
val entries = structure.entries_unchecked.map(
structure.load_entry(_, authors, topics, licenses, Releases.empty))
val log_file = down(id) + Path.basic("isabelle.log")
val log = if (log_file.file.exists) File.read(log_file) else ""
JSON.parse(File.read(info_file(id))) match {
case JSON.Object(m) if m.contains("comment") =>
val meta = Metadata(authors, entries)
Submission(id, meta, m("comment").toString, read_build(id), read_status(id), log)
case _ => isabelle.error("Could not read info")
}
}
private def check(id: ID): Option[ID] = ID.check(id).filter(up(_).file.exists)
def submit(id: ID): Unit = check(id).foreach(signal(_, "mail"))
def set_status(id: ID, status: Status.Value): Unit =
check(id).foreach { id =>
val content =
status match {
case Status.Submitted => "SUBMITTED"
case Status.Review => "PROCESSING"
case Status.Added => "ADDED"
case Status.Rejected => "REJECTED"
}
File.write(status_file(id), content)
}
def abort_build(id: ID): Unit = check(id).foreach(signal(_, "kill"))
def get_patch(id: ID): Option[Path] = check(id).map(patch_file)
def get_archive(id: ID): Option[Path] = check(id).flatMap { id =>
val dir = up(id)
File.read_dir(dir).find(_.startsWith(archive_name + ".")).map(dir + Path.basic(_))
}
}
}
/* server */
object Mode extends Enumeration {
val EDIT, SUBMISSION = Value
}
class Server(
api: API,
afp_structure: AFP_Structure,
mode: Mode.Value,
handler: Handler,
devel: Boolean,
verbose: Boolean,
progress: Progress,
port: Int = 0
) extends Web_App.Server[Model.T](api, port, verbose, progress) {
val repo = Mercurial.the_repository(afp_structure.base_dir)
var authors: Authors = Authors.empty
var topics: Topics = Topics.empty
var licenses: Licenses = Licenses.empty
var releases: Releases = Releases.empty
var entries: Set[Entry.Name] = Set.empty
private def load(): Unit = synchronized {
authors = afp_structure.load_authors
topics = afp_structure.load_topics
licenses = afp_structure.load_licenses
releases = afp_structure.load_releases
entries = afp_structure.entries.toSet
}
load()
/* endpoints */
val SUBMIT = Path.explode("submit")
val SUBMISSION = Path.explode("submission")
val SUBMISSIONS = Path.explode("submissions")
val API_SUBMISSION = Path.explode("api/submission")
val API_SUBMISSION_UPLOAD = Path.explode("api/submission/upload")
val API_SUBMISSION_CREATE = Path.explode("api/submission/create")
val API_SUBMISSION_STATUS = Path.explode("api/submission/status")
val API_RESUBMIT = Path.explode("api/resubmit")
val API_BUILD_ABORT = Path.explode("api/build/abort")
val API_SUBMIT = Path.explode("api/submit")
val API_SUBMISSION_AUTHORS_ADD = Path.explode("api/submission/authors/add")
val API_SUBMISSION_AUTHORS_REMOVE = Path.explode("api/submission/authors/remove")
val API_SUBMISSION_AFFILIATIONS_ADD = Path.explode("api/submission/affiliations/add")
val API_SUBMISSION_AFFILIATIONS_REMOVE = Path.explode("api/submission/affiliations/remove")
val API_SUBMISSION_ENTRIES_ADD = Path.explode("api/submission/entries/add")
val API_SUBMISSION_ENTRIES_REMOVE = Path.explode("api/submission/entries/remove")
val API_SUBMISSION_ENTRY_TOPICS_ADD = Path.explode("api/submission/entry/topics/add")
val API_SUBMISSION_ENTRY_TOPICS_REMOVE = Path.explode("api/submission/entry/topics/remove")
val API_SUBMISSION_ENTRY_AUTHORS_ADD = Path.explode("api/submission/entry/authors/add")
val API_SUBMISSION_ENTRY_AUTHORS_REMOVE = Path.explode("api/submission/entry/authors/remove")
val API_SUBMISSION_ENTRY_NOTIFIES_ADD = Path.explode("api/submission/entry/notifies/add")
val API_SUBMISSION_ENTRY_NOTIFIES_REMOVE = Path.explode("api/submission/entry/notifies/remove")
val API_SUBMISSION_ENTRY_RELATED_ADD = Path.explode("api/submission/entry/related/add")
val API_SUBMISSION_ENTRY_RELATED_REMOVE = Path.explode("api/submission/entry/related/remove")
val API_SUBMISSION_DOWNLOAD = Path.explode("api/download/patch")
val API_SUBMISSION_DOWNLOAD_ZIP = Path.explode("api/download/archive.zip")
val API_SUBMISSION_DOWNLOAD_TGZ = Path.explode("api/download/archive.tar.gz")
val API_CSS = Path.explode("api/main.css")
/* fields */
val ABSTRACT = "abstract"
val ADDRESS = "address"
val AFFILIATION = "affiliation"
val ARCHIVE = "archive"
val AUTHOR = "author"
val DATE = "date"
val ENTRY = "entry"
val ID = "id"
val INPUT = "input"
val KIND = "kind"
val LICENSE = "license"
val MESSAGE = "message"
val NAME = "name"
val NOTIFY = "notify"
val ORCID = "orcid"
val RELATED = "related"
val STATUS = "status"
val TITLE = "title"
val TOPIC = "topic"
/* utils */
def keyed(id: String, value: String): String = "[" + id + "] " + value
def author_string(author: Author): String = {
val orcid =
author.orcid.map(orcid => " (ORCID id: " + orcid.identifier + ")").getOrElse("")
keyed(author.id, author.name) + orcid
}
def author_option(author: Author): XML.Elem = option(author.id, author_string(author))
def affil_id(affil: Affiliation): String =
affil match {
case Unaffiliated(_) => ""
case Email(_, id, _) => id
case Homepage(_, id, _) => id
}
def affil_address(affil: Affiliation): String =
affil match {
case Unaffiliated(_) => ""
case Email(_, _, address) => address
case Homepage(_, _, url) => url.toString
}
def affil_string(affil: Affiliation): String =
affil match {
case Unaffiliated(_) => "No email or homepage"
case Email(_, id, address) => keyed(id, address)
case Homepage(_, id, url) => keyed(id, url.toString)
}
def related_string(related: Reference): String = related match {
case Metadata.DOI(identifier) => identifier
case Metadata.Formatted(rep) => rep
}
def indexed[A, B](l: List[A], key: Params.Key, field: String, f: (A, Params.Key) => B) =
l.zipWithIndex map {
case (a, i) => f(a, List_Key(key, field, i))
}
def fold[A](it: List[Params.Data], a: A)(f: (Params.Data, A) => Option[A]): Option[A] =
it.foldLeft(Option(a)) {
case (None, _) => None
case (Some(a), param) => f(param, a)
}
def download_link(href: String, body: XML.Body): XML.Elem =
class_("download")(link(href, body)) + ("target" -> "_blank")
def frontend_link(path: Path, params: Properties.T, body: XML.Body): XML.Elem =
link(api.app_url(path, params), body) + ("target" -> "_parent")
def render_if(cond: Boolean, body: XML.Body): XML.Body = if (cond) body else Nil
def render_if(cond: Boolean, elem: XML.Elem): XML.Body = if (cond) List(elem) else Nil
def render_error(for_elem: String, validated: Val[_]): XML.Body =
validated.err.map(error =>
break ::: List(css("color: red")(label(for_elem, error)))).getOrElse(Nil)
/* view */
def render_create(model: Model.Create): XML.Body = {
val updated_authors = model.updated_authors(authors)
val authors_list = updated_authors.values.toList.sortBy(_.id)
val (entry_authors, other_authors) =
updated_authors.values.toList.sortBy(_.id).partition(author =>
model.used_authors.contains(author.id))
val email_authors = authors_list.filter(_.emails.nonEmpty)
def render_topic(topic: Topic, key: Params.Key): XML.Elem =
par(
hidden(Nest_Key(key, ID), topic.id) ::
text(topic.id) :::
action_button(api.api_url(API_SUBMISSION_ENTRY_TOPICS_REMOVE), "x", key) :: Nil)
def render_affil(affil: Affiliation, key: Params.Key): XML.Elem = {
val author = updated_authors(affil.author)
val affils = author.emails ::: author.homepages ::: Unaffiliated(author.id) :: Nil
par(
hidden(Nest_Key(key, ID), affil.author) ::
text(author_string(updated_authors(affil.author))) :::
selection(Nest_Key(key, AFFILIATION),
Some(affil_id(affil)),
affils.map(affil => option(affil_id(affil), affil_string(affil)))) ::
action_button(api.api_url(API_SUBMISSION_ENTRY_AUTHORS_REMOVE), "x", key) :: Nil)
}
def render_notify(email: Email, key: Params.Key): XML.Elem = {
val author = updated_authors(email.author)
par(
hidden(Nest_Key(key, ID), email.author) ::
text(author_string(updated_authors(email.author))) :::
selection(
Nest_Key(key, AFFILIATION),
Some(affil_id(email)),
author.emails.map(affil => option(affil_id(affil), affil_string(affil)))) ::
action_button(api.api_url(API_SUBMISSION_ENTRY_NOTIFIES_REMOVE), "x", key) :: Nil)
}
def render_related(related: Reference, key: Params.Key): XML.Elem =
par(
hidden(Nest_Key(key, KIND), Model.Related.get(related).toString) ::
hidden(Nest_Key(key, INPUT), related_string(related)) ::
text(related_string(related)) :::
action_button(api.api_url(API_SUBMISSION_ENTRY_RELATED_REMOVE), "x", key) :: Nil)
def render_entry(entry: Model.Create_Entry, key: Params.Key): XML.Elem =
fieldset(legend("Entry") ::
par(
fieldlabel(Nest_Key(key, TITLE), "Title of article") ::
textfield(Nest_Key(key, TITLE), "Example Submission", entry.title.v) ::
render_error(Nest_Key(key, TITLE), entry.title)) ::
par(
fieldlabel(Nest_Key(key, NAME), "Short name") ::
textfield(Nest_Key(key, NAME), "Example_Submission", entry.name.v) ::
explanation(Nest_Key(key, NAME),
"Name of the folder where your ROOT and theory files reside.") ::
render_error(Nest_Key(key, NAME), entry.name)) ::
fieldset(legend("Topics") ::
indexed(entry.topics.v, key, TOPIC, render_topic) :::
selection(Nest_Key(key, TOPIC),
entry.topic_input.map(_.id),
topics.values.toList.map(topic => option(topic.id, topic.id))) ::
action_button(api.api_url(API_SUBMISSION_ENTRY_TOPICS_ADD), "add", key) ::
render_error("", entry.topics)) ::
par(List(
fieldlabel(Nest_Key(key, LICENSE), "License"),
radio(Nest_Key(key, LICENSE),
entry.license.id,
licenses.values.toList.map(license => license.id -> license.name)),
explanation(Nest_Key(key, LICENSE),
"Note: For LGPL submissions, please include the header \"License: LGPL\" in each file"))) ::
par(
fieldlabel(Nest_Key(key, ABSTRACT), "Abstract") ::
placeholder("HTML and MathJax, no LaTeX")(
textarea(Nest_Key(key, ABSTRACT), entry.`abstract`.v) +
("rows" -> "8") +
("cols" -> "70")) ::
explanation(Nest_Key(key, ABSTRACT),
"Note: You can use HTML or MathJax (not LaTeX!) to format your abstract.") ::
render_error(Nest_Key(key, ABSTRACT), entry.`abstract`)) ::
fieldset(legend("Authors") ::
indexed(entry.affils.v, key, AUTHOR, render_affil) :::
selection(Nest_Key(key, AUTHOR),
entry.author_input.map(_.id),
authors_list.map(author => option(author.id, author_string(author)))) ::
action_button(api.api_url(API_SUBMISSION_ENTRY_AUTHORS_ADD), "add", key) ::
explanation(Nest_Key(key, AUTHOR),
"Add an author from the list. Register new authors first below.") ::
render_error(Nest_Key(key, AUTHOR), entry.affils)) ::
fieldset(legend("Contact") ::
indexed(entry.notifies.v, key, NOTIFY, render_notify) :::
selection(Nest_Key(key, NOTIFY),
entry.notify_input.map(_.id),
optgroup("Suggested", email_authors.filter(author =>
entry.used_authors.contains(author.id)).map(author_option)) ::
email_authors.filter(author =>
!entry.used_authors.contains(author.id)).map(author_option)) ::
action_button(api.api_url(API_SUBMISSION_ENTRY_NOTIFIES_ADD), "add", key) ::
explanation(Nest_Key(key, NOTIFY),
"These addresses serve two purposes: " +
"1. They are used to send you updates about the state of your submission. " +
"2. They are the maintainers of the entry once it is accepted. " +
"Typically this will be one or more of the authors.") ::
render_error("", entry.notifies)) ::
fieldset(legend("Related Publications") ::
indexed(entry.related, key, RELATED, render_related) :::
selection(Nest_Key(Nest_Key(key, RELATED), KIND),
entry.related_kind.map(_.toString),
Model.Related.values.toList.map(v => option(v.toString, v.toString))) ::
textfield(Nest_Key(Nest_Key(key, RELATED), INPUT),
"10.1109/5.771073", entry.related_input.v) ::
action_button(api.api_url(API_SUBMISSION_ENTRY_RELATED_ADD), "add", key) ::
explanation(Nest_Key(Nest_Key(key, RELATED), INPUT),
"Publications related to the entry, as DOIs (10.1109/5.771073) or plaintext (HTML)." +
"Typically a publication by the authors describing the entry," +
" background literature (articles, books) or web resources. ") ::
render_error(Nest_Key(Nest_Key(key, RELATED), INPUT), entry.related_input)) ::
render_if(mode == Mode.SUBMISSION,
action_button(api.api_url(API_SUBMISSION_ENTRIES_REMOVE), "remove entry", key)))
def render_new_author(author: Author, key: Params.Key): XML.Elem =
par(
hidden(Nest_Key(key, ID), author.id) ::
hidden(Nest_Key(key, NAME), author.name) ::
hidden(Nest_Key(key, ORCID), author.orcid.map(_.identifier).getOrElse("")) ::
text(author_string(author)) :::
render_if(!model.used_authors.contains(author.id),
action_button(api.api_url(API_SUBMISSION_AUTHORS_REMOVE), "x", key)))
def render_new_affil(affil: Affiliation, key: Params.Key): XML.Elem =
par(
hidden(Nest_Key(key, AUTHOR), affil.author) ::
hidden(Nest_Key(key, ID), affil_id(affil)) ::
hidden(Nest_Key(key, AFFILIATION), affil_address(affil)) ::
text(author_string(updated_authors(affil.author)) + ": " + affil_string(affil)) :::
render_if(!model.used_affils.contains(affil),
action_button(api.api_url(API_SUBMISSION_AFFILIATIONS_REMOVE), "x", key)))
val (upload, preview) = mode match {
case Mode.EDIT => ("Save", "preview and save >")
case Mode.SUBMISSION => ("Upload", "preview and upload >")
}
List(submit_form(api.api_url(API_SUBMISSION),
indexed(model.entries.v, Params.empty, ENTRY, render_entry) :::
render_error("", model.entries) :::
render_if(mode == Mode.SUBMISSION,
par(List(
explanation("",
"You can submit multiple entries at once. " +
"Put the corresponding folders in the archive " +
"and use the button below to add more input fields for metadata. "),
api_button(api.api_url(API_SUBMISSION_ENTRIES_ADD), "additional entry")))) :::
break :::
fieldset(legend("New Authors") ::
explanation("", "If you are new to the AFP, add yourself here.") ::
indexed(model.new_authors.v, Params.empty, AUTHOR, render_new_author) :::
fieldlabel(Nest_Key(AUTHOR, NAME), "Name") ::
textfield(Nest_Key(AUTHOR, NAME), "Gerwin Klein", model.new_author_input) ::
fieldlabel(Nest_Key(AUTHOR, ORCID), "ORCID id (optional)") ::
textfield(Nest_Key(AUTHOR, ORCID), "0000-0002-1825-0097", model.new_author_orcid) ::
api_button(api.api_url(API_SUBMISSION_AUTHORS_ADD), "add") ::
render_error("", model.new_authors)) ::
fieldset(legend("New email or homepage") ::
explanation("",
"Add new email or homepages here. " +
"If you would like to update an existing, " +
"submit with the old one and write to the editors.") ::
indexed(model.new_affils.v, Params.empty, AFFILIATION, render_new_affil) :::
fieldlabel(AFFILIATION, "Author") ::
selection(AFFILIATION,
model.new_affils_author.map(_.id),
optgroup("Entry authors", entry_authors.map(author_option)) ::
other_authors.map(author_option)) ::
fieldlabel(Nest_Key(AFFILIATION, ADDRESS), "Email or Homepage") ::
textfield(Nest_Key(AFFILIATION, ADDRESS), "https://proofcraft.org",
model.new_affils_input) ::
api_button(api.api_url(API_SUBMISSION_AFFILIATIONS_ADD), "add") ::
render_error("", model.new_affils)) ::
break :::
fieldset(List(legend(upload),
api_button(api.api_url(API_SUBMISSION_UPLOAD), preview))) :: Nil))
}
def render_metadata(meta: Model.Metadata): XML.Body = {
def render_topic(topic: Topic, key: Params.Key): XML.Elem =
item(hidden(Nest_Key(key, ID), topic.id) :: text(topic.id))
def render_affil(affil: Affiliation, key: Params.Key): XML.Elem =
item(
hidden(Nest_Key(key, ID), affil.author) ::
hidden(Nest_Key(key, AFFILIATION), affil_id(affil)) ::
text(author_string(meta.authors(affil.author)) + ", " + affil_string(affil)))
def render_related(related: Reference, key: Params.Key): XML.Elem =
item(
hidden(Nest_Key(key, KIND), Model.Related.get(related).toString) ::
hidden(Nest_Key(key, INPUT), related_string(related)) ::
input_raw(related_string(related)) :: Nil)
def render_entry(entry: Entry, key: Params.Key): XML.Elem =
fieldset(List(
legend("Entry"),
par(
fieldlabel(Nest_Key(key, TITLE), "Title") ::
hidden(Nest_Key(key, TITLE), entry.title) ::
text(entry.title)),
par(
fieldlabel(Nest_Key(key, NAME), "Short Name") ::
hidden(Nest_Key(key, NAME), entry.name) ::
text(entry.name)),
par(
fieldlabel(Nest_Key(key, DATE), "Date") ::
hidden(Nest_Key(key, DATE), entry.date.toString) ::
text(entry.date.toString)),
par(List(
fieldlabel("", "Topics"),
list(indexed(entry.topics, key, TOPIC, render_topic)))),
par(
fieldlabel(Nest_Key(key, LICENSE), "License") ::
hidden(Nest_Key(key, LICENSE), entry.license.id) ::
text(entry.license.name)),
par(List(
fieldlabel(Nest_Key(key, ABSTRACT), "Abstract"),
hidden(Nest_Key(key, ABSTRACT), entry.`abstract`),
class_("mathjax_process")(span(List(input_raw(entry.`abstract`)))))),
par(List(
fieldlabel("", "Authors"),
list(indexed(entry.authors, key, AUTHOR, render_affil)))),
par(List(
fieldlabel("", "Contact"),
list(indexed(entry.notifies, key, NOTIFY, render_affil)))),
par(List(
fieldlabel("", "Related Publications"),
list(indexed(entry.related, key, RELATED, render_related))))))
def render_new_author(author: Author, key: Params.Key): XML.Elem =
par(List(
hidden(Nest_Key(key, ID), author.id),
hidden(Nest_Key(key, NAME), author.name),
hidden(Nest_Key(key, ORCID), author.orcid.map(_.identifier).getOrElse(""))))
def render_new_affil(affil: Affiliation, key: Params.Key): XML.Elem =
par(List(
hidden(Nest_Key(key, AUTHOR), affil.author),
hidden(Nest_Key(key, ID), affil_id(affil)),
hidden(Nest_Key(key, AFFILIATION), affil_address(affil))))
indexed(meta.entries, Params.empty, ENTRY, render_entry) :::
indexed(meta.new_authors(authors).toList, Params.empty, AUTHOR, render_new_author) :::
indexed(meta.new_affils(authors).toList, Params.empty, AFFILIATION, render_new_affil)
}
def render_submission(submission: Model.Submission): XML.Body = {
def status_text(status: Option[Model.Status.Value]): String =
status.map {
case Model.Status.Submitted => "AFP editors notified."
case Model.Status.Review => "Review in progress."
case Model.Status.Added => "Added to the AFP."
case Model.Status.Rejected => "Submission rejected."
} getOrElse
"Draft saved. Check the logs for errors and warnings, " +
"and submit to editors once successfully built."
val archive_url =
if (handler.get_archive(submission.id).exists(_.get_ext == "zip"))
API_SUBMISSION_DOWNLOAD_ZIP
else API_SUBMISSION_DOWNLOAD_TGZ
val resubmit = mode match {
case Mode.EDIT => "Update"
case Mode.SUBMISSION => "Resubmit"
}
List(submit_form(api.api_url(SUBMISSION, List(ID -> submission.id)),
render_if(mode == Mode.SUBMISSION,
download_link(api.api_url(archive_url, List(ID -> submission.id)), text("archive")) ::
download_link(api.api_url(API_SUBMISSION_DOWNLOAD, List(ID -> submission.id)),
text("metadata patch")) ::
text(" (apply with: 'patch -p0 < FILE')")) :::
render_if(mode == Mode.SUBMISSION, par(
hidden(MESSAGE, submission.message) ::
text("Comment: " + submission.message))) :::
section("Metadata") ::
render_metadata(submission.meta) :::
section("Status") ::
span(text(status_text(submission.status))) ::
render_if(submission.build != Model.Build.Running,
action_button(api.api_url(API_RESUBMIT), resubmit, submission.id)) :::
render_if(submission.build == Model.Build.Running,
action_button(api.api_url(API_BUILD_ABORT), "Abort build", submission.id)) :::
render_if(submission.build == Model.Build.Success && submission.status.isEmpty,
action_button(api.api_url(API_SUBMIT), "Send submission to AFP editors", submission.id)) :::
render_if(mode == Mode.SUBMISSION,
fieldset(legend("Build") ::
bold(text(submission.build.toString)) ::
par(text("Isabelle log:") ::: source(submission.log) :: Nil) ::
Nil))))
}
def render_upload(upload: Model.Upload): XML.Body = {
val submit = mode match {
case Mode.EDIT => "save"
case Mode.SUBMISSION => "submit"
}
List(submit_form(api.api_url(API_SUBMISSION), List(
fieldset(legend("Overview") :: render_metadata(upload.meta)),
fieldset(legend("Submit") ::
api_button(api.api_url(API_SUBMISSION), "< edit metadata") ::
render_if(mode == Mode.SUBMISSION, List(
par(List(
fieldlabel(MESSAGE, "Message for the editors (optional)"),
textfield(MESSAGE, "", upload.message),
explanation(
MESSAGE,
"Note: Anything special or noteworthy about your submission can be covered here. " +
"It will not become part of your entry. " +
"You're also welcome to leave suggestions for our AFP submission service here. ")
)),
par(List(
fieldlabel(ARCHIVE, "Archive file (.tar.gz or .zip)"),
browse(ARCHIVE, List(".zip", ".tar.gz")),
explanation(ARCHIVE,
"Note: Your zip or tar file must contain exactly one folder for each entry with your theories, ROOT, etc. " +
"The folder name must be the short/folder name used in the submission form. " +
"Hidden files and folders (e.g., __MACOSX) are not allowed."))))) :::
api_button(api.api_url(API_SUBMISSION_CREATE), submit) ::
render_error(ARCHIVE, Val.err((), upload.error))))))
}
def render_submission_list(submission_list: Model.Submission_List): XML.Body = {
def render_overview(overview: Model.Overview, key: Params.Key): XML.Elem =
item(
hidden(Nest_Key(key, ID), overview.id) ::
hidden(Nest_Key(key, DATE), overview.date.toString) ::
hidden(Nest_Key(key, NAME), overview.name) ::
span(text(overview.date.toString)) ::
span(List(frontend_link(SUBMISSION, List(ID -> overview.id),
text(overview.name)))) ::
render_if(mode == Mode.SUBMISSION,
class_("right")(span(List(
selection(Nest_Key(key, STATUS), Some(overview.status.toString),
Model.Status.values.toList.map(v => option(v.toString, v.toString))),
action_button(api.api_url(API_SUBMISSION_STATUS), "update", key))))))
def list1(ls: List[XML.Elem]): XML.Elem = if (ls.isEmpty) par(Nil) else list(ls)
val ls = indexed(submission_list.submissions, Params.empty, ENTRY, (o, k) => (o, k))
val finished =
ls.filter(t => Set(Model.Status.Added, Model.Status.Rejected).contains(t._1.status))
List(submit_form(api.api_url(API_SUBMISSION_STATUS),
render_if(mode == Mode.SUBMISSION,
text("Open") :::
list1(ls.filter(_._1.status == Model.Status.Submitted).map(render_overview)) ::
text("In Progress") :::
list1(ls.filter(_._1.status == Model.Status.Review).map(render_overview)) ::
text("Finished")) :::
list1(finished.map(render_overview)) :: Nil))
}
def render_created(created: Model.Created): XML.Body = {
val status = mode match {
case Mode.SUBMISSION => "View your submission status: "
case Mode.EDIT => "View the entry at: "
}
List(div(
span(text("Entry successfully saved. " + status)) ::
break :::
frontend_link(SUBMISSION, List(ID -> created.id),
text(api.app_url(SUBMISSION, List(ID -> created.id)))) ::
break :::
render_if(mode == Mode.SUBMISSION, span(text("(keep that url!).")))))
}
def render_invalid: XML.Body = text("Invalid request")
def render(model: Model.T): XML.Body =
model match {
case create: Model.Create => render_create(create)
case upload: Model.Upload => render_upload(upload)
case submission: Model.Submission => render_submission(submission)
case submissions: Model.Submission_List => render_submission_list(submissions)
case created: Model.Created => render_created(created)
case Model.Invalid => render_invalid
}
/* validation */
def validate_topic(id: String, selected: List[Topic]): Val_Opt[Topic] =
if (id.isEmpty) Val_Opt.user_err("Select topic first")
else {
topics.values.find(_.id == id) match {
case Some(topic) =>
if (selected.contains(topic)) Val_Opt.user_err("Topic already selected")
else Val_Opt.ok(topic)
case _ => Val_Opt.error
}
}
def validate_new_author(
id: String,
name: String,
orcid_str: String,
authors: Authors
): Val_Opt[Author] = {
val Id = """[a-zA-Z][a-zA-Z0-9]*""".r
id match {
case Id() if !authors.contains(id) =>
if (name.isEmpty || name.trim != name)
Val_Opt.user_err("Name must not be empty")
else if (orcid_str.isEmpty)
Val_Opt.ok(Author(id, name))
else Exn.capture(Orcid(orcid_str)) match {
case Exn.Res(orcid) =>
if (authors.values.exists(_.orcid.exists(_ == orcid)))
Val_Opt.user_err("Author with that orcid already exists")
else Val_Opt.ok(Author(id, name, orcid = Some(orcid)))
case _ => Val_Opt.user_err("Invalid orcid")
}
case _ => Val_Opt.error
}
}
def validate_new_affil(id: String, address: String, author: Author): Val_Opt[Affiliation] = {
if (address.isBlank) Val_Opt.user_err("Address must not be empty")
else if (address.contains("@")) {
val Id = (author.id + """_email\d*""").r
id match {
case Id() if !author.emails.map(_.id).contains(id) =>
val Address = """([^@\s]+)@([^@\s]+)""".r
address match {
case Address(user, host) => Val_Opt.ok(Email(author.id, id, user, host))
case _ => Val_Opt.user_err("Invalid email address")
}
case _ => Val_Opt.error
}
}
else {
val Id = (author.id + """_homepage\d*""").r
id match {
case Id() if !author.homepages.map(_.id).contains(id) =>
if (Url.is_wellformed(address)) Val_Opt.ok(Homepage(author.id, id, Url(address)))
else Val_Opt.user_err("Invalid url")
case _ => Val_Opt.error
}
}
}
def validate_related(
kind: Model.Related.Value,
related: String,
references: List[Reference]
): Val_Opt[Reference] =
if (related.isBlank) Val_Opt.user_err("Reference must not be empty")
else {
kind match {
case Model.Related.DOI =>
Exn.capture(DOI(related)) match {
case Exn.Res(doi) =>
if (references.contains(doi)) Val_Opt.user_err("Already present")
else Val_Opt.ok(doi)
case _ => Val_Opt.user_err("Invalid DOI format")
}
case Model.Related.Plaintext =>
val formatted = Formatted(related)
if (references.contains(formatted)) Val_Opt.user_err("Already present")
else Val_Opt.ok(formatted)
}
}
/* param parsing */
def parse_create(params: Params.Data): Option[Model.Create] = {
def parse_topic(topic: Params.Data, topics: List[Topic]): Option[Topic] =
validate_topic(topic.get(ID).value, topics).opt
def parse_email(email: Params.Data, authors: Authors): Option[Email] =
authors.get(email.get(ID).value).flatMap(
_.emails.find(_.id == email.get(AFFILIATION).value))
def parse_affil(affil: Params.Data, authors: Authors): Option[Affiliation] =
authors.get(affil.get(ID).value).flatMap { author =>
val id = affil.get(AFFILIATION).value
if (id.isEmpty) Some(Unaffiliated(author.id))
else (author.emails ++ author.homepages).collectFirst {
case e: Email if e.id == id => e
case h: Homepage if h.id == id => h
}
}
def parse_related(related: Params.Data, references: List[Reference]): Option[Reference] =
Model.Related.from_string(related.get(KIND).value).flatMap(
validate_related(_, related.get(INPUT).value, references).opt)
def parse_new_author(author: Params.Data, authors: Authors): Option[Author] =
validate_new_author(
author.get(ID).value, author.get(NAME).value, author.get(ORCID).value, authors).opt
def parse_new_affil(affil: Params.Data, authors: Authors): Option[Affiliation] =
authors.get(affil.get(AUTHOR).value).flatMap(author =>
validate_new_affil(affil.get(ID).value, affil.get(AFFILIATION).value, author).opt)
def parse_entry(entry: Params.Data, authors: Authors): Option[Model.Create_Entry] =
for {
topics <-
fold(entry.list(TOPIC), List.empty[Topic]) {
case (topic, topics) => parse_topic(topic, topics).map(topics :+ _)
}
affils <-
fold(entry.list(AUTHOR), List.empty[Affiliation]) {
case (affil, affils) => parse_affil(affil, authors).map(affils :+ _)
}
notifies <-
fold(entry.list(NOTIFY), List.empty[Email]) {
case (email, emails) => parse_email(email, authors).map(emails :+ _)
}
related <-
fold(entry.list(RELATED), List.empty[Reference]) {
case (related, references) => parse_related(related, references).map(references :+ _)
}
license <- licenses.get(entry.get(LICENSE).value)
} yield Model.Create_Entry(
name = Val.ok(entry.get(NAME).value),
title = Val.ok(entry.get(TITLE).value),
topics = Val.ok(topics),
topic_input = parse_topic(entry.get(TOPIC), Nil),
license = license,
`abstract` = Val.ok(entry.get(ABSTRACT).value),
author_input = authors.get(entry.get(AUTHOR).value),
notify_input = authors.get(entry.get(NOTIFY).value),
affils = Val.ok(affils),
notifies = Val.ok(notifies),
related = related,
related_kind = Model.Related.from_string(entry.get(RELATED).get(KIND).value),
related_input = Val.ok(entry.get(RELATED).get(INPUT).value))
for {
(new_author_ids, all_authors) <-
fold(params.list(AUTHOR), (List.empty[Author.ID], authors)) {
case (author, (new_authors, authors)) =>
parse_new_author(author, authors).map(author =>
(new_authors :+ author.id, authors.updated(author.id, author)))
}
(new_affils, all_authors) <-
fold(params.list(AFFILIATION), (List.empty[Affiliation], all_authors)) {
case (affil, (new_affils, authors)) =>
parse_new_affil(affil, authors).map { affil =>
val author = authors(affil.author)
(new_affils :+ affil, affil match {
case _: Unaffiliated => authors
case e: Email =>
authors.updated(author.id, author.copy(emails = author.emails :+ e))
case h: Homepage =>
authors.updated(author.id, author.copy(homepages = author.homepages :+ h))
})
}
}
new_authors = new_author_ids.map(all_authors)
entries <- fold(params.list(ENTRY), List.empty[Model.Create_Entry]) {
case (entry, entries) => parse_entry(entry, all_authors).map(entries :+ _)
}
} yield Model.Create(
entries = Val.ok(entries),
new_authors = Val.ok(new_authors),
new_author_input = params.get(AUTHOR).get(NAME).value,
new_author_orcid = params.get(AUTHOR).get(ORCID).value,
new_affils = Val.ok(new_affils),
new_affils_author = all_authors.get(params.get(AFFILIATION).value),
new_affils_input = params.get(AFFILIATION).get(ADDRESS).value)
}
def parse_submission_list(params: Params.Data): Option[Model.Submission_List] = {
def parse_overview(entry: Params.Data): Option[Model.Overview] =
for {
date <-
Exn.capture(LocalDate.parse(entry.get(DATE).value)) match {
case Exn.Res(date) => Some(date)
case Exn.Exn(_) => None
}
status <- Model.Status.from_string(entry.get(STATUS).value)
} yield Model.Overview(entry.get(ID).value, date, entry.get(NAME).value, status)
val submissions =
fold(params.list(ENTRY), List.empty[Model.Overview]) {
case (entry, overviews) => parse_overview(entry).map(overviews :+ _)
}
submissions.map(Model.Submission_List.apply)
}
/* control */
def add_entry(params: Params.Data): Option[Model.T] = parse_create(params).map { model =>
model.copy(entries = Val.ok(model.entries.v :+ Model.Create_Entry(license = licenses.head._2)))
}
def remove_entry(params: Params.Data): Option[Model.T] =
for {
model <- parse_create(params)
num_entry <- List_Key.num(ENTRY, params.get(Web_App.ACTION).value)
} yield model.copy(entries = Val.ok(Utils.remove_at(num_entry, model.entries.v)))
def add_author(params: Params.Data): Option[Model.T] =
for {
model <- parse_create(params)
num_entry <- List_Key.num(ENTRY, params.get(Web_App.ACTION).value)
entry <- model.entries.v.unapply(num_entry)
} yield
entry.author_input match {
case None =>
model.update_entry(num_entry, entry.copy(
affils = entry.affils.with_err("Select author first")))
case Some(author) =>
val default_affil = author.emails.headOption.orElse(
author.homepages.headOption).getOrElse(Unaffiliated(author.id))
model.update_entry(num_entry, entry.copy(
author_input = None, affils = Val.ok(entry.affils.v :+ default_affil)))
}
def remove_author(params: Params.Data): Option[Model.T] =
for {
model <- parse_create(params)
(action, num_affil) <- List_Key.split(AUTHOR, params.get(Web_App.ACTION).value)
num_entry <- List_Key.num(ENTRY, action)
entry <- model.entries.v.unapply(num_entry)
} yield
model.update_entry(num_entry, entry.copy(affils =
Val.ok(Utils.remove_at(num_affil, entry.affils.v))))
def add_notify(params: Params.Data): Option[Model.T] =
for {
model <- parse_create(params)
num_entry <- List_Key.num(ENTRY, params.get(Web_App.ACTION).value)
entry <- model.entries.v.unapply(num_entry)
entry1 <-
entry.notify_input match {
case Some(author) =>
author.emails.headOption.map(email => entry.copy(
notify_input = None, notifies = Val.ok(entry.notifies.v :+ email)))
case None =>
Some(entry.copy(notifies = entry.notifies.with_err("Select author first")))
}
} yield model.update_entry(num_entry, entry1)
def remove_notify(params: Params.Data): Option[Model.T] =
for {
model <- parse_create(params)
(action, num_notify) <- List_Key.split(NOTIFY, params.get(Web_App.ACTION).value)
num_entry <- List_Key.num(ENTRY, action)
entry <- model.entries.v.unapply(num_entry)
} yield
model.update_entry(num_entry, entry.copy(notifies =
Val.ok(Utils.remove_at(num_notify, entry.notifies.v))))
def add_topic(params: Params.Data): Option[Model.T] =
for {
model <- parse_create(params)
num_entry <- List_Key.num(ENTRY, params.get(Web_App.ACTION).value)
entry <- model.entries.v.unapply(num_entry)
entry_params <- params.list(ENTRY).unapply(num_entry)
} yield {
val topic = validate_topic(entry_params.get(TOPIC).value, entry.topics.v)
val topic_input = if (topic.is_empty) entry.topic_input else None
model.update_entry(num_entry, entry.copy(
topic_input = topic_input,
topics = Val.ok(entry.topics.v ++ topic.opt).perhaps_err(topic)))
}
def remove_topic(params: Params.Data): Option[Model.T] =
for {
model <- parse_create(params)
(action, num_topic) <- List_Key.split(TOPIC, params.get(Web_App.ACTION).value)
num_entry <- List_Key.num(ENTRY, action)
entry <- model.entries.v.unapply(num_entry)
} yield {
val entry1 = entry.copy(topics = Val.ok(Utils.remove_at(num_topic, entry.topics.v)))
model.copy(entries = Val.ok(model.entries.v.updated(num_entry, entry1)))
}
def add_related(params: Params.Data): Option[Model.T] =
for {
model <- parse_create(params)
num_entry <- List_Key.num(ENTRY, params.get(Web_App.ACTION).value)
entry <- model.entries.v.unapply(num_entry)
} yield {
val entry1 =
entry.related_kind match {
case None =>
entry.copy(related_input =
entry.related_input.with_err("Select reference kind first"))
case Some(kind) =>
val reference = validate_related(kind, entry.related_input.v, entry.related)
val related_input = if (reference.is_empty) entry.related_input.v else ""
entry.copy(
related = entry.related ++ reference.opt,
related_input = Val.ok(related_input).perhaps_err(reference))
}
model.update_entry(num_entry, entry1)
}
def remove_related(params: Params.Data): Option[Model.T] =
for {
model <- parse_create(params)
(action, num_related) <- List_Key.split(RELATED, params.get(Web_App.ACTION).value)
num_entry <- List_Key.num(ENTRY, action)
entry <- model.entries.v.unapply(num_entry)
} yield {
val entry1 = entry.copy(related = Utils.remove_at(num_related, entry.related))
model.copy(entries = Val.ok(model.entries.v.updated(num_entry, entry1)))
}
def add_new_author(params: Params.Data): Option[Model.T] = parse_create(params).map { model =>
val name = model.new_author_input.trim
if (name.isEmpty)
model.copy(new_authors = model.new_authors.with_err("Name must not be empty"))
else {
def as_ascii(str: String) = {
var res: String = str
List("ö" -> "oe", "ü" -> "ue", "ä" -> "ae", "ß" -> "ss").foreach {
case (c, rep) => res = res.replace(c, rep)
}
Normalizer.normalize(res, Normalizer.Form.NFD).replaceAll("[^\\x00-\\x7F]", "")
}
def make_author_id(name: String): String = {
val normalized = as_ascii(name)
val Suffix = """^.*?([a-zA-Z]*)$""".r
val suffix = normalized match {
case Suffix(suffix) => suffix
case _ => ""
}
val Prefix = """^([a-zA-Z]*).*$""".r
val prefix = normalized.stripSuffix(suffix) match {
case Prefix(prefix) => prefix
case _ => ""
}
val updated_authors = model.updated_authors(authors)
var ident = suffix.toLowerCase
for {
c <- prefix.toLowerCase
if updated_authors.contains(ident)
} ident += c.toString
Utils.make_unique(ident, updated_authors.keySet)
}
val id = make_author_id(name)
val author = validate_new_author(id, model.new_author_input, model.new_author_orcid,
model.updated_authors(authors))
val new_author_input = if (author.is_empty) model.new_author_input else ""
val new_author_orcid = if (author.is_empty) model.new_author_orcid else ""
model.copy(
new_author_input = new_author_input,
new_author_orcid = new_author_orcid,
new_authors = Val.ok(model.new_authors.v ++ author.opt).perhaps_err(author))
}
}
def remove_new_author(params: Params.Data): Option[Model.T] =
for {
model <- parse_create(params)
num_author <- List_Key.num(AUTHOR, params.get(Web_App.ACTION).value)
author <- model.new_authors.v.unapply(num_author)
if !model.used_authors.contains(author.id)
} yield model.copy(new_authors =
Val.ok(Utils.remove_at(num_author, model.new_authors.v)))
def add_new_affil(params: Params.Data): Option[Model.T] =
parse_create(params).map { model =>
model.new_affils_author match {
case Some(author) =>
val address = model.new_affils_input.trim
if (address.isEmpty)
model.copy(new_affils = model.new_affils.with_err("Must not be empty"))
else {
val id =
if (address.contains("@"))
Utils.make_unique(author.id + "_email", author.emails.map(_.id).toSet)
else
Utils.make_unique(author.id + "_homepage", author.homepages.map(_.id).toSet)
val affil = validate_new_affil(id, address, author)
val new_affils_input = if (affil.is_empty) model.new_affils_input else ""
model.copy(
new_affils_input = new_affils_input,
new_affils = Val.ok(model.new_affils.v ++ affil.opt).perhaps_err(affil))
}
case None => model.copy(new_affils = model.new_affils.with_err("Select author first"))
}
}
def remove_new_affil(params: Params.Data): Option[Model.T] =
for {
model <- parse_create(params)
num_affil <- List_Key.num(AFFILIATION, params.get(Web_App.ACTION).value)
affil <- model.new_affils.v.unapply(num_affil)
if !model.used_affils.contains(affil)
} yield model.copy(new_affils = Val.ok(Utils.remove_at(num_affil, model.new_affils.v)))
def upload(params: Params.Data): Option[Model.T] = parse_create(params).map { create =>
var ok = true
def validate[A](validator: A => Val[A], value: A): Val[A] = {
val res = validator(value)
if (res.err.nonEmpty) ok = false
res
}
def title(title: String): Val[String] =
if (title.isBlank) Val.err(title, "Title must not be blank")
else if (title.trim != title) Val.err(title, "Title must not contain extra spaces")
else Val.ok(title)
def name(name: String): Val[String] =
if (name.isBlank) Val.err(name, "Name must not be blank")
else if (!"[a-zA-Z0-9_-]+".r.matches(name)) Val.err(name,
"Invalid character in name")
else mode match {
case Mode.EDIT =>
if (Server.this.entries.contains(name)) Val.ok(name)
else Val.err(name, "Entry does not exist")
case Mode.SUBMISSION =>
if (Server.this.entries.contains(name)) Val.err(name, "Entry already exists")
else Val.ok(name)
}
def entries(entries: List[Model.Create_Entry]): Val[List[Model.Create_Entry]] =
if (entries.isEmpty) Val.err(entries, "Must contain at least one entry")
else if (Library.duplicates(entries.map(_.name)).nonEmpty)
Val.err(entries, "Entries must have different names")
else Val.ok(entries)
def new_authors(authors: List[Author]): Val[List[Author]] =
if (!authors.forall(author => create.used_authors.contains(author.id)))
Val.err(authors, "Unused authors")
else Val.ok(authors)
def new_affils(affils: List[Affiliation]): Val[List[Affiliation]] =
if (!affils.forall(affil => create.used_affils.contains(affil)))
Val.err(affils, "Unused affils")
else Val.ok(affils)
def entry_authors(authors: List[Affiliation]): Val[List[Affiliation]] =
if (authors.isEmpty) Val.err(authors, "Must contain at least one author")
else if (!Utils.is_distinct(authors)) Val.err(authors, "Duplicate affiliations")
else Val.ok(authors)
def notifies(notifies: List[Email]): Val[List[Email]] =
if (notifies.isEmpty) Val.err(notifies, "Must contain at least one maintainer")
else if (!Utils.is_distinct(notifies)) Val.err(notifies, "Duplicate emails")
else Val.ok(notifies)
def topics(topics: List[Topic]): Val[List[Topic]] =
if (topics.isEmpty) Val.err(topics, "Must contain at least one topic") else Val.ok(topics)
def `abstract`(txt: String): Val[String] =
if (txt.isBlank) Val.err(txt, "Entry must contain an abstract")
else if (List("\\cite", "\\emph", "\\texttt").exists(txt.contains(_)))
Val.err(txt, "LaTeX not allowed, use MathJax for math symbols")
else Val.ok(txt)
val validated = create.copy(
entries = validate(
entries, create.entries.v.map(entry => entry.copy(
name = validate(name, entry.name.v),
title = validate(title, entry.title.v),
affils = validate(entry_authors, entry.affils.v),
notifies = validate(notifies, entry.notifies.v),
topics = validate(topics, entry.topics.v),
`abstract` = validate(`abstract`, entry.`abstract`.v)
))),
new_authors = validate(new_authors, create.new_authors.v),
new_affils = validate(new_affils, create.new_affils.v))
if (ok) {
val (updated_authors, entries) = create.create(authors)
Model.Upload(Model.Metadata(updated_authors, entries), params.get(MESSAGE).value, "")
} else validated
}
def create(params: Params.Data): Option[Model.T] = {
upload(params) match {
case Some(upload: Model.Upload) =>
mode match {
case Mode.EDIT =>
handler.create(Date.now(), upload.meta, upload.message, Bytes.empty, "")
Some(Model.Created(upload.meta.entries.head.name))
case Mode.SUBMISSION =>
val archive = Bytes.decode_base64(params.get(ARCHIVE).get(FILE).value)
val file_name = params.get(ARCHIVE).value
if (archive.is_empty || file_name.isEmpty) {
Some(upload.copy(error = "Select a file"))
} else if (!file_name.endsWith(".zip") && !file_name.endsWith(".tar.gz")) {
Some(upload.copy(error = "Only .zip and .tar.gz archives allowed"))
} else {
val ext = if (file_name.endsWith(".zip")) ".zip" else ".tar.gz"
val id = handler.create(Date.now(), upload.meta, upload.message, archive, ext)
Some(Model.Created(id))
}
}
case _ => None
}
}
def empty_submission: Option[Model.T] =
Some(Model.Create(entries =
Val.ok(List(Model.Create_Entry(license = licenses.head._2)))))
def get_submission(props: Properties.T): Option[Model.Submission] =
Properties.get(props, ID).flatMap(handler.get(_, topics, licenses))
def resubmit(params: Params.Data): Option[Model.T] =
handler.get(params.get(ACTION).value, topics, licenses).map(submission =>
Model.Upload(submission.meta, submission.message, ""))
def submit(params: Params.Data): Option[Model.T] =
handler.get(params.get(ACTION).value, topics, licenses).flatMap { submission =>
if (submission.status.nonEmpty) None
else {
handler.submit(submission.id)
Some(submission.copy(status = Some(Model.Status.Submitted)))
}
}
def abort_build(params: Params.Data): Option[Model.T] =
handler.get(params.get(ACTION).value, topics, licenses).flatMap { submission =>
if (submission.build != Model.Build.Running) None
else {
handler.abort_build(submission.id)
Some(submission.copy(build = Model.Build.Aborted))
}
}
def set_status(params: Params.Data): Option[Model.T] = {
for {
list <- parse_submission_list(params)
num_entry <- List_Key.num(ENTRY, params.get(ACTION).value)
changed <- list.submissions.unapply(num_entry)
} yield {
if (changed.status == Model.Status.Added && !devel) {
progress.echo_if(verbose, "Updating server data...")
val id_before = repo.id()
repo.pull()
repo.update()
val id_after = repo.id()
if (id_before != id_after) {
load()
progress.echo("Updated repo from " + id_before + " to " + id_after)
}
}
handler.set_status(changed.id, changed.status)
list
}
}
def submission_list: Option[Model.T] = Some(handler.list())
def download(props: Properties.T): Option[Path] =
for {
id <- Properties.get(props, ID)
patch <- handler.get_patch(id)
} yield patch
def download_archive(props: Properties.T): Option[Path] =
for {
id <- Properties.get(props, ID)
archive <- handler.get_archive(id)
} yield archive
def style_sheet: Option[Path] =
Some(afp_structure.base_dir + Path.make(List("tools", "main.css")))
val error_model = Model.Invalid
val endpoints = List(
Get(SUBMIT, "empty submission form", _ => empty_submission),
Get(SUBMISSION, "get submission", get_submission),
Get(SUBMISSIONS, "list submissions", _ => submission_list),
Get_File(API_SUBMISSION_DOWNLOAD, "download patch", download),
Get_File(API_SUBMISSION_DOWNLOAD_ZIP, "download archive", download_archive),
Get_File(API_SUBMISSION_DOWNLOAD_TGZ, "download archive", download_archive),
Get_File(API_CSS, "download css", _ => style_sheet),
Post(API_RESUBMIT, "get form for resubmit", resubmit),
Post(API_SUBMIT, "submit to editors", submit),
Post(API_BUILD_ABORT, "abort the build", abort_build),
Post(API_SUBMISSION, "get submission form", parse_create),
Post(API_SUBMISSION_AUTHORS_ADD, "add author", add_new_author),
Post(API_SUBMISSION_AUTHORS_REMOVE, "remove author", remove_new_author),
Post(API_SUBMISSION_AFFILIATIONS_ADD, "add affil", add_new_affil),
Post(API_SUBMISSION_AFFILIATIONS_REMOVE, "remove affil", remove_new_affil),
Post(API_SUBMISSION_ENTRIES_ADD, "add entry", add_entry),
Post(API_SUBMISSION_ENTRIES_REMOVE, "remove entry", remove_entry),
Post(API_SUBMISSION_ENTRY_AUTHORS_ADD, "add entry author", add_author),
Post(API_SUBMISSION_ENTRY_AUTHORS_REMOVE, "remove entry author", remove_author),
Post(API_SUBMISSION_ENTRY_NOTIFIES_ADD, "add notify", add_notify),
Post(API_SUBMISSION_ENTRY_NOTIFIES_REMOVE, "remove notify", remove_notify),
Post(API_SUBMISSION_ENTRY_TOPICS_ADD, "add topic", add_topic),
Post(API_SUBMISSION_ENTRY_TOPICS_REMOVE, "remove topic", remove_topic),
Post(API_SUBMISSION_ENTRY_RELATED_ADD, "add related", add_related),
Post(API_SUBMISSION_ENTRY_RELATED_REMOVE, "remove related", remove_related),
Post(API_SUBMISSION_UPLOAD, "upload archive", upload),
Post(API_SUBMISSION_CREATE, "create submission", create),
Post(API_SUBMISSION_STATUS, "set submission status", set_status))
val head =
List(
XML.Elem(Markup("script", List(
"type" -> "text/javascript",
"id" -> "MathJax-script",
"async" -> "async",
"src" -> "https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-svg.js")), text("\n")),
script(
"MathJax={tex:{inlineMath:[['$','$'],['\\\\(','\\\\)']]},processEscapes:true,svg:{fontCache:'global'}}"),
style_file(api.api_url(API_CSS)))
}
/* Isabelle tool wrapper */
val isabelle_tool = Isabelle_Tool("afp_submit", "start afp submission server",
Scala_Project.here,
{ args =>
var backend_path = Path.current
var frontend_url = Url("http://localhost:8080")
var devel = false
var verbose = false
var port = 8080
var dir: Option[Path] = None
val getopts = Getopts("""
Usage: isabelle afp_submit [OPTIONS]
Options are:
-a PATH backend path (if endpoint is not server root)
-b URL application frontend url. Default: """ + frontend_url + """"
-d devel mode (serves frontend and skips automatic AFP repository updates)
-p PORT server port. Default: """ + port + """
-v verbose
-D DIR submission directory
Start afp submission server. Server is in "edit" mode
unless directory to store submissions in is specified.
""",
"a:" -> (arg => backend_path = Path.explode(arg)),
"b:" -> (arg => frontend_url = Url(arg)),
"d" -> (_ => devel = true),
"p:" -> (arg => port = Value.Int.parse(arg)),
"v" -> (_ => verbose = true),
"D:" -> (arg => dir = Some(Path.explode(arg))))
getopts(args)
val afp_structure = AFP_Structure()
val progress = new Console_Progress(verbose = verbose)
val (handler, mode) = dir match {
case Some(dir) => (Handler.Adapter(dir, afp_structure), Mode.SUBMISSION)
case None => (Handler.Edit(afp_structure), Mode.EDIT)
}
val api = new API(frontend_url, backend_path, devel = devel)
val server = new Server(api = api, afp_structure = afp_structure, mode = mode,
handler = handler, devel = devel, verbose = verbose, progress = progress, port = port)
server.run()
})
}
diff --git a/tools/utils.scala b/tools/utils.scala
--- a/tools/utils.scala
+++ b/tools/utils.scala
@@ -1,58 +1,58 @@
/* Author: Fabian Huch, TU Muenchen
Utilities.
*/
package afp
import isabelle.*
-import java.io.{BufferedReader, InputStreamReader, IOException}
+import java.io.IOException
import scala.collection.immutable.ListMap
object Utils {
val TIMEOUT = 30*1000
def group_sorted[A, K](l: List[A], f: A => K): ListMap[K, List[A]] =
l.foldLeft(ListMap.empty[K, List[A]]) {
case (m, a) =>
m.updatedWith(f(a)) {
case Some(as) => Some(as :+ a)
case None => Some(List(a))
}
}
def grouped_sorted[A, K](l: List[A], f: A => K): ListMap[K, A] =
group_sorted(l, f).map {
case (k, v :: Nil) => k -> v
case (k, vs) => error("Not distinct for " + quote(k.toString) + ": " + commas_quote(vs.map(_.toString)))
}
def the_entry[K, V](m: Map[K, V], k: K): V = m.getOrElse(k, error("Expected key " + quote(k.toString)))
def fetch_text(url: Url, params: Map[String, String]): String =
try {
val conn = url.open_connection()
conn.setConnectTimeout(TIMEOUT)
conn.setReadTimeout(TIMEOUT)
params.foreach { case (param, value) => conn.setRequestProperty(param, value) }
File.read_stream(conn.getInputStream)
} catch {
case _: IOException => error("Could not read from " + quote(url.toString))
}
def remove_at[A](i: Int, l: List[A]): List[A] = l.take(i) ++ l.drop(i + 1)
def make_unique(prefix: String, elems: Set[String]): String = {
if (!elems.contains(prefix)) prefix
else {
var num = 1
while (elems.contains(prefix + num)) { num += 1 }
prefix + num
}
}
def is_distinct[A](it: List[A]): Boolean = it.size == it.distinct.size
}
\ No newline at end of file
diff --git a/tools/web_app.scala b/tools/web_app.scala
--- a/tools/web_app.scala
+++ b/tools/web_app.scala
@@ -1,498 +1,497 @@
/* Author: Fabian Huch, TU Muenchen
Technical layer for web apps using server-side rendering with HTML forms.
*/
package afp
import isabelle.*
-
import scala.annotation.tailrec
object Web_App {
val FILE = "file"
val ACTION = "action"
/* form html elements */
object More_HTML {
import HTML._
def css(s: String): Attribute = new Attribute("style", s)
def name(n: String): Attribute = new Attribute("name", n)
def value(v: String): Attribute = new Attribute("value", v)
def placeholder(p: String): Attribute = new Attribute("placeholder", p)
val fieldset = new Operator("fieldset")
val button = new Operator("button")
def legend(txt: String): XML.Elem = XML.Elem(Markup("legend", Nil), text(txt))
def input(typ: String): XML.Elem = XML.Elem(Markup("input", List("type" -> typ)), Nil)
def hidden(k: String, v: String): XML.Elem = id(k)(name(k)(value(v)(input("hidden"))))
def textfield(i: String, p: String, v: String): XML.Elem =
id(i)(name(i)(value(v)(placeholder(p)(input("text")))))
def browse(i: String, accept: List[String]): XML.Elem =
id(i)(name(i)(input("file"))) + ("accept" -> accept.mkString(","))
def label(`for`: String, txt: String): XML.Elem =
XML.Elem(Markup("label", List("for" -> `for`)), text(txt))
def fieldlabel(for_elem: String, txt: String): XML.Elem = label(for_elem, " " + txt + ": ")
def explanation(for_elem: String, txt: String): XML.Elem =
par(List(emph(List(label(for_elem, txt)))))
def option(k: String, v: String): XML.Elem =
XML.Elem(Markup("option", List("value" -> k)), text(v))
def optgroup(txt: String, opts: XML.Body): XML.Elem =
XML.Elem(Markup("optgroup", List("label" -> txt)), opts)
def select(i: String, opts: XML.Body): XML.Elem =
XML.Elem(Markup("select", List("id" -> i, "name" -> i)), opts)
def textarea(i: String, v: String): XML.Elem =
XML.Elem(Markup("textarea", List("id" -> i, "name" -> i, "value" -> v)), text(v + "\n"))
def radio(i: String, v: String, values: List[(String, String)]): XML.Elem = {
def to_option(k: String): XML.Elem = {
val elem = id(i + k)(name(i)(value(k)(input("radio"))))
if (v == k) elem + ("checked" -> "checked") else elem
}
span(values.map { case (k, v) => span(List(label(i + k, v), to_option(k))) })
}
def selection(i: String, selected: Option[String], opts: XML.Body): XML.Elem = {
def sel(elem: XML.Tree): XML.Tree = {
selected match {
case Some(value) =>
val Value = new Properties.String("value")
elem match {
case XML.Elem(Markup("optgroup", props), body) =>
XML.Elem(Markup("optgroup", props), body.map(sel))
case e@XML.Elem(Markup("option", Value(v)), _) if v == value =>
e + ("selected" -> "selected")
case e => e
}
case None => elem
}
}
def is_empty_group(elem: XML.Tree): Boolean = elem match {
case XML.Elem(Markup("optgroup", _), body) if body.isEmpty => true
case _ => false
}
val default = if (selected.isEmpty) List(option("", "") + ("hidden" -> "hidden")) else Nil
select(i, default ::: opts.filterNot(is_empty_group).map(sel))
}
def api_button(call: String, label: String): XML.Elem =
button(text(label)) + ("formaction" -> call) + ("type" -> "submit")
def action_button(call: String, label: String, action: String): XML.Elem =
name(ACTION)(value(action)(api_button(call, label)))
def submit_form(endpoint: String, body: XML.Body): XML.Elem = {
val default_button = css("display: none")(input("submit") + ("formaction" -> endpoint))
val attrs =
List("method" -> "post", "target" -> "iframe", "enctype" -> "multipart/form-data")
XML.Elem(Markup("form", attrs), default_button :: body)
}
}
/* request parameters */
object Params {
type Key = String
val empty: Key = ""
object Nest_Key {
def apply(k: Key, field: String): Key =
if (k == empty) field else k + "_" + field
def unapply(k: Key): Option[(Key, String)] =
k.split('_').filterNot(_.isEmpty).toList.reverse match {
case k :: ks => Some(ks.reverse.mkString("_"), k)
case _ => None
}
}
object List_Key {
def apply(k: Key, field: String, i: Int): Key =
Nest_Key(k, field + "_" + i.toString)
def unapply(k: Key): Option[(Key, (String, Int))] =
k.split('_').filterNot(_.isEmpty).toList.reverse match {
case Value.Int(i) :: k :: ks => Some(ks.reverse.mkString("_"), (k, i))
case _ => None
}
def num(field: String, k: Key): Option[Int] = k match {
case List_Key(_, (f, i)) if f == field => Some(i)
case _ => None
}
def split(field: String, k: Key): Option[(Key, Int)] = k match {
case List_Key(key, (f, i)) if f == field => Some(key, i)
case _ => None
}
}
/* structured data */
class Data private[Params](
v: Option[String] = None,
elem: Map[String, Data] = Map.empty,
elems: Map[String, List[Data]] = Map.empty
) {
def is_empty: Boolean = v.isEmpty && elem.isEmpty && elems.isEmpty
override def toString: String = {
val parts =
v.map(v => if (v.length <= 100) quote(v) else quote(v.take(100) + "...")).toList ++
elem.toList.map { case (k, v) => k + " -> " + v.toString } ++
elems.toList.map { case (k, v) => k + " -> (" + v.mkString(",") + ")" }
"{" + parts.mkString(", ") + "}"
}
def value: String = v.getOrElse("")
def get(field: String): Data = elem.getOrElse(field, new Data())
def list(field: String): List[Data] = elems.getOrElse(field, Nil)
}
object Data {
def from_multipart(parts: List[Multi_Part.Data]): Data = {
sealed trait E
case class Value(rep: String) extends E
case class Index(i: Int, to: E) extends E
case class Nest(field: String, to: E) extends E
def group_map[A, B, C](v: List[(C, A)], agg: List[A] => B): Map[C, B] =
v.groupBy(_._1).view.mapValues(_.map(_._2)).mapValues(agg).toMap
def to_list(l: List[(Int, E)]): List[Data] = {
val t: List[(Int, Data)] = group_map(l, parse).toList
t.sortBy(_._1).map(_._2)
}
def parse(e: List[E]): Data = {
val value = e.collectFirst { case Value(rep) => rep }
val nest_by_key = e.collect {
case Nest(field, v: Value) => field -> v
case Nest(field, v: Nest) => field -> v
}
val elem = group_map(nest_by_key, parse)
val list_by_key = e.collect {
case Nest(field, Index(i, to)) => field -> (i -> to)
}
val elems = group_map(list_by_key, to_list)
new Data(value, elem, elems)
}
@tailrec
def expand(key: Key, to: E): E =
key match {
case List_Key(key, (field, i)) => expand(key, Nest(field, Index(i, to)))
case Nest_Key(key, field) => expand(key, Nest(field, to))
case _ => to
}
val params =
parts.flatMap {
case Multi_Part.Param(name, value) => List(name -> value)
case Multi_Part.File(name, file_name, content) =>
List(name -> file_name, Nest_Key(name, Web_App.FILE) -> content.encode_base64)
}
parse(params.map { case (k, v) => expand(k, Value(v)) })
}
}
}
/* form http handling */
object Multi_Part {
abstract class Data(name: String)
case class Param(name: String, value: String) extends Data(name)
case class File(name: String, file_name: String, content: Bytes) extends Data(name)
def parse(body: Bytes): List[Data] = {
/* Seq for text with embedded bytes */
case class Seq(text: String, bytes: Bytes) {
def split_one(sep: String): Option[(Seq, Seq)] = {
val text_i = text.indexOf(sep)
if (text_i >= 0 && sep.nonEmpty) {
val (before_text, at_text) = text.splitAt(text_i)
val after_text = at_text.substring(sep.length)
// text might be shorter than bytes because of misinterpreted characters
var found = false
var bytes_i = 0
while (!found && bytes_i < bytes.length) {
var sep_ok = true
var sep_i = 0
while (sep_ok && sep_i < sep.length) {
if (bytes.charAt(bytes_i + sep_i) == sep.charAt(sep_i)) {
sep_i += 1
} else {
bytes_i += 1
sep_ok = false
}
}
if (sep_ok) found = true
}
val before_bytes = bytes.subSequence(0, bytes_i)
val after_bytes = bytes.subSequence(bytes_i + sep.length, bytes.length)
Some(Seq(before_text, before_bytes), Seq(after_text, after_bytes))
} else None
}
}
val s = Seq(body.text, body)
def perhaps_unprefix(pfx: String, s: Seq): Seq =
Library.try_unprefix(pfx, s.text) match {
case Some(text) => Seq(text, s.bytes.subSequence(pfx.length, s.bytes.length))
case None => s
}
val Separator = """--(.*)""".r
s.split_one(HTTP.NEWLINE) match {
case Some(Seq(Separator(sep), _), rest) =>
val Param = """Content-Disposition: form-data; name="([^"]+)"""".r
val File = """Content-Disposition: form-data; name="([^"]+)"; filename="([^"]+)"""".r
def parts(body: Seq): Option[List[Data]] =
for {
(first_line, more) <- body.split_one(HTTP.NEWLINE)
more1 = perhaps_unprefix(HTTP.NEWLINE, more)
(value, rest) <- more1.split_one(HTTP.NEWLINE + "--" + sep)
rest1 = perhaps_unprefix(HTTP.NEWLINE, rest)
} yield first_line.text match {
case Param(name) =>
Multi_Part.Param(name, Line.normalize(value.text)) :: parts(rest1).getOrElse(Nil)
case File(name, file_name) =>
value.split_one(HTTP.NEWLINE + HTTP.NEWLINE) match {
case Some(_, content) =>
Multi_Part.File(name, file_name, content.bytes) :: parts(rest1).getOrElse(Nil)
case _ => parts(rest1).getOrElse(Nil)
}
case _ => Nil
}
parts(rest).getOrElse(Nil)
case _ => Nil
}
}
}
/* API with backend base path, and application url (e.g. for frontend links). */
class API(val app: Url, val base_path: Path, val devel: Boolean = false) {
def url(path: Path, params: Properties.T = Nil): String = {
def param(p: Properties.Entry): String = Url.encode(p._1) + "=" + Url.encode(p._2)
if (params.isEmpty) path.implode else path.implode + "?" + params.map(param).mkString("&")
}
def api_path(path: Path, external: Boolean = true): Path =
(if (devel) Path.explode("backend") else Path.current) +
(if (external) base_path else Path.current) + path
def api_url(path: Path, params: Properties.T = Nil, external: Boolean = true): String =
"/" + url(api_path(path, external = external), params)
def app_url(path: Path, params: Properties.T = Nil): String =
app.toString + "/" + url(path, params)
}
abstract class Server[A](
api: API,
port: Int = 0,
verbose: Boolean = false,
progress: Progress = new Progress()
) {
def render(model: A): XML.Body
val error_model: A
val endpoints: List[Endpoint]
val head: XML.Body
def output_document(content: XML.Body, post_height: Boolean = true): String = {
val attrs =
if (post_height) List("onLoad" -> "parent.postMessage(document.body.scrollHeight, '*')")
else Nil
cat_lines(
List(
HTML.header,
HTML.output(XML.elem("head", HTML.head_meta :: head), hidden = true, structural = true),
HTML.output(XML.Elem(Markup("body", attrs), content), hidden = true, structural = true),
HTML.footer))
}
class UI(path: Path) extends HTTP.Service(path.implode, "GET") {
def apply(request: HTTP.Request): Option[HTTP.Response] = {
progress.echo_if(verbose, "GET ui")
val on_load = """
(function() {
window.addEventListener('message', (event) => {
if (Number.isInteger(event.data)) {
this.style.height=event.data + 32 + 'px'
}
})
}).call(this)"""
val set_src = """
const base = '""" + api.app.toString.replace("/", "\\/") + """'
document.getElementById('iframe').src = base + '""" + api.api_url(path).replace("/", "\\/") + """' + window.location.search"""
Some(HTTP.Response.html(output_document(
List(
XML.Elem(
Markup(
"iframe",
List(
"id" -> "iframe",
"name" -> "iframe",
"style" -> "border-style: none; width: 100%",
"onload" -> on_load)),
HTML.text("content")),
HTML.script(set_src)),
post_height = false)))
}
}
sealed abstract class Endpoint(path: Path, method: String = "GET")
extends HTTP.Service(api.api_path(path, external = false).implode, method) {
def reply(request: HTTP.Request): HTTP.Response
final def apply(request: HTTP.Request): Option[HTTP.Response] =
Exn.capture(reply(request)) match {
case Exn.Res(res) => Some(res)
case Exn.Exn(exn) =>
val id = UUID.random_string()
progress.echo_error_message("Internal error <" + id + ">: " + exn)
error("Internal server error. ID: " + id)
}
}
private def query_params(request: HTTP.Request): Properties.T = {
def decode(s: String): Option[Properties.Entry] =
s match {
case Properties.Eq(k, v) => Some(Url.decode(k) -> Url.decode(v))
case _ => None
}
Library.try_unprefix(request.query, request.uri_name).toList.flatMap(params =>
space_explode('&', params).flatMap(decode))
}
/* endpoint types */
class Get(val path: Path, description: String, get: Properties.T => Option[A])
extends Endpoint(path) {
def reply(request: HTTP.Request): HTTP.Response = {
progress.echo_if(verbose, "GET " + description)
val params = query_params(request)
progress.echo_if(verbose, "params: " + params.toString())
val model =
get(params) match {
case Some(model) => model
case None =>
progress.echo_if(verbose, "Parsing failed")
error_model
}
HTTP.Response.html(output_document(render(model)))
}
}
class Get_File(path: Path, description: String, download: Properties.T => Option[Path])
extends Endpoint(path) {
def reply(request: HTTP.Request): HTTP.Response = {
progress.echo_if(verbose, "DOWNLOAD " + description)
val params = query_params(request)
progress.echo_if(verbose, "params: " + params.toString())
download(params) match {
case Some(path) => HTTP.Response.content(HTTP.Content.read(path))
case None =>
progress.echo_if(verbose, "Fetching file path failed")
HTTP.Response.html(output_document(render(error_model)))
}
}
}
class Post(path: Path, description: String, post: Params.Data => Option[A])
extends Endpoint(path, method = "POST") {
def reply(request: HTTP.Request): HTTP.Response = {
progress.echo_if(verbose, "POST " + description)
val parts = Multi_Part.parse(request.input)
val params = Params.Data.from_multipart(parts)
progress.echo_if(verbose, "params: " + params.toString)
val model =
post(params) match {
case Some(model) => model
case None =>
progress.echo_if(verbose, "Parsing failed")
error_model
}
HTTP.Response.html(output_document(render(model)))
}
}
/* server */
private lazy val services =
endpoints ::: (if (api.devel) endpoints.collect { case g: Get => new UI(g.path) } else Nil)
private lazy val server = HTTP.server(port = port, name = "", services = services)
def run(): Unit = {
start()
@tailrec
def loop(): Unit = {
Thread.sleep(Long.MaxValue)
loop()
}
Isabelle_Thread.interrupt_handler(_ => server.stop()) { loop() }
}
def start(): Unit = {
server.start()
progress.echo("Server started on port " + server.http_server.getAddress.getPort)
}
def stop(): Unit = {
server.stop()
progress.echo("Server stopped")
}
}
}
\ No newline at end of file