src/Pure/Tools/update_imports.scala
author wenzelm
Fri Apr 21 14:09:03 2017 +0200 (2017-04-21 ago)
changeset 65532 febfd9f78bd4
parent 65526 41dda3a292e6
child 65533 4a7e794944df
permissions -rw-r--r--
eliminated default_qualifier: just a constant;
wenzelm@65518
     1
/*  Title:      Pure/Tools/update_imports.scala
wenzelm@65518
     2
    Author:     Makarius
wenzelm@65518
     3
wenzelm@65518
     4
Update theory imports to use session qualifiers.
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@65518
    13
object Update_Imports
wenzelm@65518
    14
{
wenzelm@65518
    15
  /* update imports */
wenzelm@65518
    16
wenzelm@65526
    17
  sealed case class Update(range: Text.Range, old_text: String, new_text: String)
wenzelm@65526
    18
  {
wenzelm@65526
    19
    def edits: List[Text.Edit] =
wenzelm@65526
    20
      Text.Edit.replace(range.start, old_text, new_text)
wenzelm@65526
    21
wenzelm@65526
    22
    override def toString: String =
wenzelm@65526
    23
      range.toString + ": " + old_text + " -> " + new_text
wenzelm@65526
    24
  }
wenzelm@65526
    25
wenzelm@65526
    26
  def update_name(keywords: Keyword.Keywords, pos: Position.T, update: String => String)
wenzelm@65526
    27
    : Option[(JFile, Update)] =
wenzelm@65526
    28
  {
wenzelm@65526
    29
    val file =
wenzelm@65526
    30
      pos match {
wenzelm@65526
    31
        case Position.File(file) => Path.explode(file).file.getCanonicalFile
wenzelm@65526
    32
        case _ => error("Missing file in position" + Position.here(pos))
wenzelm@65526
    33
      }
wenzelm@65526
    34
wenzelm@65526
    35
    val text = File.read(file)
wenzelm@65526
    36
wenzelm@65526
    37
    val range =
wenzelm@65526
    38
      pos match {
wenzelm@65526
    39
        case Position.Range(symbol_range) => Symbol.Text_Chunk(text).decode(symbol_range)
wenzelm@65526
    40
        case _ => error("Missing range in position" + Position.here(pos))
wenzelm@65526
    41
      }
wenzelm@65526
    42
wenzelm@65526
    43
    Token.read_name(keywords, range.substring(text)) match {
wenzelm@65526
    44
      case Some(tok) =>
wenzelm@65526
    45
        val s1 = tok.source
wenzelm@65526
    46
        val s2 = Token.quote_name(keywords, update(tok.content))
wenzelm@65526
    47
        if (s1 == s2) None else Some((file, Update(range, s1, s2)))
wenzelm@65526
    48
      case None => error("Name token expected" + Position.here(pos))
wenzelm@65526
    49
    }
wenzelm@65526
    50
  }
wenzelm@65526
    51
wenzelm@65518
    52
  def update_imports(
wenzelm@65518
    53
    options: Options,
wenzelm@65518
    54
    progress: Progress = No_Progress,
wenzelm@65518
    55
    selection: Sessions.Selection = Sessions.Selection.empty,
wenzelm@65518
    56
    dirs: List[Path] = Nil,
wenzelm@65518
    57
    select_dirs: List[Path] = Nil,
wenzelm@65526
    58
    verbose: Boolean = false): List[(JFile, Update)] =
