adhoc check of ML sources, in addition to thy files already covered in Thy_Load;
authorwenzelm
Mon, 16 Sep 2013 16:50:49 +0200
changeset 53665 ea8343187225
parent 53664 51595a047730
child 53666 52a0a526e677
adhoc check of ML sources, in addition to thy files already covered in Thy_Load;
Admin/Release/CHECKLIST
src/Pure/Tools/build.scala
--- 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;
--- 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))) }