src/Pure/Tools/imports.scala
author wenzelm
Sun, 23 Apr 2017 23:06:50 +0200
changeset 65566 94c514ea2846
parent 65564 5b3cae328a94
child 65824 4ff79bd2b265
permissions -rw-r--r--
support for potential session imports;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
65557
29c69a599743 clarified tool name -- more official status;
wenzelm
parents: 65542
diff changeset
     1
/*  Title:      Pure/Tools/imports.scala
65518
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
     3
65557
29c69a599743 clarified tool name -- more official status;
wenzelm
parents: 65542
diff changeset
     4
Maintain theory imports wrt. session structure.
65518
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
     5
*/
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
     6
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
     7
package isabelle
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
     8
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
     9
65526
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    10
import java.io.{File => JFile}
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    11
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    12
65557
29c69a599743 clarified tool name -- more official status;
wenzelm
parents: 65542
diff changeset
    13
object Imports
65518
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
    14
{
65561
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
    15
  /* manifest */
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
    16
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
    17
  def manifest_files(start: Path, pred: JFile => Boolean = _ => true): List[JFile] =
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
    18
    Mercurial.find_repository(start) match {
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
    19
      case None =>
65564
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
    20
        Output.warning("Ignoring directory " + start + " (no Mercurial repository)")
65561
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
    21
        Nil
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
    22
      case Some(hg) =>
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
    23
        val start_path = start.file.getCanonicalFile.toPath
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
    24
        for {
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
    25
          name <- hg.manifest()
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
    26
          file = (hg.root + Path.explode(name)).file
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
    27
          if pred(file) && file.getCanonicalFile.toPath.startsWith(start_path)
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
    28
        } yield file
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
    29
    }
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
    30
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
    31
65518
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
    32
  /* update imports */
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
    33
65526
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    34
  sealed case class Update(range: Text.Range, old_text: String, new_text: String)
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    35
  {
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    36
    def edits: List[Text.Edit] =
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    37
      Text.Edit.replace(range.start, old_text, new_text)
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    38
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    39
    override def toString: String =
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    40
      range.toString + ": " + old_text + " -> " + new_text
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    41
  }
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    42
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    43
  def update_name(keywords: Keyword.Keywords, pos: Position.T, update: String => String)
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    44
    : Option[(JFile, Update)] =
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    45
  {
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    46
    val file =
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    47
      pos match {
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    48
        case Position.File(file) => Path.explode(file).file.getCanonicalFile
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    49
        case _ => error("Missing file in position" + Position.here(pos))
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    50
      }
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    51
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    52
    val text = File.read(file)
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    53
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    54
    val range =
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    55
      pos match {
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    56
        case Position.Range(symbol_range) => Symbol.Text_Chunk(text).decode(symbol_range)
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    57
        case _ => error("Missing range in position" + Position.here(pos))
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    58
      }
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    59
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    60
    Token.read_name(keywords, range.substring(text)) match {
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    61
      case Some(tok) =>
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    62
        val s1 = tok.source
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    63
        val s2 = Token.quote_name(keywords, update(tok.content))
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    64
        if (s1 == s2) None else Some((file, Update(range, s1, s2)))
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    65
      case None => error("Name token expected" + Position.here(pos))
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    66
    }
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    67
  }
41dda3a292e6 actual update_imports operations;
wenzelm
parents: 65518
diff changeset
    68
65561
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
    69
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
    70
  /* collective operations */
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
    71
65558
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
    72
  def imports(
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
    73
    options: Options,
65566
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
    74
    operation_imports: Boolean = false,
65561
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
    75
    operation_manifest: Boolean = false,
65558
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
    76
    operation_update: Boolean = false,
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
    77
    progress: Progress = No_Progress,
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
    78
    selection: Sessions.Selection = Sessions.Selection.empty,
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
    79
    dirs: List[Path] = Nil,
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
    80
    select_dirs: List[Path] = Nil,
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
    81
    verbose: Boolean = false) =
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
    82
  {
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
    83
    val full_sessions = Sessions.load(options, dirs, select_dirs)
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
    84
    val (selected, selected_sessions) = full_sessions.selection(selection)
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
    85
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
    86
    val deps =
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
    87
      Sessions.deps(selected_sessions, progress = progress, verbose = verbose,
65561
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
    88
        global_theories = full_sessions.global_theories,
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
    89
        all_known = true)
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
    90
65566
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
    91
    val root_keywords = Sessions.root_syntax.keywords
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
    92
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
    93
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
    94
    if (operation_imports) {
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
    95
      progress.echo("\nPotential session imports:")
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
    96
      selected.sorted.foreach(session_name =>
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
    97
      {
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
    98
        val info = full_sessions(session_name)
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
    99
        val session_resources = new Resources(deps(session_name))
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   100
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   101
        val declared_imports =
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   102
          full_sessions.imports_ancestors(session_name).toSet + session_name
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   103
        val extra_imports =
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   104
          (for {
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   105
            (_, a) <- session_resources.session_base.known.theories.iterator
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   106
            if session_resources.theory_qualifier(a) == info.theory_qualifier
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   107
            b <- deps.all_known.get_file(Path.explode(a.node).file)
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   108
            qualifier = session_resources.theory_qualifier(b)
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   109
            if !declared_imports.contains(qualifier)
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   110
          } yield qualifier).toSet
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   111
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   112
        if (extra_imports.nonEmpty) {
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   113
          progress.echo("session " + Token.quote_name(root_keywords, session_name) + ": " +
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   114
            extra_imports.toList.sorted.map(Token.quote_name(root_keywords, _)).mkString(" "))
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   115
        }
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   116
      })
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   117
    }
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   118
65561
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
   119
    if (operation_manifest) {
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
   120
      progress.echo("\nManifest check:")
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
   121
      val unused_files =
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
   122
        for {
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
   123
          (_, dir) <- Sessions.directories(dirs, select_dirs)
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
   124
          file <- manifest_files(dir, file => file.getName.endsWith(".thy"))
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
   125
          if deps.all_known.get_file(file).isEmpty
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
   126
        } yield file
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
   127
      unused_files.foreach(file => progress.echo("unused file " + quote(file.toString)))
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
   128
    }
65558
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   129
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   130
    if (operation_update) {
65564
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   131
      progress.echo("\nUpdate theory imports:")
65558
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   132
      val updates =
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   133
        selected.flatMap(session_name =>
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   134
        {
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   135
          val info = full_sessions(session_name)
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   136
          val session_base = deps(session_name)
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   137
          val session_resources = new Resources(session_base)
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   138
          val imports_resources = new Resources(session_base.get_imports)
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   139
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   140
          def standard_import(qualifier: String, dir: String, s: String): String =
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   141
          {
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   142
            val name = imports_resources.import_name(qualifier, dir, s)
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   143
            val file = Path.explode(name.node).file
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   144
            val s1 =
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   145
              imports_resources.session_base.known.get_file(file) match {
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   146
                case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   147
                  name1.theory
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   148
                case Some(name1) if Thy_Header.is_base_name(s) =>
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   149
                  name1.theory_base_name
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   150
                case _ => s
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   151
              }
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   152
            val name2 = imports_resources.import_name(qualifier, dir, s1)
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   153
            if (name.node == name2.node) s1 else s
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   154
          }
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   155
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   156
          val updates_root =
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   157
            for {
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   158
              (_, pos) <- info.theories.flatMap(_._2)
65566
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   159
              upd <- update_name(root_keywords, pos,
65558
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   160
                standard_import(info.theory_qualifier, info.dir.implode, _))
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   161
            } yield upd
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   162
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   163
          val updates_theories =
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   164
            for {
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   165
              (_, name) <- session_base.known.theories_local.toList
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   166
              (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   167
              upd <- update_name(session_base.syntax.keywords, pos,
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   168
                standard_import(session_resources.theory_qualifier(name), name.master_dir, _))
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   169
            } yield upd
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   170
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   171
          updates_root ::: updates_theories
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   172
        })
65564
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   173
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   174
      val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _)
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   175
      val conflicts =
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   176
        file_updates.iterator_list.flatMap({ case (file, upds) =>
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   177
          Library.duplicates(upds.sortBy(_.range.start),
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   178
            (x: Update, y: Update) => x.range overlaps y.range) match
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   179
          {
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   180
            case Nil => None
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   181
            case bad => Some((file, bad))
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   182
          }
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   183
        })
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   184
      if (conflicts.nonEmpty)
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   185
        error(cat_lines(
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   186
          conflicts.map({ case (file, bad) =>
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   187
            "Conflicting updates for file " + file + bad.mkString("\n  ", "\n  ", "") })))
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   188
65566
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   189
      for ((file, upds) <- file_updates.iterator_list.toList.sortBy(p => p._1.toString)) {
65564
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   190
        progress.echo("file " + quote(file.toString))
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   191
        val edits =
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   192
          upds.sortBy(upd => - upd.range.start).flatMap(upd =>
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   193
            Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text))
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   194
        val new_text =
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   195
          (File.read(file) /: edits)({ case (text, edit) =>
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   196
            edit.edit(text, 0) match {
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   197
              case (None, text1) => text1
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   198
              case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file)
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   199
            }
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   200
          })
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   201
        File.write_backup2(Path.explode(File.standard_path(file)), new_text)
5b3cae328a94 tuned messages;
wenzelm
parents: 65561
diff changeset
   202
      }
65558
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   203
    }
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   204
  }
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   205
65518
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   206
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   207
  /* Isabelle tool wrapper */
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   208
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   209
  val isabelle_tool =
