--- a/etc/isabelle.css Sun May 14 13:55:51 2017 +0200
+++ b/etc/isabelle.css Sun May 14 22:07:16 2017 +0200
@@ -16,6 +16,16 @@
src: url('fonts/Vacuous.ttf') format('truetype');
}
+
+/* standard document markup */
+
+dt {
+ float: left;
+ clear: left;
+ padding-right: 0.5em;
+ font-weight: bold;
+}
+
body { background-color: #FFFFFF; }
.head { background-color: #FFFFFF; }
@@ -65,4 +75,3 @@
.comment { color: #CC0000; }
.improper { color: #FF5050; }
.bad { background-color: #FF6A6A; }
-
--- a/src/HOL/Analysis/Great_Picard.thy Sun May 14 13:55:51 2017 +0200
+++ b/src/HOL/Analysis/Great_Picard.thy Sun May 14 22:07:16 2017 +0200
@@ -614,7 +614,7 @@
qed
-subsection\<open>The Arzelà–Ascoli theorem\<close>
+subsection\<open>The Arzelà--Ascoli theorem\<close>
lemma subsequence_diagonalization_lemma:
fixes P :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> bool"
--- a/src/Pure/Admin/build_release.scala Sun May 14 13:55:51 2017 +0200
+++ b/src/Pure/Admin/build_release.scala Sun May 14 22:07:16 2017 +0200
@@ -123,21 +123,18 @@
info.all_bundles.find(name => (release_info.dist_dir + Path.explode(name)).is_file)
} yield (bundle, info)
- Isabelle_System.mkdirs(dir)
-
val afp_link =
HTML.link("https://bitbucket.org/isa-afp/afp-devel/commits/" + afp_rev,
HTML.text("AFP/" + afp_rev))
- File.write(dir + Path.explode("index.html"),
- HTML.output_document(
- List(HTML.title(release_info.name)),
- List(
- HTML.chapter(release_info.name + " (" + release_id + ")"),
- HTML.itemize(
- website_platform_bundles.map({ case (bundle, info) =>
- List(HTML.link(bundle, HTML.text(info.platform_description))) }))) :::
- (if (afp_rev == "") Nil else List(HTML.par(HTML.text("See also ") ::: List(afp_link))))))
+ HTML.write_document(dir, "index.html",
+ List(HTML.title(release_info.name)),
+ List(
+ HTML.chapter(release_info.name + " (" + release_id + ")"),
+ HTML.itemize(
+ website_platform_bundles.map({ case (bundle, info) =>
+ List(HTML.link(bundle, HTML.text(info.platform_description))) }))) :::
+ (if (afp_rev == "") Nil else List(HTML.par(HTML.text("See also ") ::: List(afp_link)))))
for ((bundle, _) <- website_platform_bundles)
File.copy(release_info.dist_dir + Path.explode(bundle), dir)
--- a/src/Pure/Admin/build_status.scala Sun May 14 13:55:51 2017 +0200
+++ b/src/Pure/Admin/build_status.scala Sun May 14 22:07:16 2017 +0200
@@ -203,18 +203,16 @@
def clean_name(name: String): String =
name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString)
- Isabelle_System.mkdirs(target_dir)
- File.write(target_dir + Path.basic("index.html"),
- HTML.output_document(
- List(HTML.title("Isabelle build status")),
- List(HTML.chapter("Isabelle build status"),
- HTML.par(
- List(HTML.itemize(
- List(HTML.bold(HTML.text("status date: ")) :: HTML.text(data.date.toString))))),
- HTML.par(
- List(HTML.itemize(data.entries.map({ case data_entry =>
- List(HTML.link(clean_name(data_entry.name) + "/index.html",
- HTML.text(data_entry.name))) })))))))
+ HTML.write_document(target_dir, "index.html",
+ List(HTML.title("Isabelle build status")),
+ List(HTML.chapter("Isabelle build status"),
+ HTML.par(
+ List(HTML.description(
+ List(HTML.text("status date:") -> HTML.text(data.date.toString))))),
+ HTML.par(
+ List(HTML.itemize(data.entries.map({ case data_entry =>
+ List(HTML.link(clean_name(data_entry.name) + "/index.html",
+ HTML.text(data_entry.name))) }))))))
for (data_entry <- data.entries) {
val data_name = data_entry.name
@@ -308,36 +306,35 @@
}
}, data_entry.sessions).toMap
- File.write(dir + Path.basic("index.html"),
- HTML.output_document(
- List(HTML.title("Isabelle build status for " + data_name)),
- HTML.chapter("Isabelle build status for " + data_name) ::
- HTML.par(
- List(HTML.itemize(
- List(
- HTML.bold(HTML.text("status date: ")) :: HTML.text(data.date.toString),
- HTML.bold(HTML.text("build host: ")) :: HTML.text(commas(data_entry.hosts)))))) ::
- HTML.par(
- List(HTML.itemize(
- data_entry.sessions.map(session =>
- HTML.link("#session_" + session.name, HTML.text(session.name)) ::
- HTML.text(" (" + session.timing.message_resources + ")"))))) ::
- data_entry.sessions.flatMap(session =>
+ HTML.write_document(dir, "index.html",
+ List(HTML.title("Isabelle build status for " + data_name)),
+ HTML.chapter("Isabelle build status for " + data_name) ::
+ HTML.par(
+ List(HTML.description(
List(
- HTML.section(session.name) + HTML.id("session_" + session.name),
- HTML.par(
- HTML.itemize(List(
- HTML.bold(HTML.text("timing: ")) :: HTML.text(session.timing.message_resources),
- HTML.bold(HTML.text("ML timing: ")) ::
- HTML.text(session.ml_timing.message_resources)) :::
- proper_string(session.isabelle_version).map(s =>
- HTML.bold(HTML.text("Isabelle version: ")) :: HTML.text(s)).toList :::
- proper_string(session.afp_version).map(s =>
- HTML.bold(HTML.text("AFP version: ")) :: HTML.text(s)).toList) ::
- session_plots.getOrElse(session.name, Nil).map(plot_name =>
- HTML.image(plot_name) +
- HTML.width(image_width / 2) +
- HTML.height(image_height / 2)))))))
+ HTML.text("status date:") -> HTML.text(data.date.toString),
+ HTML.text("build host:") -> HTML.text(commas(data_entry.hosts)))))) ::
+ HTML.par(
+ List(HTML.itemize(
+ data_entry.sessions.map(session =>
+ HTML.link("#session_" + session.name, HTML.text(session.name)) ::
+ HTML.text(" (" + session.timing.message_resources + ")"))))) ::
+ data_entry.sessions.flatMap(session =>
+ List(
+ HTML.section(session.name) + HTML.id("session_" + session.name),
+ HTML.par(
+ HTML.description(
+ List(
+ HTML.text("timing:") -> HTML.text(session.timing.message_resources),
+ HTML.text("ML timing:") -> HTML.text(session.ml_timing.message_resources)) :::
+ proper_string(session.isabelle_version).map(s =>
+ HTML.text("Isabelle version:") -> HTML.text(s)).toList :::
+ proper_string(session.afp_version).map(s =>
+ HTML.text("AFP version:") -> HTML.text(s)).toList) ::
+ session_plots.getOrElse(session.name, Nil).map(plot_name =>
+ HTML.image(plot_name) +
+ HTML.width(image_width / 2) +
+ HTML.height(image_height / 2))))))
}
}
--- a/src/Pure/Admin/check_sources.scala Sun May 14 13:55:51 2017 +0200
+++ b/src/Pure/Admin/check_sources.scala Sun May 14 22:07:16 2017 +0200
@@ -49,7 +49,7 @@
Output.writeln("Checking " + root + " ...")
val hg = Mercurial.repository(root)
for {
- file <- hg.manifest()
+ file <- hg.known_files()
if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT")
} check_file(root + Path.explode(file))
}
@@ -63,7 +63,7 @@
val getopts = Getopts("""
Usage: isabelle check_sources [ROOT_DIRS...]
- Check .thy, .ML, ROOT files from manifest of Mercurial ROOT_DIRS.
+ Check .thy, .ML, ROOT against known files of Mercurial ROOT_DIRS.
""")
val specs = getopts(args)
--- a/src/Pure/Admin/isabelle_cronjob.scala Sun May 14 13:55:51 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Sun May 14 22:07:16 2017 +0200
@@ -105,8 +105,9 @@
user: String = "",
port: Int = 0,
shared_home: Boolean = true,
+ historic: Boolean = false,
history: Int = 0,
- historic: Boolean = false,
+ history_base: String = "build_history_base",
options: String = "",
args: String = "",
detect: SQL.Source = "")
@@ -119,14 +120,24 @@
def profile: Build_Status.Profile =
Build_Status.Profile(description, history, sql)
- def pick(options: Options, rev: String = ""): Option[String] =
+ def history_base_filter(hg: Mercurial.Repository): Set[String] =
+ {
+ val rev0 = hg.id(history_base)
+ val graph = hg.graph()
+ (rev0 :: graph.all_succs(List(rev0))).toSet
+ }
+
+ def pick(options: Options, rev: String = "", filter: String => Boolean = (_: String) => true)
+ : Option[String] =
{
val store = Build_Log.store(options)
using(store.open_database())(db =>
{
def pick_days(days: Int): Option[String] =
{
- val items = recent_items(db, days = days, rev = rev, sql = sql)
+ val items =
+ recent_items(db, days = days, rev = rev, sql = sql).
+ filter(item => filter(item.isabelle_version))
def runs = unknown_runs(items)
val known_rev =
@@ -145,8 +156,8 @@
}
pick_days(options.int("build_log_history") max history) orElse
- pick_days(100) orElse
- pick_days(1000)
+ pick_days(200) orElse
+ pick_days(2000)
})
}
}
@@ -164,13 +175,14 @@
val remote_builds: List[List[Remote_Build]] =
{
List(
- List(Remote_Build("Poly/ML 5.7 Linux", "lxbroy8", history = 90, historic = true,
+ List(Remote_Build("Poly/ML 5.7 Linux", "lxbroy8", historic = true, history = 90,
+ history_base = "37074e22e8be",
options = "-m32 -B -M1x2,2 -t polyml-5.7 -e 'init_component /home/isabelle/contrib/polyml-5.7'",
args = "-N -g timing",
detect = Build_Log.Prop.build_tags + " = " + SQL.string("polyml-5.7"))),
List(Remote_Build("Linux A", "lxbroy9",
options = "-m32 -B -M1x2,2", args = "-N -g timing")),
- List(Remote_Build("Linux B", "lxbroy10", history = 90, historic = true,
+ List(Remote_Build("Linux B", "lxbroy10", historic = true, history = 90,
options = "-m32 -B -M1x4,2,4,6", args = "-N -g timing")),
List(
Remote_Build("Mac OS X 10.9 Mavericks", "macbroy2", options = "-m32 -M8", args = "-a",
@@ -366,14 +378,17 @@
val main_start_date = Date.now()
File.write(main_state_file, main_start_date + " " + log_service.hostname)
- val rev = Mercurial.repository(isabelle_repos).id()
+ val hg = Mercurial.repository(isabelle_repos)
+ val rev = hg.id()
run(main_start_date,
Logger_Task("isabelle_cronjob", logger =>
run_now(
SEQ(List(build_release, build_history_base,
PAR(remote_builds.map(seq =>
- SEQ(seq.flatMap(r => r.pick(logger.options, rev).map(remote_build_history(_, r)))))),
+ SEQ(seq.flatMap(r =>
+ r.pick(logger.options, rev, r.history_base_filter(hg)).
+ map(remote_build_history(_, r)))))),
Logger_Task("jenkins_logs", _ => Jenkins.download_logs(jenkins_jobs, main_dir)),
Logger_Task("build_log_database",
logger => Isabelle_Devel.build_log_database(logger.options)),
--- a/src/Pure/Admin/isabelle_devel.scala Sun May 14 13:55:51 2017 +0200
+++ b/src/Pure/Admin/isabelle_devel.scala Sun May 14 22:07:16 2017 +0200
@@ -25,27 +25,25 @@
{
val header = "Isabelle Development Resources"
- Isabelle_System.mkdirs(root)
- File.write(root + Path.explode("index.html"),
- HTML.output_document(
- List(HTML.title(header)),
- List(HTML.chapter(header),
- HTML.itemize(
- List(
- HTML.text("Isabelle nightly ") :::
- List(HTML.link(RELEASE_SNAPSHOT, HTML.text("release snapshot"))) :::
- HTML.text(" (for all platforms)"),
+ HTML.write_document(root, "index.html",
+ List(HTML.title(header)),
+ List(HTML.chapter(header),
+ HTML.itemize(
+ List(
+ HTML.text("Isabelle nightly ") :::
+ List(HTML.link(RELEASE_SNAPSHOT, HTML.text("release snapshot"))) :::
+ HTML.text(" (for all platforms)"),
- HTML.text("Isabelle ") :::
- List(HTML.link(BUILD_STATUS + "/index.html", HTML.text("build status"))) :::
- HTML.text(" information"),
+ HTML.text("Isabelle ") :::
+ List(HTML.link(BUILD_STATUS + "/index.html", HTML.text("build status"))) :::
+ HTML.text(" information"),
- HTML.text("Database with recent ") :::
- List(HTML.link(BUILD_LOG_DB, HTML.text("build log"))) :::
- HTML.text(" information (e.g. for ") :::
- List(HTML.link("http://sqlitebrowser.org",
- List(HTML.code(HTML.text("sqlitebrowser"))))) :::
- HTML.text(")"))))))
+ HTML.text("Database with recent ") :::
+ List(HTML.link(BUILD_LOG_DB, HTML.text("build log"))) :::
+ HTML.text(" information (e.g. for ") :::
+ List(HTML.link("http://sqlitebrowser.org",
+ List(HTML.code(HTML.text("sqlitebrowser"))))) :::
+ HTML.text(")")))))
}
--- a/src/Pure/General/exn.scala Sun May 14 13:55:51 2017 +0200
+++ b/src/Pure/General/exn.scala Sun May 14 22:07:16 2017 +0200
@@ -20,7 +20,7 @@
}
override def hashCode: Int = message.hashCode
- override def toString: String = "\n" + Output.error_text(message)
+ override def toString: String = "\n" + Output.error_message_text(message)
}
object ERROR
--- a/src/Pure/General/http.scala Sun May 14 13:55:51 2017 +0200
+++ b/src/Pure/General/http.scala Sun May 14 22:07:16 2017 +0200
@@ -77,7 +77,7 @@
case Exn.Res(None) =>
http.write_response(404, Response.empty)
case Exn.Exn(ERROR(msg)) =>
- http.write_response(500, Response.text(Output.error_text(msg)))
+ http.write_response(500, Response.text(Output.error_message_text(msg)))
case Exn.Exn(exn) => throw exn
}
else http.write_response(400, Response.empty)
--- a/src/Pure/General/mercurial.scala Sun May 14 13:55:51 2017 +0200
+++ b/src/Pure/General/mercurial.scala Sun May 14 22:07:16 2017 +0200
@@ -10,6 +10,9 @@
import java.io.{File => JFile}
+import scala.annotation.tailrec
+import scala.collection.mutable
+
object Mercurial
{
@@ -68,7 +71,7 @@
case Some(ssh) => ssh.is_dir(root)
}
if (present) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg }
- else clone_repository(source, root, options = "--noupdate", ssh = ssh)
+ else clone_repository(source, root, options = "--pull --noupdate", ssh = ssh)
}
class Repository private[Mercurial](root_path: Path, ssh: Option[SSH.Session])
@@ -96,7 +99,7 @@
def command(name: String, args: String = "", options: String = ""): Process_Result =
{
val cmdline =
- "\"${HG:-hg}\"" +
+ "\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
(if (name == "clone") "" else " --repository " + File.bash_path(root)) +
" --noninteractive " + name + " " + options + " " + args
ssh match {
@@ -137,5 +140,50 @@
hg.command("update",
opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check), options).check
}
+
+ def known_files(): List[String] =
+ hg.command("status", options = "--modified --added --clean --no-status").check.out_lines
+
+ def graph(): Graph[String, Unit] =
+ {
+ val Node = """^node: (\w{12}) (\w{12}) (\w{12})""".r
+ val log_result =
+ log(template = """node: {node|short} {p1node|short} {p2node|short}\n""")
+ (Graph.string[Unit] /: split_lines(log_result)) {
+ case (graph, Node(x, y, z)) =>
+ val deps = List(y, z).filterNot(s => s.forall(_ == '0'))
+ val graph1 = (graph /: (x :: deps))(_.default_node(_, ()))
+ (graph1 /: deps)({ case (g, dep) => g.add_edge(dep, x) })
+ case (graph, _) => graph
+ }
+ }
+ }
+
+
+ /* unknown files */
+
+ def unknown_files(files: List[Path], ssh: Option[SSH.Session] = None): List[Path] =
+ {
+ val unknown = new mutable.ListBuffer[Path]
+
+ @tailrec def check(paths: List[Path])
+ {
+ paths match {
+ case path :: rest =>
+ find_repository(path, ssh) match {
+ case None => unknown += path; check(rest)
+ case Some(hg) =>
+ val known =
+ hg.known_files().iterator.map(name =>
+ (hg.root + Path.explode(name)).canonical_file).toSet
+ if (!known(path.canonical_file)) unknown += path
+ check(rest.filterNot(p => known(p.canonical_file)))
+ }
+ case Nil =>
+ }
+ }
+
+ check(files)
+ unknown.toList
}
}
--- a/src/Pure/General/output.scala Sun May 14 13:55:51 2017 +0200
+++ b/src/Pure/General/output.scala Sun May 14 22:07:16 2017 +0200
@@ -14,8 +14,12 @@
catch { case ERROR(_) => msg }
def writeln_text(msg: String): String = clean_yxml(msg)
- def warning_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("### " + _))
- def error_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("*** " + _))
+
+ def warning_text(msg: String): String =
+ cat_lines(split_lines(clean_yxml(msg)).map("### " + _))
+
+ def error_message_text(msg: String): String =
+ cat_lines(split_lines(clean_yxml(msg)).map("*** " + _))
def writeln(msg: String, stdout: Boolean = false)
{
@@ -36,8 +40,8 @@
def error_message(msg: String, stdout: Boolean = false)
{
if (msg != "") {
- if (stdout) Console.println(error_text(msg))
- else Console.err.println(error_text(msg))
+ if (stdout) Console.println(error_message_text(msg))
+ else Console.err.println(error_message_text(msg))
}
}
}
--- a/src/Pure/General/path.scala Sun May 14 13:55:51 2017 +0200
+++ b/src/Pure/General/path.scala Sun May 14 22:07:16 2017 +0200
@@ -211,4 +211,6 @@
def file: JFile = File.platform_file(this)
def is_file: Boolean = file.isFile
def is_dir: Boolean = file.isDirectory
+
+ def canonical_file: JFile = file.getCanonicalFile
}
--- a/src/Pure/System/numa.scala Sun May 14 13:55:51 2017 +0200
+++ b/src/Pure/System/numa.scala Sun May 14 22:07:16 2017 +0200
@@ -42,7 +42,7 @@
/* shuffling of CPU nodes */
- def enabled_warning(enabled: Boolean): Boolean =
+ def enabled_warning(progress: Progress, enabled: Boolean): Boolean =
{
def warning =
if (nodes().length < 2) Some("no NUMA nodes available")
@@ -51,7 +51,7 @@
enabled &&
(warning match {
- case Some(s) => Output.warning("Shuffling of CPU nodes is disabled: " + s); false
+ case Some(s) => progress.echo_warning("Shuffling of CPU nodes is disabled: " + s); false
case _ => true
})
}
--- a/src/Pure/System/progress.scala Sun May 14 13:55:51 2017 +0200
+++ b/src/Pure/System/progress.scala Sun May 14 22:07:16 2017 +0200
@@ -16,6 +16,9 @@
def echo_if(cond: Boolean, msg: String) { if (cond) echo(msg) }
def theory(session: String, theory: String) {}
+ def echo_warning(msg: String) { echo(Output.warning_text(msg)) }
+ def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) }
+
def stopped: Boolean = false
override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
--- a/src/Pure/Thy/html.scala Sun May 14 13:55:51 2017 +0200
+++ b/src/Pure/Thy/html.scala Sun May 14 22:07:16 2017 +0200
@@ -58,6 +58,10 @@
/* output XML as HTML */
+ private val structural_elements =
+ Set("head", "body", "meta", "div", "pre", "p", "title", "h1", "h2", "h3", "h4", "h5", "h6",
+ "ul", "ol", "dl", "li", "dt", "dd")
+
def output(body: XML.Body, s: StringBuilder)
{
def attrib(p: (String, String)): Unit =
@@ -69,9 +73,11 @@
case XML.Elem(markup, Nil) =>
s ++= "<"; elem(markup); s ++= "/>"
case XML.Elem(markup, ts) =>
- s ++= "\n<"; elem(markup); s ++= ">"
+ if (structural_elements(markup.name)) s += '\n'
+ s ++= "<"; elem(markup); s ++= ">"
ts.foreach(tree)
- s ++= "</"; s ++= markup.name; s ++= ">\n"
+ s ++= "</"; s ++= markup.name; s ++= ">"
+ if (structural_elements(markup.name)) s += '\n'
case XML.Text(txt) => output(txt, s)
}
body.foreach(tree)
@@ -142,13 +148,32 @@
XML.Elem(Markup("meta",
List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil)
- def output_document(head: XML.Body, body: XML.Body): String =
+ def head_css(css: String): XML.Elem =
+ XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> css)), Nil)
+
+ def output_document(head: XML.Body, body: XML.Body, css: String = "isabelle.css"): String =
cat_lines(
List(header,
- output(XML.elem("head", head_meta :: head)),
+ output(XML.elem("head", head_meta :: (if (css == "") Nil else List(head_css(css))) ::: head)),
output(XML.elem("body", body))))
+ /* document directory */
+
+ def init_dir(dir: Path)
+ {
+ Isabelle_System.mkdirs(dir)
+ File.copy(Path.explode("~~/etc/isabelle.css"), dir)
+ }
+
+ def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body,
+ css: String = "isabelle.css")
+ {
+ init_dir(dir)
+ File.write(dir + Path.basic(name), output_document(head, body, css))
+ }
+
+
/* Isabelle document */
def begin_document(title: String): String =
--- a/src/Pure/Thy/sessions.scala Sun May 14 13:55:51 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Sun May 14 22:07:16 2017 +0200
@@ -37,9 +37,9 @@
def local_theories_iterator =
{
- val local_path = local_dir.file.getCanonicalFile.toPath
+ val local_path = local_dir.canonical_file.toPath
theories.iterator.filter(name =>
- Path.explode(name.node).file.getCanonicalFile.toPath.startsWith(local_path))
+ Path.explode(name.node).canonical_file.toPath.startsWith(local_path))
}
val known_theories =
@@ -60,7 +60,7 @@
(Map.empty[JFile, List[Document.Node.Name]] /:
(bases_iterator(true) ++ bases_iterator(false) ++ theories.iterator))({
case (known, name) =>
- val file = Path.explode(name.node).file.getCanonicalFile
+ val file = Path.explode(name.node).canonical_file
val theories1 = known.getOrElse(file, Nil)
if (theories1.exists(name1 => name.node == name1.node && name.theory == name1.theory))
known
--- a/src/Pure/Tools/build.scala Sun May 14 13:55:51 2017 +0200
+++ b/src/Pure/Tools/build.scala Sun May 14 22:07:16 2017 +0200
@@ -34,7 +34,8 @@
private object Queue
{
- def load_timings(store: Sessions.Store, name: String): (List[Properties.T], Double) =
+ def load_timings(progress: Progress, store: Sessions.Store, name: String)
+ : (List[Properties.T], Double) =
{
val no_timings: (List[Properties.T], Double) = (Nil, 0.0)
@@ -43,7 +44,7 @@
case Some(database) =>
def ignore_error(msg: String) =
{
- Output.warning("Ignoring bad database: " +
+ progress.echo_warning("Ignoring bad database: " +
database.expand + (if (msg == "") "" else "\n" + msg))
no_timings
}
@@ -63,12 +64,12 @@
}
}
- def apply(sessions: Sessions.T, store: Sessions.Store): Queue =
+ def apply(progress: Progress, sessions: Sessions.T, store: Sessions.Store): Queue =
{
val graph = sessions.build_graph
val names = graph.keys
- val timings = names.map(name => (name, load_timings(store, name)))
+ val timings = names.map(name => (name, load_timings(progress, store, name)))
val command_timings =
Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
val session_timing =
@@ -245,7 +246,7 @@
case msg =>
result.copy(
rc = result.rc max 1,
- out_lines = result.out_lines ::: split_lines(Output.error_text(msg)))
+ out_lines = result.out_lines ::: split_lines(Output.error_message_text(msg)))
}
}
else {
@@ -309,8 +310,8 @@
timeout_request.foreach(_.cancel)
if (result.interrupted) {
- if (was_timeout) result.error(Output.error_text("Timeout")).was_timeout
- else result.error(Output.error_text("Interrupt"))
+ if (was_timeout) result.error(Output.error_message_text("Timeout")).was_timeout
+ else result.error(Output.error_message_text("Interrupt"))
}
else result
}
@@ -337,6 +338,7 @@
def build(
options: Options,
progress: Progress = No_Progress,
+ check_unknown_files: Boolean = false,
build_heap: Boolean = false,
clean_build: Boolean = false,
dirs: List[Path] = Nil,
@@ -376,11 +378,24 @@
def sources_stamp(name: String): List[String] =
(selected_sessions(name).meta_digest :: deps.sources(name)).map(_.toString).sorted
+ if (check_unknown_files) {
+ val source_files =
+ (for {
+ (_, base) <- deps.session_bases.iterator
+ (path, _) <- base.sources.iterator
+ } yield path).toList
+ val unknown_files = Mercurial.unknown_files(source_files)
+ if (unknown_files.nonEmpty) {
+ progress.echo_warning("Unknown files (not part of a Mercurial repository):" +
+ unknown_files.map(path => path.expand.implode).sorted.mkString("\n ", "\n ", ""))
+ }
+ }
+
/* main build process */
val store = Sessions.store(system_mode)
- val queue = Queue(selected_sessions, store)
+ val queue = Queue(progress, selected_sessions, store)
store.prepare_output()
@@ -551,7 +566,7 @@
val results0 =
if (deps.is_empty) {
- progress.echo(Output.warning_text("Nothing to build"))
+ progress.echo_warning("Nothing to build")
Map.empty[String, Result]
}
else loop(queue, Map.empty, Map.empty)
@@ -679,11 +694,12 @@
val results =
progress.interrupt_handler {
build(options, progress,
+ check_unknown_files = Mercurial.is_repository(Path.explode("~~")),
build_heap = build_heap,
clean_build = clean_build,
dirs = dirs,
select_dirs = select_dirs,
- numa_shuffling = NUMA.enabled_warning(numa_shuffling),
+ numa_shuffling = NUMA.enabled_warning(progress, numa_shuffling),
max_jobs = max_jobs,
list_files = list_files,
check_keywords = check_keywords,
--- a/src/Pure/Tools/check_keywords.scala Sun May 14 13:55:51 2017 +0200
+++ b/src/Pure/Tools/check_keywords.scala Sun May 14 22:07:16 2017 +0200
@@ -46,9 +46,8 @@
}, parallel_args).flatten
for ((tok, pos) <- bad) {
- progress.echo(Output.warning_text(
- "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) +
- Position.here(pos)))
+ progress.echo_warning(
+ "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) + Position.here(pos))
}
}
}
--- a/src/Pure/Tools/imports.scala Sun May 14 13:55:51 2017 +0200
+++ b/src/Pure/Tools/imports.scala Sun May 14 22:07:16 2017 +0200
@@ -12,17 +12,18 @@
object Imports
{
- /* manifest */
+ /* repository files */
- def manifest_files(start: Path, pred: JFile => Boolean = _ => true): List[JFile] =
+ def repository_files(progress: Progress, start: Path, pred: JFile => Boolean = _ => true)
+ : List[JFile] =
Mercurial.find_repository(start) match {
case None =>
- Output.warning("Ignoring directory " + start + " (no Mercurial repository)")
+ progress.echo_warning("Ignoring directory " + start + " (no Mercurial repository)")
Nil
case Some(hg) =>
- val start_path = start.file.getCanonicalFile.toPath
+ val start_path = start.canonical_file.toPath
for {
- name <- hg.manifest()
+ name <- hg.known_files()
file = (hg.root + Path.explode(name)).file
if pred(file) && file.getCanonicalFile.toPath.startsWith(start_path)
} yield file
@@ -45,7 +46,7 @@
{
val file =
pos match {
- case Position.File(file) => Path.explode(file).file.getCanonicalFile
+ case Position.File(file) => Path.explode(file).canonical_file
case _ => error("Missing file in position" + Position.here(pos))
}
@@ -72,7 +73,7 @@
def imports(
options: Options,
operation_imports: Boolean = false,
- operation_manifest: Boolean = false,
+ operation_repository_files: Boolean = false,
operation_update: Boolean = false,
progress: Progress = No_Progress,
selection: Sessions.Selection = Sessions.Selection.empty,
@@ -116,12 +117,12 @@
})
}
- if (operation_manifest) {
- progress.echo("\nManifest check:")
+ if (operation_repository_files) {
+ progress.echo("\nMercurial files check:")
val unused_files =
for {
(_, dir) <- Sessions.directories(dirs, select_dirs)
- file <- manifest_files(dir, file => file.getName.endsWith(".thy"))
+ file <- repository_files(progress, dir, file => file.getName.endsWith(".thy"))
if deps.all_known.get_file(file).isEmpty
} yield file
unused_files.foreach(file => progress.echo("unused file " + quote(file.toString)))
@@ -211,7 +212,7 @@
{
var select_dirs: List[Path] = Nil
var operation_imports = false
- var operation_manifest = false
+ var operation_repository_files = false
var requirements = false
var operation_update = false
var exclude_session_groups: List[String] = Nil
@@ -228,7 +229,7 @@
Options are:
-D DIR include session directory and select its sessions
-I operation: report potential session imports
- -M operation: Mercurial manifest check for imported theory files
+ -M operation: Mercurial files check for imported theory files
-R operate on requirements of selected sessions
-U operation: update theory imports to use session qualifiers
-X NAME exclude sessions from group NAME and all descendants
@@ -244,7 +245,7 @@
""",
"D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
"I" -> (_ => operation_imports = true),
- "M" -> (_ => operation_manifest = true),
+ "M" -> (_ => operation_repository_files = true),
"R" -> (_ => requirements = true),
"U" -> (_ => operation_update = true),
"X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
@@ -256,7 +257,7 @@
"x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
val sessions = getopts(args)
- if (args.isEmpty || !(operation_imports || operation_manifest || operation_update))
+ if (args.isEmpty || !(operation_imports || operation_repository_files || operation_update))
getopts.usage()
val selection =
@@ -266,7 +267,7 @@
val progress = new Console_Progress(verbose = verbose)
imports(options, operation_imports = operation_imports,
- operation_manifest = operation_manifest, operation_update = operation_update,
+ operation_repository_files = operation_repository_files, operation_update = operation_update,
progress = progress, selection = selection, dirs = dirs, select_dirs = select_dirs,
verbose = verbose)
})
--- a/src/Tools/VSCode/src/channel.scala Sun May 14 13:55:51 2017 +0200
+++ b/src/Tools/VSCode/src/channel.scala Sun May 14 22:07:16 2017 +0200
@@ -110,6 +110,8 @@
def make_progress(verbose: Boolean = false): Progress =
new Progress {
override def echo(msg: String): Unit = log_writeln(msg)
+ override def echo_warning(msg: String): Unit = log_warning(msg)
+ override def echo_error_message(msg: String): Unit = log_error_message(msg)
override def theory(session: String, theory: String): Unit =
if (verbose) echo(session + ": theory " + theory)
}
--- a/src/Tools/jEdit/src/session_build.scala Sun May 14 13:55:51 2017 +0200
+++ b/src/Tools/jEdit/src/session_build.scala Sun May 14 22:07:16 2017 +0200
@@ -173,7 +173,7 @@
try { ("", JEdit_Sessions.session_build(options, progress = progress)) }
catch {
case exn: Throwable =>
- (Output.error_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2))
+ (Output.error_message_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2))
}
progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))