src/Pure/Tools/imports.scala
author wenzelm
Tue Nov 07 16:50:26 2017 +0100 (20 months ago)
changeset 67026 687c822ee5e3
parent 67025 961285f581e6
child 68204 a554da2811f2
permissions -rw-r--r--
tuned 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@67025
   103
    val selected_sessions = full_sessions.selection(selection)
wenzelm@65558
   104
wenzelm@65558
   105
    val deps =
wenzelm@66962
   106
      Sessions.deps(selected_sessions, full_sessions.global_theories,
wenzelm@66962
   107
        progress = progress, verbose = verbose).check_errors
wenzelm@65561
   108
wenzelm@65566
   109
    val root_keywords = Sessions.root_syntax.keywords
wenzelm@65566
   110
wenzelm@65566
   111
    if (operation_imports) {
wenzelm@67025
   112
      val report_imports: List[Report] =
wenzelm@67025
   113
        selected_sessions.build_topological_order.map((session_name: String) =>
wenzelm@67025
   114
          {
wenzelm@67025
   115
            val info = selected_sessions(session_name)
wenzelm@67025
   116
            val session_base = deps(session_name)
wenzelm@65566
   117
wenzelm@67025
   118
            val declared_imports =
wenzelm@67025
   119
              selected_sessions.imports_requirements(List(session_name)).toSet
wenzelm@66851
   120
wenzelm@67025
   121
            val extra_imports =
wenzelm@67025
   122
              (for {
wenzelm@67025
   123
                (_, a) <- session_base.known.theories.iterator
wenzelm@67025
   124
                if session_base.theory_qualifier(a) == info.name
wenzelm@67025
   125
                b <- deps.all_known.get_file(a.path.file)
wenzelm@67025
   126
                qualifier = session_base.theory_qualifier(b)
wenzelm@67025
   127
                if !declared_imports.contains(qualifier)
wenzelm@67025
   128
              } yield qualifier).toSet
wenzelm@65566
   129
wenzelm@67025
   130
            val loaded_imports =
wenzelm@67025
   131
              selected_sessions.imports_requirements(
wenzelm@67025
   132
                session_base.loaded_theories.keys.map(a =>
wenzelm@67025
   133
                  session_base.theory_qualifier(session_base.known.theories(a))))
wenzelm@67025
   134
              .toSet - session_name
wenzelm@66851
   135
wenzelm@67025
   136
            val minimal_imports =
wenzelm@67025
   137
              loaded_imports.filter(s1 =>
wenzelm@67025
   138
                !loaded_imports.exists(s2 => selected_sessions.imports_graph.is_edge(s1, s2)))
wenzelm@66851
   139
wenzelm@67025
   140
            def make_result(set: Set[String]): Option[List[String]] =
wenzelm@67025
   141
              if (set.isEmpty) None
wenzelm@67025
   142
              else Some(selected_sessions.imports_topological_order.filter(set))
wenzelm@66851
   143
wenzelm@67025
   144
            Report(info, declared_imports, make_result(extra_imports),
wenzelm@67025
   145
              if (loaded_imports == declared_imports - session_name) None
wenzelm@67025
   146
              else make_result(minimal_imports))
wenzelm@67025
   147
          })
wenzelm@66851
   148
wenzelm@66851
   149
      progress.echo("\nPotential session imports:")
wenzelm@66851
   150
      for {
wenzelm@66851
   151
        report <- report_imports.sortBy(_.declared_imports.size)
wenzelm@66851
   152
        potential_imports <- report.potential_imports
wenzelm@66851
   153
      } progress.echo(report.print(root_keywords, potential_imports))
wenzelm@66851
   154
wenzelm@66851
   155
      progress.echo("\nActual session imports:")
wenzelm@66851
   156
      for {
wenzelm@66851
   157
        report <- report_imports
wenzelm@66851
   158
        actual_imports <- report.actual_imports
wenzelm@66851
   159
      } progress.echo(report.print(root_keywords, actual_imports))
wenzelm@65566
   160
    }
wenzelm@65566
   161
wenzelm@65824
   162
    if (operation_repository_files) {
wenzelm@66671
   163
      progress.echo("\nMercurial repository check:")
wenzelm@65561
   164
      val unused_files =
wenzelm@65561
   165
        for {
wenzelm@65561
   166
          (_, dir) <- Sessions.directories(dirs, select_dirs)
wenzelm@65830
   167
          file <- repository_files(progress, dir, file => file.getName.endsWith(".thy"))
wenzelm@65561
   168
          if deps.all_known.get_file(file).isEmpty
wenzelm@65561
   169
        } yield file
wenzelm@65561
   170
      unused_files.foreach(file => progress.echo("unused file " + quote(file.toString)))
wenzelm@65561
   171
    }
