# HG changeset patch
# User wenzelm
# Date 1427905013 -7200
# Node ID a68a0fec288d3691448d4af14a12ec11856ebd63
# Parent  ca16b657901f34ca0b9f0ae36aba2698d3ae7fd5
clarified module;
more parallel processing;

diff -r ca16b657901f -r a68a0fec288d src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Apr 01 17:58:23 2015 +0200
+++ b/src/Pure/Tools/build.scala	Wed Apr 01 18:16:53 2015 +0200
@@ -507,17 +507,8 @@
             if (list_files)
               progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
 
-            if (check_keywords.nonEmpty) {
-              for (path <- theory_files) {
-                if (progress.stopped) throw Exn.Interrupt()
-                for ((tok, pos) <- Check_Keywords.conflicts(syntax.keywords, check_keywords, path))
-                {
-                  progress.echo(Output.warning_text(
-                    "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) +
-                      Position.here(pos)))
-                }
-              }
-            }
+            if (check_keywords.nonEmpty)
+              Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files)
 
             val sources = all_files.map(p => (p, SHA1.digest(p.file)))
 
diff -r ca16b657901f -r a68a0fec288d src/Pure/Tools/check_keywords.scala
--- a/src/Pure/Tools/check_keywords.scala	Wed Apr 01 17:58:23 2015 +0200
+++ b/src/Pure/Tools/check_keywords.scala	Wed Apr 01 18:16:53 2015 +0200
@@ -31,7 +31,24 @@
     Parser.result
   }
 
-  def conflicts(
-    keywords: Keyword.Keywords, check: Set[String], path: Path): List[(Token, Position.T)] =
-    conflicts(keywords, check, File.read(path), Token.Pos.file(path.expand.implode))
+  def check_keywords(
+    progress: Build.Progress,
+    keywords: Keyword.Keywords,
+    check: Set[String],
+    paths: List[Path])
+  {
+    val parallel_args = paths.map(path => (File.read(path), Token.Pos.file(path.expand.implode)))
+
+    val bad =
+      Par_List.map((arg: (String, Token.Pos)) => {
+        if (progress.stopped) throw Exn.Interrupt()
+        conflicts(keywords, check, arg._1, arg._2)
+      }, parallel_args).flatten
+
+    for ((tok, pos) <- bad) {
+      progress.echo(Output.warning_text(
+        "keyword conflict: " + tok.kind.toString + " " + quote(tok.content) +
+          Position.here(pos)))
+    }
+  }
 }