# HG changeset patch
# User wenzelm
# Date 1379343049 -7200
# Node ID ea8343187225d9abd172a7ec5cded36c513df44c
# Parent  51595a047730b027af5668dfc77f18ed013bd027
adhoc check of ML sources, in addition to thy files already covered in Thy_Load;

diff -r 51595a047730 -r ea8343187225 Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST	Mon Sep 16 16:46:52 2013 +0200
+++ b/Admin/Release/CHECKLIST	Mon Sep 16 16:50:49 2013 +0200
@@ -19,6 +19,8 @@
 
 - check file positions within logic images (hyperlinks etc.);
 
+- check ML sources: isabelle build -nal;
+
 - run isabelle update_keywords;
 
 - check ANNOUNCE, README, NEWS, COPYRIGHT, CONTRIBUTORS;
diff -r 51595a047730 -r ea8343187225 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Sep 16 16:46:52 2013 +0200
+++ b/src/Pure/Tools/build.scala	Mon Sep 16 16:50:49 2013 +0200
@@ -441,8 +441,22 @@
             (thy_deps.deps.map(dep => Path.explode(dep.name.node)) ::: body_files :::
               info.files.map(file => info.dir + file)).map(_.expand)
 
-          if (list_files)
+          if (list_files) {
             progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
+            for {
+              file <- all_files
+              if file.split_ext._2 == "ML"
+            } {
+              val path = info.dir + file
+              try { Symbol.decode_strict(File.read(path)) }
+              catch {
+                case ERROR(msg) =>
+                  cat_error(msg,
+                    "The error(s) above occurred in session " + quote(name) +
+                      " file " + path.toString)
+              }
+            }
+          }
 
           val sources =
             try { all_files.map(p => (p, SHA1.digest(p.file))) }