src/Pure/Tools/imports.scala
author wenzelm
Thu Aug 17 21:12:55 2017 +0200 (22 months ago)
changeset 66449 1be102db1598
parent 66234 836898197296
child 66571 0fdeb24e535e
permissions -rw-r--r--
support for incremental update according to session graph structure;
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@65518
    33
  /* update imports */
wenzelm@65518
    34
wenzelm@65526
    35
  sealed case class Update(range: Text.Range, old_text: String, new_text: String)
wenzelm@65526
    36
  {
wenzelm@65526
    37
    def edits: List[Text.Edit] =
wenzelm@65526
    38
      Text.Edit.replace(range.start, old_text, new_text)
wenzelm@65526
    39
wenzelm@65526
    40
    override def toString: String =
wenzelm@65526
    41
      range.toString + ": " + old_text + " -> " + new_text
wenzelm@65526
    42
  }
wenzelm@65526
    43
wenzelm@65526
    44
  def update_name(keywords: Keyword.Keywords, pos: Position.T, update: String => String)
wenzelm@65526
    45
    : Option[(JFile, Update)] =
wenzelm@65526
    46
  {
wenzelm@65526
    47
    val file =
wenzelm@65526
    48
      pos match {
wenzelm@65833
    49
        case Position.File(file) => Path.explode(file).canonical_file
wenzelm@65526
    50
        case _ => error("Missing file in position" + Position.here(pos))
wenzelm@65526
    51
      }
wenzelm@65526
    52
wenzelm@65526
    53
    val text = File.read(file)
wenzelm@65526
    54
wenzelm@65526
    55
    val range =
wenzelm@65526
    56
      pos match {
wenzelm@65526
    57
        case Position.Range(symbol_range) => Symbol.Text_Chunk(text).decode(symbol_range)
wenzelm@65526
    58
        case _ => error("Missing range in position" + Position.here(pos))
wenzelm@65526
    59
      }
wenzelm@65526
    60
wenzelm@65526
    61
    Token.read_name(keywords, range.substring(text)) match {
wenzelm@65526
    62
      case Some(tok) =>
wenzelm@65526
    63
        val s1 = tok.source
wenzelm@65526
    64
        val s2 = Token.quote_name(keywords, update(tok.content))
wenzelm@65526
    65
        if (s1 == s2) None else Some((file, Update(range, s1, s2)))
wenzelm@65526
    66
      case None => error("Name token expected" + Position.here(pos))
wenzelm@65526
    67
    }
wenzelm@65526
    68
  }
wenzelm@65526
    69
wenzelm@65561
    70
wenzelm@65561
    71
  /* collective operations */
wenzelm@65561
    72
wenzelm@65558
    73
  def imports(
wenzelm@65558
    74
    options: Options,
wenzelm@65566
    75
    operation_imports: Boolean = false,
wenzelm@65824
    76
    operation_repository_files: Boolean = false,
wenzelm@65558
    77
    operation_update: Boolean = false,
wenzelm@66449
    78
    update_message: String = "",
wenzelm@65558
    79
    progress: Progress = No_Progress,
wenzelm@65558
    80
    selection: Sessions.Selection = Sessions.Selection.empty,
wenzelm@65558
    81
    dirs: List[Path] = Nil,
wenzelm@65558
    82
    select_dirs: List[Path] = Nil,
wenzelm@65558
    83
    verbose: Boolean = false) =
