clarified notion of unknown files: ignore files outside of a Mercurial repository;

--- a/src/Pure/General/mercurial.scala	Thu Mar 08 11:20:45 2018 +0100
+++ b/src/Pure/General/mercurial.scala	Thu Mar 08 11:46:37 2018 +0100
@@ -151,10 +151,11 @@
   }
 
 
-  /* unknown files */
+  /* check files */
 
-  def unknown_files(files: List[Path], ssh: SSH.System = SSH.Local): List[Path] =
+  def check_files(files: List[Path], ssh: SSH.System = SSH.Local): (List[Path], List[Path]) =
   {
+    val outside = new mutable.ListBuffer[Path]
     val unknown = new mutable.ListBuffer[Path]
 
     @tailrec def check(paths: List[Path])
@@ -162,7 +163,7 @@
       paths match {
         case path :: rest =>
           find_repository(path, ssh) match {
-            case None => unknown += path; check(rest)
+            case None => outside += path; check(rest)
             case Some(hg) =>
               val known =
                 hg.known_files().iterator.map(name =>
@@ -175,6 +176,6 @@
     }
 
     check(files)
-    unknown.toList
+    (outside.toList, unknown.toList)
   }
 }

--- a/src/Pure/Tools/build.scala	Thu Mar 08 11:20:45 2018 +0100
+++ b/src/Pure/Tools/build.scala	Thu Mar 08 11:46:37 2018 +0100
@@ -438,10 +438,10 @@
         } yield path).toList
       val exclude_files = List(Path.explode("$POLYML_EXE")).map(_.canonical_file)
       val unknown_files =
-        Mercurial.unknown_files(source_files).
+        Mercurial.check_files(source_files)._2.
           filterNot(path => exclude_files.contains(path.canonical_file))
       if (unknown_files.nonEmpty) {
-        progress.echo_warning("Unknown files (not part of a Mercurial repository):" +
+        progress.echo_warning("Unknown files (not part of the underlying Mercurial repository):" +
           unknown_files.map(path => path.expand.implode).sorted.mkString("\n  ", "\n  ", ""))
       }
     }