support for potential session imports;
authorwenzelm
Sun Apr 23 23:06:50 2017 +0200 (2017-04-23)
changeset 6556694c514ea2846
parent 65565 3219a7ed669c
child 65567 c556c09765dd
support for potential session imports;
src/Pure/Thy/sessions.scala
src/Pure/Tools/imports.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Sun Apr 23 22:00:15 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Sun Apr 23 23:06:50 2017 +0200
     1.3 @@ -448,6 +448,9 @@
     1.4      def build_topological_order: List[Info] =
     1.5        build_graph.topological_order.map(apply(_))
     1.6  
     1.7 +    def imports_ancestors(name: String): List[String] =
     1.8 +      imports_graph.all_preds(List(name)).tail.reverse
     1.9 +
    1.10      def imports_topological_order: List[Info] =
    1.11        imports_graph.topological_order.map(apply(_))
    1.12  
     2.1 --- a/src/Pure/Tools/imports.scala	Sun Apr 23 22:00:15 2017 +0200
     2.2 +++ b/src/Pure/Tools/imports.scala	Sun Apr 23 23:06:50 2017 +0200
     2.3 @@ -71,6 +71,7 @@
     2.4  
     2.5    def imports(
     2.6      options: Options,
     2.7 +    operation_imports: Boolean = false,
     2.8      operation_manifest: Boolean = false,
     2.9      operation_update: Boolean = false,
    2.10      progress: Progress = No_Progress,
    2.11 @@ -87,6 +88,34 @@
    2.12          global_theories = full_sessions.global_theories,
    2.13          all_known = true)
    2.14  
    2.15 +    val root_keywords = Sessions.root_syntax.keywords
    2.16 +
    2.17 +
    2.18 +    if (operation_imports) {
    2.19 +      progress.echo("\nPotential session imports:")
    2.20 +      selected.sorted.foreach(session_name =>
    2.21 +      {
    2.22 +        val info = full_sessions(session_name)
    2.23 +        val session_resources = new Resources(deps(session_name))
    2.24 +
    2.25 +        val declared_imports =
    2.26 +          full_sessions.imports_ancestors(session_name).toSet + session_name
    2.27 +        val extra_imports =
    2.28 +          (for {
    2.29 +            (_, a) <- session_resources.session_base.known.theories.iterator
    2.30 +            if session_resources.theory_qualifier(a) == info.theory_qualifier
    2.31 +            b <- deps.all_known.get_file(Path.explode(a.node).file)
    2.32 +            qualifier = session_resources.theory_qualifier(b)
    2.33 +            if !declared_imports.contains(qualifier)
    2.34 +          } yield qualifier).toSet
    2.35 +
    2.36 +        if (extra_imports.nonEmpty) {
    2.37 +          progress.echo("session " + Token.quote_name(root_keywords, session_name) + ": " +
    2.38 +            extra_imports.toList.sorted.map(Token.quote_name(root_keywords, _)).mkString(" "))
    2.39 +        }
    2.40 +      })
    2.41 +    }
    2.42 +
    2.43      if (operation_manifest) {
    2.44        progress.echo("\nManifest check:")
    2.45        val unused_files =
    2.46 @@ -108,12 +137,6 @@
    2.47            val session_resources = new Resources(session_base)
    2.48            val imports_resources = new Resources(session_base.get_imports)
    2.49  
    2.50 -          val local_theories =
    2.51 -            (for {
    2.52 -              (_, name) <- session_base.known.theories_local.iterator
    2.53 -              if session_resources.theory_qualifier(name) == info.theory_qualifier
    2.54 -            } yield name).toSet
    2.55 -
    2.56            def standard_import(qualifier: String, dir: String, s: String): String =
    2.57            {
    2.58              val name = imports_resources.import_name(qualifier, dir, s)
    2.59 @@ -133,7 +156,7 @@
    2.60            val updates_root =
    2.61              for {
    2.62                (_, pos) <- info.theories.flatMap(_._2)
    2.63 -              upd <- update_name(Sessions.root_syntax.keywords, pos,
    2.64 +              upd <- update_name(root_keywords, pos,
    2.65                  standard_import(info.theory_qualifier, info.dir.implode, _))
    2.66              } yield upd
    2.67  
    2.68 @@ -163,7 +186,7 @@
    2.69            conflicts.map({ case (file, bad) =>
    2.70              "Conflicting updates for file " + file + bad.mkString("\n  ", "\n  ", "") })))
    2.71  
    2.72 -      for ((file, upds) <- file_updates.iterator_list) {
    2.73 +      for ((file, upds) <- file_updates.iterator_list.toList.sortBy(p => p._1.toString)) {
    2.74          progress.echo("file " + quote(file.toString))
    2.75          val edits =
    2.76            upds.sortBy(upd => - upd.range.start).flatMap(upd =>
    2.77 @@ -187,6 +210,7 @@
    2.78      Isabelle_Tool("imports", "maintain theory imports wrt. session structure", args =>
    2.79      {
    2.80        var select_dirs: List[Path] = Nil
    2.81 +      var operation_imports = false
    2.82        var operation_manifest = false
    2.83        var requirements = false
    2.84        var operation_update = false
    2.85 @@ -203,6 +227,7 @@
    2.86  
    2.87    Options are:
    2.88      -D DIR       include session directory and select its sessions
    2.89 +    -I           operation: report potential session imports
    2.90      -M           operation: Mercurial manifest check for imported theory files
    2.91      -R           operate on requirements of selected sessions
    2.92      -U           operation: update theory imports to use session qualifiers
    2.93 @@ -215,9 +240,10 @@
    2.94      -x NAME      exclude session NAME and all descendants
    2.95  
    2.96    Maintain theory imports wrt. session structure. At least one operation
    2.97 -  needs to be specified (see option -U).
    2.98 +  needs to be specified (see options -I -M -U).
    2.99  """,
   2.100        "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
   2.101 +      "I" -> (_ => operation_imports = true),
   2.102        "M" -> (_ => operation_manifest = true),
   2.103        "R" -> (_ => requirements = true),
   2.104        "U" -> (_ => operation_update = true),
   2.105 @@ -230,7 +256,7 @@
   2.106        "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
   2.107  
   2.108        val sessions = getopts(args)
   2.109 -      if (args.isEmpty || !(operation_manifest || operation_update))
   2.110 +      if (args.isEmpty || !(operation_imports || operation_manifest || operation_update))
   2.111          getopts.usage()
   2.112  
   2.113        val selection =
   2.114 @@ -239,7 +265,8 @@
   2.115  
   2.116        val progress = new Console_Progress(verbose = verbose)
   2.117  
   2.118 -      imports(options, operation_manifest = operation_manifest, operation_update = operation_update,
   2.119 +      imports(options, operation_imports = operation_imports,
   2.120 +        operation_manifest = operation_manifest, operation_update = operation_update,
   2.121          progress = progress, selection = selection, dirs = dirs, select_dirs = select_dirs,
   2.122          verbose = verbose)
   2.123      })