wenzelm@65558
    84
  {
wenzelm@65558
    85
    val full_sessions = Sessions.load(options, dirs, select_dirs)
wenzelm@65558
    86
    val (selected, selected_sessions) = full_sessions.selection(selection)
wenzelm@65558
    87
wenzelm@65558
    88
    val deps =
wenzelm@65558
    89
      Sessions.deps(selected_sessions, progress = progress, verbose = verbose,
wenzelm@65561
    90
        global_theories = full_sessions.global_theories,
wenzelm@65561
    91
        all_known = true)
wenzelm@65561
    92
wenzelm@65566
    93
    val root_keywords = Sessions.root_syntax.keywords
wenzelm@65566
    94
wenzelm@65566
    95
wenzelm@65566
    96
    if (operation_imports) {
wenzelm@65566
    97
      progress.echo("\nPotential session imports:")
wenzelm@66033
    98
      selected.flatMap(session_name =>
wenzelm@65566
    99
      {
wenzelm@65566
   100
        val info = full_sessions(session_name)
wenzelm@65566
   101
        val session_resources = new Resources(deps(session_name))
wenzelm@65566
   102
wenzelm@65566
   103
        val declared_imports =
wenzelm@65566
   104
          full_sessions.imports_ancestors(session_name).toSet + session_name
wenzelm@65566
   105
        val extra_imports =
wenzelm@65566
   106
          (for {
wenzelm@65566
   107
            (_, a) <- session_resources.session_base.known.theories.iterator
wenzelm@65566
   108
            if session_resources.theory_qualifier(a) == info.theory_qualifier
wenzelm@65566
   109
            b <- deps.all_known.get_file(Path.explode(a.node).file)
wenzelm@65566
   110
            qualifier = session_resources.theory_qualifier(b)
wenzelm@65566
   111
            if !declared_imports.contains(qualifier)
wenzelm@65566
   112
          } yield qualifier).toSet
wenzelm@65566
   113
wenzelm@66033
   114
        if (extra_imports.isEmpty) None
wenzelm@66033
   115
        else Some((session_name, extra_imports.toList.sorted, declared_imports.size))
wenzelm@66033
   116
      }).sortBy(_._3).foreach({ case (session_name, extra_imports, _) =>
wenzelm@66033
   117
        progress.echo("session " + Token.quote_name(root_keywords, session_name) + ": " +
wenzelm@66033
   118
          extra_imports.map(Token.quote_name(root_keywords, _)).mkString(" "))
wenzelm@65566
   119
      })
wenzelm@65566
   120
    }
wenzelm@65566
   121
wenzelm@65824
   122
    if (operation_repository_files) {
wenzelm@65824
   123
      progress.echo("\nMercurial files check:")
wenzelm@65561
   124
      val unused_files =
wenzelm@65561
   125
        for {
wenzelm@65561
   126
          (_, dir) <- Sessions.directories(dirs, select_dirs)
wenzelm@65830
   127
          file <- repository_files(progress, dir, file => file.getName.endsWith(".thy"))
wenzelm@65561
   128
          if deps.all_known.get_file(file).isEmpty
wenzelm@65561
   129
        } yield file
wenzelm@65561
   130
      unused_files.foreach(file => progress.echo("unused file " + quote(file.toString)))
wenzelm@65561
   131
    }
wenzelm@65558
   132
wenzelm@65558
   133
    if (operation_update) {
wenzelm@66449
   134
      progress.echo("\nUpdate theory imports" + update_message + ":")
wenzelm@65558
   135
      val updates =
wenzelm@65558
   136
        selected.flatMap(session_name =>
wenzelm@65558
   137
        {
wenzelm@65558
   138
          val info = full_sessions(session_name)
wenzelm@65558
   139
          val session_base = deps(session_name)
wenzelm@65558
   140
          val session_resources = new Resources(session_base)
wenzelm@66028
   141
          val imports_base = session_base.get_imports
wenzelm@66028
   142
          val imports_resources = new Resources(imports_base)
wenzelm@65558
   143
wenzelm@65558
   144
          def standard_import(qualifier: String, dir: String, s: String): String =
wenzelm@65558
   145
          {
wenzelm@65558
   146
            val name = imports_resources.import_name(qualifier, dir, s)
wenzelm@65558
   147
            val s1 =
wenzelm@66029
   148
              if (imports_base.loaded_theory(name)) name.theory
wenzelm@66025
   149
              else {
wenzelm@66028
   150
                imports_base.known.get_file(Path.explode(name.node).file) match {
wenzelm@66025
   151
                  case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
wenzelm@66025
   152
                    name1.theory
wenzelm@66025
   153
                  case Some(name1) if Thy_Header.is_base_name(s) =>
wenzelm@66025
   154
                    name1.theory_base_name
wenzelm@66025
   155
                  case _ => s
wenzelm@66025
   156
                }
wenzelm@65558
   157
              }
wenzelm@65558
   158
            val name2 = imports_resources.import_name(qualifier, dir, s1)
wenzelm@65558
   159
            if (name.node == name2.node) s1 else s
wenzelm@65558
   160
          }
wenzelm@65558
   161
wenzelm@65558
   162
          val updates_root =
wenzelm@65558
   163
            for {
wenzelm@65558
   164
              (_, pos) <- info.theories.flatMap(_._2)
wenzelm@65566
   165
              upd <- update_name(root_keywords, pos,
wenzelm@65558
   166
                standard_import(info.theory_qualifier, info.dir.implode, _))
wenzelm@65558
   167
            } yield upd
wenzelm@65558
   168
wenzelm@65558
   169
          val updates_theories =
wenzelm@65558
   170
            for {
wenzelm@65558
   171
              (_, name) <- session_base.known.theories_local.toList
wenzelm@66030
   172
              if session_resources.theory_qualifier(name) == info.theory_qualifier
wenzelm@65558
   173
              (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
wenzelm@65558
   174
              upd <- update_name(session_base.syntax.keywords, pos,
wenzelm@65558
   175
                standard_import(session_resources.theory_qualifier(name), name.master_dir, _))
wenzelm@65558
   176
            } yield upd
wenzelm@65558
   177
wenzelm@65558
   178
          updates_root ::: updates_theories
wenzelm@65558
   179
        })
wenzelm@65564
   180
wenzelm@65564
   181
      val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _)
wenzelm@65564
   182
      val conflicts =
wenzelm@65564
   183
        file_updates.iterator_list.flatMap({ case (file, upds) =>
wenzelm@65564
   184
          Library.duplicates(upds.sortBy(_.range.start),
wenzelm@65564
   185
            (x: Update, y: Update) => x.range overlaps y.range) match
wenzelm@65564
   186
          {
wenzelm@65564
   187
            case Nil => None
wenzelm@65564
   188
            case bad => Some((file, bad))
wenzelm@65564
   189
          }
wenzelm@65564
   190
        })
wenzelm@65564
   191
      if (conflicts.nonEmpty)
wenzelm@65564
   192
        error(cat_lines(
wenzelm@65564
   193
          conflicts.map({ case (file, bad) =>
wenzelm@65564
   194
            "Conflicting updates for file " + file + bad.mkString("\n  ", "\n  ", "") })))
wenzelm@65564
   195
wenzelm@65566
   196
      for ((file, upds) <- file_updates.iterator_list.toList.sortBy(p => p._1.toString)) {
wenzelm@65564
   197
        progress.echo("file " + quote(file.toString))
wenzelm@65564
   198
        val edits =
wenzelm@65564
   199
          upds.sortBy(upd => - upd.range.start).flatMap(upd =>
wenzelm@65564
   200
            Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text))
wenzelm@65564
   201
        val new_text =
wenzelm@65564
   202
          (File.read(file) /: edits)({ case (text, edit) =>
wenzelm@65564
   203
            edit.edit(text, 0) match {
wenzelm@65564
   204
              case (None, text1) => text1
wenzelm@65564
   205
              case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file)
wenzelm@65564
   206
            }
wenzelm@65564
   207
          })
wenzelm@65564
   208
        File.write_backup2(Path.explode(File.standard_path(file)), new_text)
wenzelm@65564
   209
      }