wenzelm@65558
   172
wenzelm@65558
   173
    if (operation_update) {
wenzelm@66449
   174
      progress.echo("\nUpdate theory imports" + update_message + ":")
wenzelm@65558
   175
      val updates =
wenzelm@67025
   176
        selected_sessions.build_topological_order.flatMap(session_name =>
wenzelm@67025
   177
          {
wenzelm@67025
   178
            val info = selected_sessions(session_name)
wenzelm@67025
   179
            val session_base = deps(session_name)
wenzelm@67025
   180
            val session_resources = new Resources(session_base)
wenzelm@67025
   181
            val imports_base = session_base.get_imports
wenzelm@67025
   182
            val imports_resources = new Resources(imports_base)
wenzelm@65558
   183
wenzelm@67025
   184
            def standard_import(qualifier: String, dir: String, s: String): String =
wenzelm@67025
   185
              imports_resources.standard_import(session_base, qualifier, dir, s)
wenzelm@65558
   186
wenzelm@67025
   187
            val updates_root =
wenzelm@67025
   188
              for {
wenzelm@67025
   189
                (_, pos) <- info.theories.flatMap(_._2)
wenzelm@67025
   190
                upd <- update_name(root_keywords, pos, standard_import(info.name, info.dir.implode, _))
wenzelm@67025
   191
              } yield upd
wenzelm@65558
   192
wenzelm@67025
   193
            val updates_theories =
wenzelm@67025
   194
              for {
wenzelm@67025
   195
                (_, name) <- session_base.known.theories_local.toList
wenzelm@67025
   196
                if session_base.theory_qualifier(name) == info.name
wenzelm@67025
   197
                (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
wenzelm@67025
   198
                upd <- update_name(session_base.overall_syntax.keywords, pos,
wenzelm@67025
   199
                  standard_import(session_base.theory_qualifier(name), name.master_dir, _))
wenzelm@67025
   200
              } yield upd
wenzelm@65558
   201
wenzelm@67025
   202
            updates_root ::: updates_theories
wenzelm@67025
   203
          })
wenzelm@65564
   204
wenzelm@65564
   205
      val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _)
wenzelm@65564
   206
      val conflicts =
wenzelm@65564
   207
        file_updates.iterator_list.flatMap({ case (file, upds) =>
wenzelm@65564
   208
          Library.duplicates(upds.sortBy(_.range.start),
wenzelm@65564
   209
            (x: Update, y: Update) => x.range overlaps y.range) match
wenzelm@65564
   210
          {
wenzelm@65564
   211
            case Nil => None
wenzelm@65564
   212
            case bad => Some((file, bad))
wenzelm@65564
   213
          }
wenzelm@65564
   214
        })
wenzelm@65564
   215
      if (conflicts.nonEmpty)
wenzelm@65564
   216
        error(cat_lines(
wenzelm@65564
   217
          conflicts.map({ case (file, bad) =>
wenzelm@65564
   218
            "Conflicting updates for file " + file + bad.mkString("\n  ", "\n  ", "") })))
wenzelm@65564
   219
wenzelm@65566
   220
      for ((file, upds) <- file_updates.iterator_list.toList.sortBy(p => p._1.toString)) {
wenzelm@65564
   221
        progress.echo("file " + quote(file.toString))
wenzelm@65564
   222
        val edits =
wenzelm@65564
   223
          upds.sortBy(upd => - upd.range.start).flatMap(upd =>
wenzelm@65564
   224
            Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text))
wenzelm@65564
   225
        val new_text =
wenzelm@65564
   226
          (File.read(file) /: edits)({ case (text, edit) =>
wenzelm@65564
   227
            edit.edit(text, 0) match {
wenzelm@65564
   228
              case (None, text1) => text1
wenzelm@65564
   229
              case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file)
wenzelm@65564
   230
            }
wenzelm@65564
   231
          })
wenzelm@65564
   232
        File.write_backup2(Path.explode(File.standard_path(file)), new_text)
wenzelm@65564
   233
      }
wenzelm@65558
   234
    }
wenzelm@65558
   235
  }
wenzelm@65558
   236
wenzelm@65518
   237
wenzelm@65518
   238
  /* Isabelle tool wrapper */
wenzelm@65518
   239
wenzelm@65518
   240
  val isabelle_tool =