wenzelm@65518
    59
  {
wenzelm@65518
    60
    val full_sessions = Sessions.load(options, dirs, select_dirs)
wenzelm@65518
    61
    val (selected, selected_sessions) = full_sessions.selection(selection)
wenzelm@65526
    62
wenzelm@65518
    63
    val deps =
wenzelm@65518
    64
      Sessions.deps(selected_sessions, progress = progress, verbose = verbose,
wenzelm@65518
    65
        global_theories = full_sessions.global_theories)
wenzelm@65518
    66
wenzelm@65526
    67
    selected.flatMap(session_name =>
wenzelm@65526
    68
    {
wenzelm@65526
    69
      val info = full_sessions(session_name)
wenzelm@65526
    70
      val session_base = deps(session_name)
wenzelm@65532
    71
      val resources = new Resources(session_base)
wenzelm@65526
    72
      val local_theories = session_base.known.theories_local.iterator.map(_._2).toSet
wenzelm@65526
    73
wenzelm@65526
    74
      def standard_import(qualifier: String, s: String): String =
wenzelm@65526
    75
      {
wenzelm@65526
    76
        val name = resources.import_name(qualifier, "", s)
wenzelm@65526
    77
        if (!local_theories.contains(name)) s
wenzelm@65526
    78
        if (resources.theory_qualifier(name) != qualifier) name.theory
wenzelm@65526
    79
        else if (Thy_Header.is_base_name(s)) name.theory_base_name
wenzelm@65526
    80
        else s
wenzelm@65526
    81
      }
wenzelm@65526
    82
wenzelm@65526
    83
      val updates_root =
wenzelm@65526
    84
        for {
wenzelm@65526
    85
          (_, pos) <- info.theories.flatMap(_._2)
wenzelm@65526
    86
          upd <- update_name(Sessions.root_syntax.keywords, pos,
wenzelm@65526
    87
            standard_import(info.theory_qualifier, _))
wenzelm@65526
    88
        } yield upd
wenzelm@65526
    89
wenzelm@65526
    90
      val updates_theories =
wenzelm@65526
    91
        for {
wenzelm@65526
    92
          (_, name) <- session_base.known.theories_local.toList
wenzelm@65526
    93
          (_, pos) <-
wenzelm@65526
    94
            // FIXME proper UTF8 positions for check_thy
wenzelm@65526
    95
            resources.check_thy_reader(name,
wenzelm@65526
    96
              Scan.char_reader(File.read(Path.explode(name.node))),
wenzelm@65526
    97
              Token.Pos.file(name.node)).imports
wenzelm@65526
    98
          upd <- update_name(session_base.syntax.keywords, pos,
wenzelm@65526
    99
            standard_import(resources.theory_qualifier(name), _))
wenzelm@65526
   100
        } yield upd
wenzelm@65526
   101
wenzelm@65526
   102
      updates_root ::: updates_theories
wenzelm@65526
   103
    })
wenzelm@65526
   104
  }
wenzelm@65526
   105
wenzelm@65526
   106
  def apply_updates(updates: List[(JFile, Update)])
wenzelm@65526
   107
  {
wenzelm@65526
   108
    val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _)
wenzelm@65526
   109
    val conflicts =
wenzelm@65526
   110
      file_updates.iterator_list.flatMap({ case (file, upds) =>
wenzelm@65526
   111
        Library.duplicates(upds.sortBy(_.range.start),
wenzelm@65526
   112
          (x: Update, y: Update) => x.range overlaps y.range) match
wenzelm@65526
   113
        {
wenzelm@65526
   114
          case Nil => None
wenzelm@65526
   115
          case bad => Some((file, bad))
wenzelm@65526
   116
        }
wenzelm@65526
   117
      })
wenzelm@65526
   118
    if (conflicts.nonEmpty)
wenzelm@65526
   119
      error(cat_lines(
wenzelm@65526
   120
        conflicts.map({ case (file, bad) =>
wenzelm@65526
   121
          "Conflicting updates for file " + file + bad.mkString("\n  ", "\n  ", "") })))
wenzelm@65526
   122
wenzelm@65526
   123
    for ((file, upds) <- file_updates.iterator_list) {
wenzelm@65526
   124
      val edits =
wenzelm@65526
   125
        upds.sortBy(upd => - upd.range.start).flatMap(upd =>
wenzelm@65526
   126
          Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text))
wenzelm@65526
   127
      val new_text =
