clarified: repository files before commit;
authorwenzelm
Sun May 14 15:58:07 2017 +0200 (2017-05-14)
changeset 658244ff79bd2b265
parent 65823 4f353215888a
child 65825 11f87ab51ddb
clarified: repository files before commit;
src/Pure/Tools/imports.scala
     1.1 --- a/src/Pure/Tools/imports.scala	Sun May 14 15:35:25 2017 +0200
     1.2 +++ b/src/Pure/Tools/imports.scala	Sun May 14 15:58:07 2017 +0200
     1.3 @@ -12,9 +12,9 @@
     1.4  
     1.5  object Imports
     1.6  {
     1.7 -  /* manifest */
     1.8 +  /* repository files */
     1.9  
    1.10 -  def manifest_files(start: Path, pred: JFile => Boolean = _ => true): List[JFile] =
    1.11 +  def repository_files(start: Path, pred: JFile => Boolean = _ => true): List[JFile] =
    1.12      Mercurial.find_repository(start) match {
    1.13        case None =>
    1.14          Output.warning("Ignoring directory " + start + " (no Mercurial repository)")
    1.15 @@ -22,7 +22,7 @@
    1.16        case Some(hg) =>
    1.17          val start_path = start.file.getCanonicalFile.toPath
    1.18          for {
    1.19 -          name <- hg.manifest()
    1.20 +          name <- hg.known_files()
    1.21            file = (hg.root + Path.explode(name)).file
    1.22            if pred(file) && file.getCanonicalFile.toPath.startsWith(start_path)
    1.23          } yield file
    1.24 @@ -72,7 +72,7 @@
    1.25    def imports(
    1.26      options: Options,
    1.27      operation_imports: Boolean = false,
    1.28 -    operation_manifest: Boolean = false,
    1.29 +    operation_repository_files: Boolean = false,
    1.30      operation_update: Boolean = false,
    1.31      progress: Progress = No_Progress,
    1.32      selection: Sessions.Selection = Sessions.Selection.empty,
    1.33 @@ -116,12 +116,12 @@
    1.34        })
    1.35      }
    1.36  
    1.37 -    if (operation_manifest) {
    1.38 -      progress.echo("\nManifest check:")
    1.39 +    if (operation_repository_files) {
    1.40 +      progress.echo("\nMercurial files check:")
    1.41        val unused_files =
    1.42          for {
    1.43            (_, dir) <- Sessions.directories(dirs, select_dirs)
    1.44 -          file <- manifest_files(dir, file => file.getName.endsWith(".thy"))
    1.45 +          file <- repository_files(dir, file => file.getName.endsWith(".thy"))
    1.46            if deps.all_known.get_file(file).isEmpty
    1.47          } yield file
    1.48        unused_files.foreach(file => progress.echo("unused file " + quote(file.toString)))
    1.49 @@ -211,7 +211,7 @@
    1.50      {
    1.51        var select_dirs: List[Path] = Nil
    1.52        var operation_imports = false
    1.53 -      var operation_manifest = false
    1.54 +      var operation_repository_files = false
    1.55        var requirements = false
    1.56        var operation_update = false
    1.57        var exclude_session_groups: List[String] = Nil
    1.58 @@ -228,7 +228,7 @@
    1.59    Options are:
    1.60      -D DIR       include session directory and select its sessions
    1.61      -I           operation: report potential session imports
    1.62 -    -M           operation: Mercurial manifest check for imported theory files
    1.63 +    -M           operation: Mercurial files check for imported theory files
    1.64      -R           operate on requirements of selected sessions
    1.65      -U           operation: update theory imports to use session qualifiers
    1.66      -X NAME      exclude sessions from group NAME and all descendants
    1.67 @@ -244,7 +244,7 @@
    1.68  """,
    1.69        "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
    1.70        "I" -> (_ => operation_imports = true),
    1.71 -      "M" -> (_ => operation_manifest = true),
    1.72 +      "M" -> (_ => operation_repository_files = true),
    1.73        "R" -> (_ => requirements = true),
    1.74        "U" -> (_ => operation_update = true),
    1.75        "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
    1.76 @@ -256,7 +256,7 @@
    1.77        "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
    1.78  
    1.79        val sessions = getopts(args)
    1.80 -      if (args.isEmpty || !(operation_imports || operation_manifest || operation_update))
    1.81 +      if (args.isEmpty || !(operation_imports || operation_repository_files || operation_update))
    1.82          getopts.usage()
    1.83  
    1.84        val selection =
    1.85 @@ -266,7 +266,7 @@
    1.86        val progress = new Console_Progress(verbose = verbose)
    1.87  
    1.88        imports(options, operation_imports = operation_imports,
    1.89 -        operation_manifest = operation_manifest, operation_update = operation_update,
    1.90 +        operation_repository_files = operation_repository_files, operation_update = operation_update,
    1.91          progress = progress, selection = selection, dirs = dirs, select_dirs = select_dirs,
    1.92          verbose = verbose)
    1.93      })