src/Pure/Tools/imports.scala
changeset 65561 741b1d3930c0
parent 65558 479406635409
child 65564 5b3cae328a94
     1.1 --- a/src/Pure/Tools/imports.scala	Sun Apr 23 18:12:42 2017 +0200
     1.2 +++ b/src/Pure/Tools/imports.scala	Sun Apr 23 18:47:56 2017 +0200
     1.3 @@ -12,6 +12,23 @@
     1.4  
     1.5  object Imports
     1.6  {
     1.7 +  /* manifest */
     1.8 +
     1.9 +  def manifest_files(start: Path, pred: JFile => Boolean = _ => true): List[JFile] =
    1.10 +    Mercurial.find_repository(start) match {
    1.11 +      case None =>
    1.12 +        Output.warning("Ignoring directory " + quote(start.toString) + " (no Mercurial repository)")
    1.13 +        Nil
    1.14 +      case Some(hg) =>
    1.15 +        val start_path = start.file.getCanonicalFile.toPath
    1.16 +        for {
    1.17 +          name <- hg.manifest()
    1.18 +          file = (hg.root + Path.explode(name)).file
    1.19 +          if pred(file) && file.getCanonicalFile.toPath.startsWith(start_path)
    1.20 +        } yield file
    1.21 +    }
    1.22 +
    1.23 +
    1.24    /* update imports */
    1.25  
    1.26    sealed case class Update(range: Text.Range, old_text: String, new_text: String)
    1.27 @@ -81,8 +98,12 @@
    1.28      }
    1.29    }
    1.30  
    1.31 +
    1.32 +  /* collective operations */
    1.33 +
    1.34    def imports(
    1.35      options: Options,
    1.36 +    operation_manifest: Boolean = false,
    1.37      operation_update: Boolean = false,
    1.38      progress: Progress = No_Progress,
    1.39      selection: Sessions.Selection = Sessions.Selection.empty,
    1.40 @@ -95,7 +116,19 @@
    1.41  
    1.42      val deps =
    1.43        Sessions.deps(selected_sessions, progress = progress, verbose = verbose,
    1.44 -        global_theories = full_sessions.global_theories)
    1.45 +        global_theories = full_sessions.global_theories,
    1.46 +        all_known = true)
    1.47 +
    1.48 +    if (operation_manifest) {
    1.49 +      progress.echo("\nManifest check:")
    1.50 +      val unused_files =
    1.51 +        for {
    1.52 +          (_, dir) <- Sessions.directories(dirs, select_dirs)
    1.53 +          file <- manifest_files(dir, file => file.getName.endsWith(".thy"))
    1.54 +          if deps.all_known.get_file(file).isEmpty
    1.55 +        } yield file
    1.56 +      unused_files.foreach(file => progress.echo("unused file " + quote(file.toString)))
    1.57 +    }
    1.58  
    1.59      if (operation_update) {
    1.60        val updates =
    1.61 @@ -156,6 +189,7 @@
    1.62      Isabelle_Tool("imports", "maintain theory imports wrt. session structure", args =>
    1.63      {
    1.64        var select_dirs: List[Path] = Nil
    1.65 +      var operation_manifest = false
    1.66        var requirements = false
    1.67        var operation_update = false
    1.68        var exclude_session_groups: List[String] = Nil
    1.69 @@ -171,6 +205,7 @@
    1.70  
    1.71    Options are:
    1.72      -D DIR       include session directory and select its sessions
    1.73 +    -M           operation: Mercurial manifest check for imported theory files
    1.74      -R           operate on requirements of selected sessions
    1.75      -U           operation: update theory imports to use session qualifiers
    1.76      -X NAME      exclude sessions from group NAME and all descendants
    1.77 @@ -185,6 +220,7 @@
    1.78    needs to be specified (see option -U).
    1.79  """,
    1.80        "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
    1.81 +      "M" -> (_ => operation_manifest = true),
    1.82        "R" -> (_ => requirements = true),
    1.83        "U" -> (_ => operation_update = true),
    1.84        "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
    1.85 @@ -196,7 +232,8 @@
    1.86        "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
    1.87  
    1.88        val sessions = getopts(args)
    1.89 -      if (args.isEmpty || !operation_update) getopts.usage()
    1.90 +      if (args.isEmpty || !(operation_manifest || operation_update))
    1.91 +        getopts.usage()
    1.92  
    1.93        val selection =
    1.94          Sessions.Selection(requirements, all_sessions, exclude_session_groups,
    1.95 @@ -204,7 +241,8 @@
    1.96  
    1.97        val progress = new Console_Progress(verbose = verbose)
    1.98  
    1.99 -      imports(options, operation_update = operation_update, progress = progress,
   1.100 -        selection = selection, dirs = dirs, select_dirs = select_dirs, verbose = verbose)
   1.101 +      imports(options, operation_manifest = operation_manifest, operation_update = operation_update,
   1.102 +        progress = progress, selection = selection, dirs = dirs, select_dirs = select_dirs,
   1.103 +        verbose = verbose)
   1.104      })
   1.105  }