wenzelm@65526
   128
        (File.read(file) /: edits)({ case (text, edit) =>
wenzelm@65526
   129
          edit.edit(text, 0) match {
wenzelm@65526
   130
            case (None, text1) => text1
wenzelm@65526
   131
            case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file)
wenzelm@65526
   132
          }
wenzelm@65526
   133
        })
wenzelm@65526
   134
      File.write_backup(Path.explode(File.standard_path(file)), new_text)
wenzelm@65526
   135
    }
wenzelm@65518
   136
  }
wenzelm@65518
   137
wenzelm@65518
   138
wenzelm@65518
   139
  /* Isabelle tool wrapper */
wenzelm@65518
   140
wenzelm@65518
   141
  val isabelle_tool =
wenzelm@65518
   142
    Isabelle_Tool("update_imports", "update theory imports to use session qualifiers", args =>
wenzelm@65518
   143
    {
wenzelm@65518
   144
      var select_dirs: List[Path] = Nil
wenzelm@65518
   145
      var requirements = false
wenzelm@65518
   146
      var exclude_session_groups: List[String] = Nil
wenzelm@65518
   147
      var all_sessions = false
wenzelm@65518
   148
      var dirs: List[Path] = Nil
wenzelm@65518
   149
      var session_groups: List[String] = Nil
wenzelm@65518
   150
      var options = Options.init()
wenzelm@65518
   151
      var verbose = false
wenzelm@65518
   152
      var exclude_sessions: List[String] = Nil
wenzelm@65518
   153
wenzelm@65518
   154
      val getopts = Getopts("""
wenzelm@65518
   155
Usage: isabelle update_imports [OPTIONS] [SESSIONS ...]
wenzelm@65518
   156
wenzelm@65518
   157
  Options are:
wenzelm@65518
   158
    -D DIR       include session directory and select its sessions
wenzelm@65518
   159
    -R           operate on requirements of selected sessions
wenzelm@65518
   160
    -X NAME      exclude sessions from group NAME and all descendants
wenzelm@65518
   161
    -a           select all sessions
wenzelm@65518
   162
    -d DIR       include session directory
wenzelm@65518
   163
    -g NAME      select session group NAME
wenzelm@65518
   164
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
wenzelm@65518
   165
    -v           verbose
wenzelm@65518
   166
    -x NAME      exclude session NAME and all descendants
wenzelm@65518
   167
wenzelm@65518
   168
  Update theory imports to use session qualifiers.
wenzelm@65518
   169
wenzelm@65518
   170
  Old versions of files are preserved by appending "~~".
wenzelm@65518
   171
""",
wenzelm@65518
   172
      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
wenzelm@65518
   173
      "R" -> (_ => requirements = true),
wenzelm@65518
   174
      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
wenzelm@65518
   175
      "a" -> (_ => all_sessions = true),
wenzelm@65518
   176
      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
wenzelm@65518
   177
      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
wenzelm@65518
   178
      "o:" -> (arg => options = options + arg),
wenzelm@65518
   179
      "v" -> (_ => verbose = true),
wenzelm@65518
   180
      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
wenzelm@65518
   181
wenzelm@65518
   182
      val sessions = getopts(args)
wenzelm@65518
   183
      if (args.isEmpty) getopts.usage()
wenzelm@65518
   184
wenzelm@65518
   185
      val selection =
wenzelm@65518
   186
        Sessions.Selection(requirements, all_sessions, exclude_session_groups,
wenzelm@65518
   187
          exclude_sessions, session_groups, sessions)
wenzelm@65518
   188
wenzelm@65518
   189
      val progress = new Console_Progress(verbose = verbose)
wenzelm@65518
   190
wenzelm@65526
   191
      val updates =
wenzelm@65526
   192
        update_imports(options, progress = progress, selection = selection,
wenzelm@65526
   193
          dirs = dirs, select_dirs = select_dirs, verbose = verbose)
wenzelm@65526
   194
wenzelm@65526
   195
      apply_updates(updates)
wenzelm@65518
   196
    })
wenzelm@65518
   197
}