src/Pure/Tools/imports.scala
changeset 65566 94c514ea2846
parent 65564 5b3cae328a94
child 65824 4ff79bd2b265
     1.1 --- a/src/Pure/Tools/imports.scala	Sun Apr 23 22:00:15 2017 +0200
     1.2 +++ b/src/Pure/Tools/imports.scala	Sun Apr 23 23:06:50 2017 +0200
     1.3 @@ -71,6 +71,7 @@
     1.4  
     1.5    def imports(
     1.6      options: Options,
     1.7 +    operation_imports: Boolean = false,
     1.8      operation_manifest: Boolean = false,
     1.9      operation_update: Boolean = false,
    1.10      progress: Progress = No_Progress,
    1.11 @@ -87,6 +88,34 @@
    1.12          global_theories = full_sessions.global_theories,
    1.13          all_known = true)
    1.14  
    1.15 +    val root_keywords = Sessions.root_syntax.keywords
    1.16 +
    1.17 +
    1.18 +    if (operation_imports) {
    1.19 +      progress.echo("\nPotential session imports:")
    1.20 +      selected.sorted.foreach(session_name =>
    1.21 +      {
    1.22 +        val info = full_sessions(session_name)
    1.23 +        val session_resources = new Resources(deps(session_name))
    1.24 +
    1.25 +        val declared_imports =
    1.26 +          full_sessions.imports_ancestors(session_name).toSet + session_name
    1.27 +        val extra_imports =
    1.28 +          (for {
    1.29 +            (_, a) <- session_resources.session_base.known.theories.iterator
    1.30 +            if session_resources.theory_qualifier(a) == info.theory_qualifier
    1.31 +            b <- deps.all_known.get_file(Path.explode(a.node).file)
    1.32 +            qualifier = session_resources.theory_qualifier(b)
    1.33 +            if !declared_imports.contains(qualifier)
    1.34 +          } yield qualifier).toSet
    1.35 +
    1.36 +        if (extra_imports.nonEmpty) {
    1.37 +          progress.echo("session " + Token.quote_name(root_keywords, session_name) + ": " +
    1.38 +            extra_imports.toList.sorted.map(Token.quote_name(root_keywords, _)).mkString(" "))
    1.39 +        }
    1.40 +      })
    1.41 +    }
    1.42 +
    1.43      if (operation_manifest) {
    1.44        progress.echo("\nManifest check:")
    1.45        val unused_files =
    1.46 @@ -108,12 +137,6 @@
    1.47            val session_resources = new Resources(session_base)
    1.48            val imports_resources = new Resources(session_base.get_imports)
    1.49  
    1.50 -          val local_theories =
    1.51 -            (for {
    1.52 -              (_, name) <- session_base.known.theories_local.iterator
    1.53 -              if session_resources.theory_qualifier(name) == info.theory_qualifier
    1.54 -            } yield name).toSet
    1.55 -
    1.56            def standard_import(qualifier: String, dir: String, s: String): String =
    1.57            {
    1.58              val name = imports_resources.import_name(qualifier, dir, s)
    1.59 @@ -133,7 +156,7 @@
    1.60            val updates_root =
    1.61              for {
    1.62                (_, pos) <- info.theories.flatMap(_._2)
    1.63 -              upd <- update_name(Sessions.root_syntax.keywords, pos,
    1.64 +              upd <- update_name(root_keywords, pos,
    1.65                  standard_import(info.theory_qualifier, info.dir.implode, _))
    1.66              } yield upd
    1.67  
    1.68 @@ -163,7 +186,7 @@
    1.69            conflicts.map({ case (file, bad) =>
    1.70              "Conflicting updates for file " + file + bad.mkString("\n  ", "\n  ", "") })))
    1.71  
    1.72 -      for ((file, upds) <- file_updates.iterator_list) {
    1.73 +      for ((file, upds) <- file_updates.iterator_list.toList.sortBy(p => p._1.toString)) {
    1.74          progress.echo("file " + quote(file.toString))
    1.75          val edits =
    1.76            upds.sortBy(upd => - upd.range.start).flatMap(upd =>
    1.77 @@ -187,6 +210,7 @@
    1.78      Isabelle_Tool("imports", "maintain theory imports wrt. session structure", args =>
    1.79      {
    1.80        var select_dirs: List[Path] = Nil
    1.81 +      var operation_imports = false
    1.82        var operation_manifest = false
    1.83        var requirements = false
    1.84        var operation_update = false
    1.85 @@ -203,6 +227,7 @@
    1.86  
    1.87    Options are:
    1.88      -D DIR       include session directory and select its sessions
    1.89 +    -I           operation: report potential session imports
    1.90      -M           operation: Mercurial manifest check for imported theory files
    1.91      -R           operate on requirements of selected sessions
    1.92      -U           operation: update theory imports to use session qualifiers
    1.93 @@ -215,9 +240,10 @@
    1.94      -x NAME      exclude session NAME and all descendants
    1.95  
    1.96    Maintain theory imports wrt. session structure. At least one operation
    1.97 -  needs to be specified (see option -U).
    1.98 +  needs to be specified (see options -I -M -U).
    1.99  """,
   1.100        "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
   1.101 +      "I" -> (_ => operation_imports = true),
   1.102        "M" -> (_ => operation_manifest = true),
   1.103        "R" -> (_ => requirements = true),
   1.104        "U" -> (_ => operation_update = true),
   1.105 @@ -230,7 +256,7 @@
   1.106        "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
   1.107  
   1.108        val sessions = getopts(args)
   1.109 -      if (args.isEmpty || !(operation_manifest || operation_update))
   1.110 +      if (args.isEmpty || !(operation_imports || operation_manifest || operation_update))
   1.111          getopts.usage()
   1.112  
   1.113        val selection =
   1.114 @@ -239,7 +265,8 @@
   1.115  
   1.116        val progress = new Console_Progress(verbose = verbose)
   1.117  
   1.118 -      imports(options, operation_manifest = operation_manifest, operation_update = operation_update,
   1.119 +      imports(options, operation_imports = operation_imports,
   1.120 +        operation_manifest = operation_manifest, operation_update = operation_update,
   1.121          progress = progress, selection = selection, dirs = dirs, select_dirs = select_dirs,
   1.122          verbose = verbose)
   1.123      })