src/Pure/Tools/check_keywords.scala
changeset 59895 a68a0fec288d
parent 59891 9ce697050455
child 61276 8a4bd05c1735
--- 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)))
+    }
+  }
 }