tuned messages;
authorwenzelm
Sun Apr 23 19:17:04 2017 +0200 (2017-04-23)
changeset 655645b3cae328a94
parent 65563 e83c9e94e891
child 65565 3219a7ed669c
tuned messages;
src/Pure/Tools/imports.scala
     1.1 --- a/src/Pure/Tools/imports.scala	Sun Apr 23 19:06:53 2017 +0200
     1.2 +++ b/src/Pure/Tools/imports.scala	Sun Apr 23 19:17:04 2017 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4    def manifest_files(start: Path, pred: JFile => Boolean = _ => true): List[JFile] =
     1.5      Mercurial.find_repository(start) match {
     1.6        case None =>
     1.7 -        Output.warning("Ignoring directory " + quote(start.toString) + " (no Mercurial repository)")
     1.8 +        Output.warning("Ignoring directory " + start + " (no Mercurial repository)")
     1.9          Nil
    1.10        case Some(hg) =>
    1.11          val start_path = start.file.getCanonicalFile.toPath
    1.12 @@ -66,38 +66,6 @@
    1.13      }
    1.14    }
    1.15  
    1.16 -  def apply_updates(updates: List[(JFile, Update)])
    1.17 -  {
    1.18 -    val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _)
    1.19 -    val conflicts =
    1.20 -      file_updates.iterator_list.flatMap({ case (file, upds) =>
    1.21 -        Library.duplicates(upds.sortBy(_.range.start),
    1.22 -          (x: Update, y: Update) => x.range overlaps y.range) match
    1.23 -        {
    1.24 -          case Nil => None
    1.25 -          case bad => Some((file, bad))
    1.26 -        }
    1.27 -      })
    1.28 -    if (conflicts.nonEmpty)
    1.29 -      error(cat_lines(
    1.30 -        conflicts.map({ case (file, bad) =>
    1.31 -          "Conflicting updates for file " + file + bad.mkString("\n  ", "\n  ", "") })))
    1.32 -
    1.33 -    for ((file, upds) <- file_updates.iterator_list) {
    1.34 -      val edits =
    1.35 -        upds.sortBy(upd => - upd.range.start).flatMap(upd =>
    1.36 -          Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text))
    1.37 -      val new_text =
    1.38 -        (File.read(file) /: edits)({ case (text, edit) =>
    1.39 -          edit.edit(text, 0) match {
    1.40 -            case (None, text1) => text1
    1.41 -            case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file)
    1.42 -          }
    1.43 -        })
    1.44 -      File.write_backup2(Path.explode(File.standard_path(file)), new_text)
    1.45 -    }
    1.46 -  }
    1.47 -
    1.48  
    1.49    /* collective operations */
    1.50  
    1.51 @@ -131,6 +99,7 @@
    1.52      }
    1.53  
    1.54      if (operation_update) {
    1.55 +      progress.echo("\nUpdate theory imports:")
    1.56        val updates =
    1.57          selected.flatMap(session_name =>
    1.58          {
    1.59 @@ -178,7 +147,36 @@
    1.60  
    1.61            updates_root ::: updates_theories
    1.62          })
    1.63 -      apply_updates(updates)
    1.64 +
    1.65 +      val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _)
    1.66 +      val conflicts =
    1.67 +        file_updates.iterator_list.flatMap({ case (file, upds) =>
    1.68 +          Library.duplicates(upds.sortBy(_.range.start),
    1.69 +            (x: Update, y: Update) => x.range overlaps y.range) match
    1.70 +          {
    1.71 +            case Nil => None
    1.72 +            case bad => Some((file, bad))
    1.73 +          }
    1.74 +        })
    1.75 +      if (conflicts.nonEmpty)
    1.76 +        error(cat_lines(
    1.77 +          conflicts.map({ case (file, bad) =>
    1.78 +            "Conflicting updates for file " + file + bad.mkString("\n  ", "\n  ", "") })))
    1.79 +
    1.80 +      for ((file, upds) <- file_updates.iterator_list) {
    1.81 +        progress.echo("file " + quote(file.toString))
    1.82 +        val edits =
    1.83 +          upds.sortBy(upd => - upd.range.start).flatMap(upd =>
    1.84 +            Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text))
    1.85 +        val new_text =
    1.86 +          (File.read(file) /: edits)({ case (text, edit) =>
    1.87 +            edit.edit(text, 0) match {
    1.88 +              case (None, text1) => text1
    1.89 +              case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file)
    1.90 +            }
    1.91 +          })
    1.92 +        File.write_backup2(Path.explode(File.standard_path(file)), new_text)
    1.93 +      }
    1.94      }
    1.95    }
    1.96