wenzelm@65557
   241
    Isabelle_Tool("imports", "maintain theory imports wrt. session structure", args =>
wenzelm@65518
   242
    {
wenzelm@66737
   243
      var base_sessions: List[String] = Nil
wenzelm@65518
   244
      var select_dirs: List[Path] = Nil
wenzelm@65566
   245
      var operation_imports = false
wenzelm@65824
   246
      var operation_repository_files = false
wenzelm@65518
   247
      var requirements = false
wenzelm@65558
   248
      var operation_update = false
wenzelm@65518
   249
      var exclude_session_groups: List[String] = Nil
wenzelm@65518
   250
      var all_sessions = false
wenzelm@65518
   251
      var dirs: List[Path] = Nil
wenzelm@65518
   252
      var session_groups: List[String] = Nil
wenzelm@66449
   253
      var incremental_update = false
wenzelm@65518
   254
      var options = Options.init()
wenzelm@65518
   255
      var verbose = false
wenzelm@65518
   256
      var exclude_sessions: List[String] = Nil
wenzelm@65518
   257
wenzelm@65518
   258
      val getopts = Getopts("""
wenzelm@65557
   259
Usage: isabelle imports [OPTIONS] [SESSIONS ...]
wenzelm@65518
   260
wenzelm@65518
   261
  Options are:
wenzelm@66737
   262
    -B NAME      include session NAME and all descendants
wenzelm@65518
   263
    -D DIR       include session directory and select its sessions
wenzelm@66851
   264
    -I           operation: report session imports
wenzelm@66671
   265
    -M           operation: Mercurial repository check for theory files
wenzelm@65518
   266
    -R           operate on requirements of selected sessions
wenzelm@65558
   267
    -U           operation: update theory imports to use session qualifiers
wenzelm@65518
   268
    -X NAME      exclude sessions from group NAME and all descendants
wenzelm@65518
   269
    -a           select all sessions
wenzelm@65518
   270
    -d DIR       include session directory
wenzelm@65518
   271
    -g NAME      select session group NAME
wenzelm@66449
   272
    -i           incremental update according to session graph structure
wenzelm@65518
   273
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
wenzelm@65518
   274
    -v           verbose
wenzelm@65518
   275
    -x NAME      exclude session NAME and all descendants
wenzelm@65518
   276
wenzelm@65558
   277
  Maintain theory imports wrt. session structure. At least one operation
wenzelm@65566
   278
  needs to be specified (see options -I -M -U).
wenzelm@65518
   279
""",
wenzelm@66737
   280
      "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
wenzelm@65518
   281
      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
wenzelm@65566
   282
      "I" -> (_ => operation_imports = true),
wenzelm@65824
   283
      "M" -> (_ => operation_repository_files = true),
wenzelm@65518
   284
      "R" -> (_ => requirements = true),
wenzelm@65558
   285
      "U" -> (_ => operation_update = true),
wenzelm@65518
   286
      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
wenzelm@65518
   287
      "a" -> (_ => all_sessions = true),
wenzelm@65518
   288
      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
wenzelm@65518
   289
      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
wenzelm@66449
   290
      "i" -> (_ => incremental_update = true),
wenzelm@65518
   291
      "o:" -> (arg => options = options + arg),
wenzelm@65518
   292
      "v" -> (_ => verbose = true),
wenzelm@65518
   293
      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
wenzelm@65518
   294
wenzelm@65518
   295
      val sessions = getopts(args)
wenzelm@65824
   296
      if (args.isEmpty || !(operation_imports || operation_repository_files || operation_update))
wenzelm@65561
   297
        getopts.usage()
wenzelm@65518
   298
wenzelm@65518
   299
      val selection =
wenzelm@66737
   300
        Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
wenzelm@65518
   301
          exclude_sessions, session_groups, sessions)
wenzelm@65518
   302
wenzelm@65518
   303
      val progress = new Console_Progress(verbose = verbose)
wenzelm@65518
   304
wenzelm@66449
   305
      if (operation_imports || operation_repository_files ||
wenzelm@66449
   306
          operation_update && !incremental_update)
wenzelm@66449
   307
      {
wenzelm@66449
   308
        imports(options, operation_imports = operation_imports,
wenzelm@66449
   309
          operation_repository_files = operation_repository_files,
wenzelm@66449
   310
          operation_update = operation_update,
wenzelm@66449
   311
          progress = progress, selection = selection, dirs = dirs, select_dirs = select_dirs,
wenzelm@66449
   312
          verbose = verbose)
wenzelm@66449
   313
      }
wenzelm@66449
   314
      else if (operation_update && incremental_update) {
wenzelm@67026
   315
        Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs).
wenzelm@67026
   316
          selection(selection).imports_topological_order.foreach(name =>
wenzelm@67025
   317
            {
wenzelm@67025
   318
              imports(options, operation_update = operation_update, progress = progress,
wenzelm@67025
   319
                update_message = " for session " + quote(name),
wenzelm@67025
   320
                selection = Sessions.Selection(sessions = List(name)),
wenzelm@67025
   321
                dirs = dirs ::: select_dirs, verbose = verbose)
wenzelm@67025
   322
            })
wenzelm@66449
   323
      }
wenzelm@65518
   324
    })
wenzelm@65518
   325
}