src/Pure/Tools/imports.scala
author wenzelm
Thu May 17 15:38:36 2018 +0200 (13 months ago)
changeset 68204 a554da2811f2
parent 67026 687c822ee5e3
child 68304 09270aa40884
permissions -rw-r--r--
clarified signature;
wenzelm@65557
     1
/*  Title:      Pure/Tools/imports.scala
wenzelm@65518
     2
    Author:     Makarius
wenzelm@65518
     3
wenzelm@65557
     4
Maintain theory imports wrt. session structure.
wenzelm@65518
     5
*/
wenzelm@65518
     6
wenzelm@65518
     7
package isabelle
wenzelm@65518
     8
wenzelm@65518
     9
wenzelm@65526
    10
import java.io.{File => JFile}
wenzelm@65526
    11
wenzelm@65526
    12
wenzelm@65557
    13
object Imports
wenzelm@65518
    14
{
wenzelm@65824
    15
  /* repository files */
wenzelm@65561
    16
wenzelm@65830
    17
  def repository_files(progress: Progress, start: Path, pred: JFile => Boolean = _ => true)
wenzelm@65830
    18
      : List[JFile] =
wenzelm@65561
    19
    Mercurial.find_repository(start) match {
wenzelm@65561
    20
      case None =>
wenzelm@65830
    21
        progress.echo_warning("Ignoring directory " + start + " (no Mercurial repository)")
wenzelm@65561
    22
        Nil
wenzelm@65561
    23
      case Some(hg) =>
wenzelm@65833
    24
        val start_path = start.canonical_file.toPath
wenzelm@65561
    25
        for {
wenzelm@65824
    26
          name <- hg.known_files()
wenzelm@65561
    27
          file = (hg.root + Path.explode(name)).file
wenzelm@66234
    28
          if pred(file) && File.canonical(file).toPath.startsWith(start_path)
wenzelm@65561
    29
        } yield file
wenzelm@65561
    30
    }
wenzelm@65561
    31
wenzelm@65561
    32
wenzelm@66851
    33
  /* report imports */
wenzelm@66851
    34
wenzelm@66851
    35
  sealed case class Report(
wenzelm@66851
    36
    info: Sessions.Info,
wenzelm@66851
    37
    declared_imports: Set[String],
wenzelm@66851
    38
    potential_imports: Option[List[String]],
wenzelm@66851
    39
    actual_imports: Option[List[String]])
wenzelm@66851
    40
  {
wenzelm@66851
    41
    def print(keywords: Keyword.Keywords, result: List[String]): String =
wenzelm@66851
    42
    {
wenzelm@66851
    43
      def print_name(name: String): String = Token.quote_name(keywords, name)
wenzelm@66851
    44
wenzelm@66851
    45
      "  session " + print_name(info.name) + ": " + result.map(print_name(_)).mkString(" ")
wenzelm@66851
    46
    }
wenzelm@66851
    47
  }
wenzelm@66851
    48
wenzelm@66851
    49
wenzelm@65518
    50
  /* update imports */
wenzelm@65518
    51
wenzelm@65526
    52
  sealed case class Update(range: Text.Range, old_text: String, new_text: String)
wenzelm@65526
    53
  {
wenzelm@65526
    54
    def edits: List[Text.Edit] =
wenzelm@65526
    55
      Text.Edit.replace(range.start, old_text, new_text)
wenzelm@65526
    56
wenzelm@65526
    57
    override def toString: String =
wenzelm@65526
    58
      range.toString + ": " + old_text + " -> " + new_text
wenzelm@65526
    59
  }
wenzelm@65526
    60
wenzelm@65526
    61
  def update_name(keywords: Keyword.Keywords, pos: Position.T, update: String => String)
wenzelm@65526
    62
    : Option[(JFile, Update)] =
wenzelm@65526
    63
  {
wenzelm@65526
    64
    val file =
wenzelm@65526
    65
      pos match {
wenzelm@65833
    66
        case Position.File(file) => Path.explode(file).canonical_file
wenzelm@65526
    67
        case _ => error("Missing file in position" + Position.here(pos))
wenzelm@65526
    68
      }
wenzelm@65526
    69
wenzelm@65526
    70
    val text = File.read(file)
wenzelm@65526
    71
wenzelm@65526
    72
    val range =
wenzelm@65526
    73
      pos match {
wenzelm@65526
    74
        case Position.Range(symbol_range) => Symbol.Text_Chunk(text).decode(symbol_range)
wenzelm@65526
    75
        case _ => error("Missing range in position" + Position.here(pos))
wenzelm@65526
    76
      }
wenzelm@65526
    77
wenzelm@65526
    78
    Token.read_name(keywords, range.substring(text)) match {
wenzelm@65526
    79
      case Some(tok) =>
wenzelm@65526
    80
        val s1 = tok.source
wenzelm@65526
    81
        val s2 = Token.quote_name(keywords, update(tok.content))
wenzelm@65526
    82
        if (s1 == s2) None else Some((file, Update(range, s1, s2)))
wenzelm@65526
    83
      case None => error("Name token expected" + Position.here(pos))
wenzelm@65526
    84
    }
wenzelm@65526
    85
  }
wenzelm@65526
    86
wenzelm@65561
    87
wenzelm@65561
    88
  /* collective operations */
wenzelm@65561
    89
wenzelm@65558
    90
  def imports(
wenzelm@65558
    91
    options: Options,
wenzelm@65566
    92
    operation_imports: Boolean = false,
wenzelm@65824
    93
    operation_repository_files: Boolean = false,
wenzelm@65558
    94
    operation_update: Boolean = false,
wenzelm@66449
    95
    update_message: String = "",
wenzelm@65558
    96
    progress: Progress = No_Progress,
wenzelm@65558
    97
    selection: Sessions.Selection = Sessions.Selection.empty,
wenzelm@65558
    98
    dirs: List[Path] = Nil,
wenzelm@65558
    99
    select_dirs: List[Path] = Nil,
wenzelm@65558
   100
    verbose: Boolean = false) =
wenzelm@65558
   101
  {
wenzelm@67026
   102
    val full_sessions = Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs)
wenzelm@65558
   103
wenzelm@65558
   104
    val deps =
wenzelm@68204
   105
      Sessions.deps(full_sessions.selection(selection), full_sessions.global_theories,
wenzelm@66962
   106
        progress = progress, verbose = verbose).check_errors
wenzelm@65561
   107
wenzelm@65566
   108
    val root_keywords = Sessions.root_syntax.keywords
wenzelm@65566
   109
wenzelm@65566
   110
    if (operation_imports) {
wenzelm@67025
   111
      val report_imports: List[Report] =
wenzelm@68204
   112
        deps.sessions_structure.build_topological_order.map((session_name: String) =>
wenzelm@67025
   113
          {
wenzelm@68204
   114
            val info = deps.sessions_structure(session_name)
wenzelm@67025
   115
            val session_base = deps(session_name)
wenzelm@65566
   116
wenzelm@67025
   117
            val declared_imports =
wenzelm@68204
   118
              deps.sessions_structure.imports_requirements(List(session_name)).toSet
wenzelm@66851
   119
wenzelm@67025
   120
            val extra_imports =
wenzelm@67025
   121
              (for {
wenzelm@67025
   122
                (_, a) <- session_base.known.theories.iterator
wenzelm@67025
   123
                if session_base.theory_qualifier(a) == info.name
wenzelm@67025
   124
                b <- deps.all_known.get_file(a.path.file)
wenzelm@67025
   125
                qualifier = session_base.theory_qualifier(b)
wenzelm@67025
   126
                if !declared_imports.contains(qualifier)
wenzelm@67025
   127
              } yield qualifier).toSet
wenzelm@65566
   128
wenzelm@67025
   129
            val loaded_imports =
wenzelm@68204
   130
              deps.sessions_structure.imports_requirements(
wenzelm@67025
   131
                session_base.loaded_theories.keys.map(a =>
wenzelm@67025
   132
                  session_base.theory_qualifier(session_base.known.theories(a))))
wenzelm@67025
   133
              .toSet - session_name
wenzelm@66851
   134
wenzelm@67025
   135
            val minimal_imports =
wenzelm@67025
   136
              loaded_imports.filter(s1 =>
wenzelm@68204
   137
                !loaded_imports.exists(s2 => deps.sessions_structure.imports_graph.is_edge(s1, s2)))
wenzelm@66851
   138
wenzelm@67025
   139
            def make_result(set: Set[String]): Option[List[String]] =
wenzelm@67025
   140
              if (set.isEmpty) None
wenzelm@68204
   141
              else Some(deps.sessions_structure.imports_topological_order.filter(set))
wenzelm@66851
   142
wenzelm@67025
   143
            Report(info, declared_imports, make_result(extra_imports),
wenzelm@67025
   144
              if (loaded_imports == declared_imports - session_name) None
wenzelm@67025
   145
              else make_result(minimal_imports))
wenzelm@67025
   146
          })
wenzelm@66851
   147
wenzelm@66851
   148
      progress.echo("\nPotential session imports:")
wenzelm@66851
   149
      for {
wenzelm@66851
   150
        report <- report_imports.sortBy(_.declared_imports.size)
wenzelm@66851
   151
        potential_imports <- report.potential_imports
wenzelm@66851
   152
      } progress.echo(report.print(root_keywords, potential_imports))
wenzelm@66851
   153
wenzelm@66851
   154
      progress.echo("\nActual session imports:")
wenzelm@66851
   155
      for {
wenzelm@66851
   156
        report <- report_imports
wenzelm@66851
   157
        actual_imports <- report.actual_imports
wenzelm@66851
   158
      } progress.echo(report.print(root_keywords, actual_imports))
wenzelm@65566
   159
    }
wenzelm@65566
   160
wenzelm@65824
   161
    if (operation_repository_files) {
wenzelm@66671
   162
      progress.echo("\nMercurial repository check:")
wenzelm@65561
   163
      val unused_files =
wenzelm@65561
   164
        for {
wenzelm@65561
   165
          (_, dir) <- Sessions.directories(dirs, select_dirs)
wenzelm@65830
   166
          file <- repository_files(progress, dir, file => file.getName.endsWith(".thy"))
wenzelm@65561
   167
          if deps.all_known.get_file(file).isEmpty
wenzelm@65561
   168
        } yield file
wenzelm@65561
   169
      unused_files.foreach(file => progress.echo("unused file " + quote(file.toString)))
wenzelm@65561
   170
    }
wenzelm@65558
   171
wenzelm@65558
   172
    if (operation_update) {
wenzelm@66449
   173
      progress.echo("\nUpdate theory imports" + update_message + ":")
wenzelm@65558
   174
      val updates =
wenzelm@68204
   175
        deps.sessions_structure.build_topological_order.flatMap(session_name =>
wenzelm@67025
   176
          {
wenzelm@68204
   177
            val info = deps.sessions_structure(session_name)
wenzelm@67025
   178
            val session_base = deps(session_name)
wenzelm@67025
   179
            val session_resources = new Resources(session_base)
wenzelm@67025
   180
            val imports_base = session_base.get_imports
wenzelm@67025
   181
            val imports_resources = new Resources(imports_base)
wenzelm@65558
   182
wenzelm@67025
   183
            def standard_import(qualifier: String, dir: String, s: String): String =
wenzelm@67025
   184
              imports_resources.standard_import(session_base, qualifier, dir, s)
wenzelm@65558
   185
wenzelm@67025
   186
            val updates_root =
wenzelm@67025
   187
              for {
wenzelm@67025
   188
                (_, pos) <- info.theories.flatMap(_._2)
wenzelm@67025
   189
                upd <- update_name(root_keywords, pos, standard_import(info.name, info.dir.implode, _))
wenzelm@67025
   190
              } yield upd
wenzelm@65558
   191
wenzelm@67025
   192
            val updates_theories =
wenzelm@67025
   193
              for {
wenzelm@67025
   194
                (_, name) <- session_base.known.theories_local.toList
wenzelm@67025
   195
                if session_base.theory_qualifier(name) == info.name
wenzelm@67025
   196
                (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
wenzelm@67025
   197
                upd <- update_name(session_base.overall_syntax.keywords, pos,
wenzelm@67025
   198
                  standard_import(session_base.theory_qualifier(name), name.master_dir, _))
wenzelm@67025
   199
              } yield upd
wenzelm@65558
   200
wenzelm@67025
   201
            updates_root ::: updates_theories
wenzelm@67025
   202
          })
wenzelm@65564
   203
wenzelm@65564
   204
      val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _)
wenzelm@65564
   205
      val conflicts =
wenzelm@65564
   206
        file_updates.iterator_list.flatMap({ case (file, upds) =>
wenzelm@65564
   207
          Library.duplicates(upds.sortBy(_.range.start),
wenzelm@65564
   208
            (x: Update, y: Update) => x.range overlaps y.range) match
wenzelm@65564
   209
          {
wenzelm@65564
   210
            case Nil => None
wenzelm@65564
   211
            case bad => Some((file, bad))
wenzelm@65564
   212
          }
wenzelm@65564
   213
        })
wenzelm@65564
   214
      if (conflicts.nonEmpty)
wenzelm@65564
   215
        error(cat_lines(
wenzelm@65564
   216
          conflicts.map({ case (file, bad) =>
wenzelm@65564
   217
            "Conflicting updates for file " + file + bad.mkString("\n  ", "\n  ", "") })))
wenzelm@65564
   218
wenzelm@65566
   219
      for ((file, upds) <- file_updates.iterator_list.toList.sortBy(p => p._1.toString)) {
wenzelm@65564
   220
        progress.echo("file " + quote(file.toString))
wenzelm@65564
   221
        val edits =
wenzelm@65564
   222
          upds.sortBy(upd => - upd.range.start).flatMap(upd =>
wenzelm@65564
   223
            Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text))
wenzelm@65564
   224
        val new_text =
wenzelm@65564
   225
          (File.read(file) /: edits)({ case (text, edit) =>
wenzelm@65564
   226
            edit.edit(text, 0) match {
wenzelm@65564
   227
              case (None, text1) => text1
wenzelm@65564
   228
              case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file)
wenzelm@65564
   229
            }
wenzelm@65564
   230
          })
wenzelm@65564
   231
        File.write_backup2(Path.explode(File.standard_path(file)), new_text)
wenzelm@65564
   232
      }
