support for Mercurial manifest check;
authorwenzelm
Sun Apr 23 18:47:56 2017 +0200 (2017-04-23)
changeset 65561741b1d3930c0
parent 65560 327842649e8d
child 65562 f9753d949afc
support for Mercurial manifest check;
src/Pure/Thy/sessions.scala
src/Pure/Tools/imports.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Sun Apr 23 18:12:42 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Sun Apr 23 18:47:56 2017 +0200
     1.3 @@ -628,6 +628,12 @@
     1.4      if (is_session_dir(dir)) File.pwd() + dir.expand
     1.5      else error("Bad session root directory: " + dir.toString)
     1.6  
     1.7 +  def directories(dirs: List[Path], select_dirs: List[Path]): List[(Boolean, Path)] =
     1.8 +  {
     1.9 +    val default_dirs = Isabelle_System.components().filter(is_session_dir(_))
    1.10 +    (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
    1.11 +  }
    1.12 +
    1.13    def load(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil): T =
    1.14    {
    1.15      def load_dir(select: Boolean, dir: Path): List[(String, Info)] =
    1.16 @@ -655,11 +661,9 @@
    1.17        else Nil
    1.18      }
    1.19  
    1.20 -    val default_dirs = Isabelle_System.components().filter(is_session_dir(_))
    1.21 -
    1.22      make(
    1.23        for {
    1.24 -        (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
    1.25 +        (select, dir) <- directories(dirs, select_dirs)
    1.26          info <- load_dir(select, check_session_dir(dir))
    1.27        } yield info)
    1.28    }
     2.1 --- a/src/Pure/Tools/imports.scala	Sun Apr 23 18:12:42 2017 +0200
     2.2 +++ b/src/Pure/Tools/imports.scala	Sun Apr 23 18:47:56 2017 +0200
     2.3 @@ -12,6 +12,23 @@
     2.4  
     2.5  object Imports
     2.6  {
     2.7 +  /* manifest */
     2.8 +
     2.9 +  def manifest_files(start: Path, pred: JFile => Boolean = _ => true): List[JFile] =
    2.10 +    Mercurial.find_repository(start) match {
    2.11 +      case None =>
    2.12 +        Output.warning("Ignoring directory " + quote(start.toString) + " (no Mercurial repository)")
    2.13 +        Nil
    2.14 +      case Some(hg) =>
    2.15 +        val start_path = start.file.getCanonicalFile.toPath
    2.16 +        for {
    2.17 +          name <- hg.manifest()
    2.18 +          file = (hg.root + Path.explode(name)).file
    2.19 +          if pred(file) && file.getCanonicalFile.toPath.startsWith(start_path)
    2.20 +        } yield file
    2.21 +    }
    2.22 +
    2.23 +
    2.24    /* update imports */
    2.25  
    2.26    sealed case class Update(range: Text.Range, old_text: String, new_text: String)
    2.27 @@ -81,8 +98,12 @@
    2.28      }
    2.29    }
    2.30  
    2.31 +
    2.32 +  /* collective operations */
    2.33 +
    2.34    def imports(
    2.35      options: Options,
    2.36 +    operation_manifest: Boolean = false,
    2.37      operation_update: Boolean = false,
    2.38      progress: Progress = No_Progress,
    2.39      selection: Sessions.Selection = Sessions.Selection.empty,
    2.40 @@ -95,7 +116,19 @@
    2.41  
    2.42      val deps =
    2.43        Sessions.deps(selected_sessions, progress = progress, verbose = verbose,
    2.44 -        global_theories = full_sessions.global_theories)
    2.45 +        global_theories = full_sessions.global_theories,
    2.46 +        all_known = true)
    2.47 +
    2.48 +    if (operation_manifest) {
    2.49 +      progress.echo("\nManifest check:")
    2.50 +      val unused_files =
    2.51 +        for {
    2.52 +          (_, dir) <- Sessions.directories(dirs, select_dirs)
    2.53 +          file <- manifest_files(dir, file => file.getName.endsWith(".thy"))
    2.54 +          if deps.all_known.get_file(file).isEmpty
    2.55 +        } yield file
    2.56 +      unused_files.foreach(file => progress.echo("unused file " + quote(file.toString)))
    2.57 +    }
    2.58  
    2.59      if (operation_update) {
    2.60        val updates =
    2.61 @@ -156,6 +189,7 @@
    2.62      Isabelle_Tool("imports", "maintain theory imports wrt. session structure", args =>
    2.63      {
    2.64        var select_dirs: List[Path] = Nil
    2.65 +      var operation_manifest = false
    2.66        var requirements = false
    2.67        var operation_update = false
    2.68        var exclude_session_groups: List[String] = Nil
    2.69 @@ -171,6 +205,7 @@
    2.70  
    2.71    Options are:
    2.72      -D DIR       include session directory and select its sessions
    2.73 +    -M           operation: Mercurial manifest check for imported theory files
    2.74      -R           operate on requirements of selected sessions
    2.75      -U           operation: update theory imports to use session qualifiers
    2.76      -X NAME      exclude sessions from group NAME and all descendants
    2.77 @@ -185,6 +220,7 @@
    2.78    needs to be specified (see option -U).
    2.79  """,
    2.80        "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
    2.81 +      "M" -> (_ => operation_manifest = true),
    2.82        "R" -> (_ => requirements = true),
    2.83        "U" -> (_ => operation_update = true),
    2.84        "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
    2.85 @@ -196,7 +232,8 @@
    2.86        "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
    2.87  
    2.88        val sessions = getopts(args)
    2.89 -      if (args.isEmpty || !operation_update) getopts.usage()
    2.90 +      if (args.isEmpty || !(operation_manifest || operation_update))
    2.91 +        getopts.usage()
    2.92  
    2.93        val selection =
    2.94          Sessions.Selection(requirements, all_sessions, exclude_session_groups,
    2.95 @@ -204,7 +241,8 @@
    2.96  
    2.97        val progress = new Console_Progress(verbose = verbose)
    2.98  
    2.99 -      imports(options, operation_update = operation_update, progress = progress,
   2.100 -        selection = selection, dirs = dirs, select_dirs = select_dirs, verbose = verbose)
   2.101 +      imports(options, operation_manifest = operation_manifest, operation_update = operation_update,
   2.102 +        progress = progress, selection = selection, dirs = dirs, select_dirs = select_dirs,
   2.103 +        verbose = verbose)
   2.104      })
   2.105  }