wenzelm@65558
   210
    }
wenzelm@65558
   211
  }
wenzelm@65558
   212
wenzelm@65518
   213
wenzelm@65518
   214
  /* Isabelle tool wrapper */
wenzelm@65518
   215
wenzelm@65518
   216
  val isabelle_tool =
wenzelm@65557
   217
    Isabelle_Tool("imports", "maintain theory imports wrt. session structure", args =>
wenzelm@65518
   218
    {
wenzelm@65518
   219
      var select_dirs: List[Path] = Nil
wenzelm@65566
   220
      var operation_imports = false
wenzelm@65824
   221
      var operation_repository_files = false
wenzelm@65518
   222
      var requirements = false
wenzelm@65558
   223
      var operation_update = false
wenzelm@65518
   224
      var exclude_session_groups: List[String] = Nil
wenzelm@65518
   225
      var all_sessions = false
wenzelm@65518
   226
      var dirs: List[Path] = Nil
wenzelm@65518
   227
      var session_groups: List[String] = Nil
wenzelm@66449
   228
      var incremental_update = false
wenzelm@65518
   229
      var options = Options.init()
wenzelm@65518
   230
      var verbose = false
wenzelm@65518
   231
      var exclude_sessions: List[String] = Nil
wenzelm@65518
   232
wenzelm@65518
   233
      val getopts = Getopts("""
wenzelm@65557
   234
Usage: isabelle imports [OPTIONS] [SESSIONS ...]
wenzelm@65518
   235
wenzelm@65518
   236
  Options are:
wenzelm@65518
   237
    -D DIR       include session directory and select its sessions
wenzelm@65566
   238
    -I           operation: report potential session imports
wenzelm@65824
   239
    -M           operation: Mercurial files check for imported theory files
wenzelm@65518
   240
    -R           operate on requirements of selected sessions
wenzelm@65558
   241
    -U           operation: update theory imports to use session qualifiers
wenzelm@65518
   242
    -X NAME      exclude sessions from group NAME and all descendants
wenzelm@65518
   243
    -a           select all sessions
wenzelm@65518
   244
    -d DIR       include session directory
wenzelm@65518
   245
    -g NAME      select session group NAME
wenzelm@66449
   246
    -i           incremental update according to session graph structure
wenzelm@65518
   247
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
wenzelm@65518
   248
    -v           verbose
wenzelm@65518
   249
    -x NAME      exclude session NAME and all descendants
wenzelm@65518
   250
wenzelm@65558
   251
  Maintain theory imports wrt. session structure. At least one operation
wenzelm@65566
   252
  needs to be specified (see options -I -M -U).
wenzelm@65518
   253
""",
wenzelm@65518
   254
      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
wenzelm@65566
   255
      "I" -> (_ => operation_imports = true),
wenzelm@65824
   256
      "M" -> (_ => operation_repository_files = true),
wenzelm@65518
   257
      "R" -> (_ => requirements = true),
wenzelm@65558
   258
      "U" -> (_ => operation_update = true),
wenzelm@65518
   259
      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
wenzelm@65518
   260
      "a" -> (_ => all_sessions = true),
wenzelm@65518
   261
      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
wenzelm@65518
   262
      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
wenzelm@66449
   263
      "i" -> (_ => incremental_update = true),
wenzelm@65518
   264
      "o:" -> (arg => options = options + arg),
wenzelm@65518
   265
      "v" -> (_ => verbose = true),
wenzelm@65518
   266
      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
wenzelm@65518
   267
wenzelm@65518
   268
      val sessions = getopts(args)
wenzelm@65824
   269
      if (args.isEmpty || !(operation_imports || operation_repository_files || operation_update))
wenzelm@65561
   270
        getopts.usage()
wenzelm@65518
   271
wenzelm@65518
   272
      val selection =
wenzelm@65518
   273
        Sessions.Selection(requirements, all_sessions, exclude_session_groups,
wenzelm@65518
   274
          exclude_sessions, session_groups, sessions)
wenzelm@65518
   275
wenzelm@65518
   276
      val progress = new Console_Progress(verbose = verbose)
wenzelm@65518
   277
wenzelm@66449
   278
      if (operation_imports || operation_repository_files ||
wenzelm@66449
   279
          operation_update && !incremental_update)
wenzelm@66449
   280
      {
wenzelm@66449
   281
        imports(options, operation_imports = operation_imports,
wenzelm@66449
   282
          operation_repository_files = operation_repository_files,
wenzelm@66449
   283
          operation_update = operation_update,
wenzelm@66449
   284
          progress = progress, selection = selection, dirs = dirs, select_dirs = select_dirs,
wenzelm@66449
   285
          verbose = verbose)
wenzelm@66449
   286
      }
wenzelm@66449
   287
      else if (operation_update && incremental_update) {
wenzelm@66449
   288
        val (selected, selected_sessions) =
wenzelm@66449
   289
          Sessions.load(options, dirs, select_dirs).selection(selection)
wenzelm@66449
   290
        selected_sessions.imports_topological_order.foreach(info =>
wenzelm@66449
   291
        {
wenzelm@66449
   292
          imports(options, operation_update = operation_update, progress = progress,
wenzelm@66449
   293
            update_message = " for session " + quote(info.name),
wenzelm@66449
   294
            selection = Sessions.Selection(sessions = List(info.name)),
wenzelm@66449
   295
            dirs = dirs ::: select_dirs, verbose = verbose)
wenzelm@66449
   296
        })
wenzelm@66449
   297
      }
wenzelm@65518
   298
    })
wenzelm@65518
   299
}