wenzelm@65558
   233
    }
wenzelm@65558
   234
  }
wenzelm@65558
   235
wenzelm@65518
   236
wenzelm@65518
   237
  /* Isabelle tool wrapper */
wenzelm@65518
   238
wenzelm@65518
   239
  val isabelle_tool =
wenzelm@65557
   240
    Isabelle_Tool("imports", "maintain theory imports wrt. session structure", args =>
wenzelm@65518
   241
    {
wenzelm@66737
   242
      var base_sessions: List[String] = Nil
wenzelm@65518
   243
      var select_dirs: List[Path] = Nil
wenzelm@65566
   244
      var operation_imports = false
wenzelm@65824
   245
      var operation_repository_files = false
wenzelm@65518
   246
      var requirements = false
wenzelm@65558
   247
      var operation_update = false
wenzelm@65518
   248
      var exclude_session_groups: List[String] = Nil
wenzelm@65518
   249
      var all_sessions = false
wenzelm@65518
   250
      var dirs: List[Path] = Nil
wenzelm@65518
   251
      var session_groups: List[String] = Nil
wenzelm@66449
   252
      var incremental_update = false
wenzelm@65518
   253
      var options = Options.init()
wenzelm@65518
   254
      var verbose = false
wenzelm@65518
   255
      var exclude_sessions: List[String] = Nil
wenzelm@65518
   256
wenzelm@65518
   257
      val getopts = Getopts("""
wenzelm@65557
   258
Usage: isabelle imports [OPTIONS] [SESSIONS ...]
wenzelm@65518
   259
wenzelm@65518
   260
  Options are:
wenzelm@66737
   261
    -B NAME      include session NAME and all descendants
wenzelm@65518
   262
    -D DIR       include session directory and select its sessions
wenzelm@66851
   263
    -I           operation: report session imports
wenzelm@66671
   264
    -M           operation: Mercurial repository check for theory files
wenzelm@65518
   265
    -R           operate on requirements of selected sessions
wenzelm@65558
   266
    -U           operation: update theory imports to use session qualifiers
wenzelm@65518
   267
    -X NAME      exclude sessions from group NAME and all descendants
wenzelm@65518
   268
    -a           select all sessions
wenzelm@65518
   269
    -d DIR       include session directory
wenzelm@65518
   270
    -g NAME      select session group NAME
wenzelm@66449
   271
    -i           incremental update according to session graph structure
wenzelm@65518
   272
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
wenzelm@65518
   273
    -v           verbose
wenzelm@65518
   274
    -x NAME      exclude session NAME and all descendants
wenzelm@65518
   275
wenzelm@65558
   276
  Maintain theory imports wrt. session structure. At least one operation
wenzelm@65566
   277
  needs to be specified (see options -I -M -U).
wenzelm@65518
   278
""",
wenzelm@66737
   279
      "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
wenzelm@65518
   280
      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
wenzelm@65566
   281
      "I" -> (_ => operation_imports = true),
wenzelm@65824
   282
      "M" -> (_ => operation_repository_files = true),
wenzelm@65518
   283
      "R" -> (_ => requirements = true),
wenzelm@65558
   284
      "U" -> (_ => operation_update = true),
wenzelm@65518
   285
      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
wenzelm@65518
   286
      "a" -> (_ => all_sessions = true),
wenzelm@65518
   287
      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
wenzelm@65518
   288
      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
wenzelm@66449
   289
      "i" -> (_ => incremental_update = true),
wenzelm@65518
   290
      "o:" -> (arg => options = options + arg),
wenzelm@65518
   291
      "v" -> (_ => verbose = true),
wenzelm@65518
   292
      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
wenzelm@65518
   293
wenzelm@65518
   294
      val sessions = getopts(args)
wenzelm@65824
   295
      if (args.isEmpty || !(operation_imports || operation_repository_files || operation_update))
wenzelm@65561
   296
        getopts.usage()
wenzelm@65518
   297
wenzelm@65518
   298
      val selection =
wenzelm@66737
   299
        Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
wenzelm@65518
   300
          exclude_sessions, session_groups, sessions)
wenzelm@65518
   301
wenzelm@65518
   302
      val progress = new Console_Progress(verbose = verbose)
wenzelm@65518
   303
wenzelm@66449
   304
      if (operation_imports || operation_repository_files ||
wenzelm@66449
   305
          operation_update && !incremental_update)
wenzelm@66449
   306
      {
wenzelm@66449
   307
        imports(options, operation_imports = operation_imports,
wenzelm@66449
   308
          operation_repository_files = operation_repository_files,
wenzelm@66449
   309
          operation_update = operation_update,
wenzelm@66449
   310
          progress = progress, selection = selection, dirs = dirs, select_dirs = select_dirs,
wenzelm@66449
   311
          verbose = verbose)
wenzelm@66449
   312
      }
wenzelm@66449
   313
      else if (operation_update && incremental_update) {
wenzelm@67026
   314
        Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs).
wenzelm@67026
   315
          selection(selection).imports_topological_order.foreach(name =>
wenzelm@67025
   316
            {
wenzelm@67025
   317
              imports(options, operation_update = operation_update, progress = progress,
wenzelm@67025
   318
                update_message = " for session " + quote(name),
wenzelm@67025
   319
                selection = Sessions.Selection(sessions = List(name)),
wenzelm@67025
   320
                dirs = dirs ::: select_dirs, verbose = verbose)
wenzelm@67025
   321
            })
wenzelm@66449
   322
      }
wenzelm@65518
   323
    })
wenzelm@65518
   324
}