65557
29c69a599743 clarified tool name -- more official status;
wenzelm
parents: 65542
diff changeset
   210
    Isabelle_Tool("imports", "maintain theory imports wrt. session structure", args =>
65518
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   211
    {
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   212
      var select_dirs: List[Path] = Nil
65566
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   213
      var operation_imports = false
65561
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
   214
      var operation_manifest = false
65518
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   215
      var requirements = false
65558
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   216
      var operation_update = false
65518
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   217
      var exclude_session_groups: List[String] = Nil
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   218
      var all_sessions = false
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   219
      var dirs: List[Path] = Nil
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   220
      var session_groups: List[String] = Nil
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   221
      var options = Options.init()
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   222
      var verbose = false
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   223
      var exclude_sessions: List[String] = Nil
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   224
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   225
      val getopts = Getopts("""
65557
29c69a599743 clarified tool name -- more official status;
wenzelm
parents: 65542
diff changeset
   226
Usage: isabelle imports [OPTIONS] [SESSIONS ...]
65518
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   227
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   228
  Options are:
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   229
    -D DIR       include session directory and select its sessions
65566
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   230
    -I           operation: report potential session imports
65561
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
   231
    -M           operation: Mercurial manifest check for imported theory files
65518
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   232
    -R           operate on requirements of selected sessions
65558
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   233
    -U           operation: update theory imports to use session qualifiers
65518
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   234
    -X NAME      exclude sessions from group NAME and all descendants
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   235
    -a           select all sessions
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   236
    -d DIR       include session directory
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   237
    -g NAME      select session group NAME
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   238
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   239
    -v           verbose
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   240
    -x NAME      exclude session NAME and all descendants
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   241
65558
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   242
  Maintain theory imports wrt. session structure. At least one operation
65566
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   243
  needs to be specified (see options -I -M -U).
65518
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   244
""",
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   245
      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
65566
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   246
      "I" -> (_ => operation_imports = true),
65561
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
   247
      "M" -> (_ => operation_manifest = true),
65518
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   248
      "R" -> (_ => requirements = true),
65558
479406635409 support for multiple operations via options;
wenzelm
parents: 65557
diff changeset
   249
      "U" -> (_ => operation_update = true),
65518
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   250
      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   251
      "a" -> (_ => all_sessions = true),
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   252
      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   253
      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   254
      "o:" -> (arg => options = options + arg),
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   255
      "v" -> (_ => verbose = true),
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   256
      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   257
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   258
      val sessions = getopts(args)
65566
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   259
      if (args.isEmpty || !(operation_imports || operation_manifest || operation_update))
65561
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
   260
        getopts.usage()
65518
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   261
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   262
      val selection =
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   263
        Sessions.Selection(requirements, all_sessions, exclude_session_groups,
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   264
          exclude_sessions, session_groups, sessions)
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   265
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   266
      val progress = new Console_Progress(verbose = verbose)
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   267
65566
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   268
      imports(options, operation_imports = operation_imports,
94c514ea2846 support for potential session imports;
wenzelm
parents: 65564
diff changeset
   269
        operation_manifest = operation_manifest, operation_update = operation_update,
65561
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
   270
        progress = progress, selection = selection, dirs = dirs, select_dirs = select_dirs,
741b1d3930c0 support for Mercurial manifest check;
wenzelm
parents: 65558
diff changeset
   271
        verbose = verbose)
65518
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   272
    })
bc8fa59211b7 wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff changeset
   273
}