src/Pure/Tools/update_imports.scala
changeset 65526 41dda3a292e6
parent 65518 bc8fa59211b7
child 65532 febfd9f78bd4
     1.1 --- a/src/Pure/Tools/update_imports.scala	Thu Apr 20 17:34:31 2017 +0200
     1.2 +++ b/src/Pure/Tools/update_imports.scala	Thu Apr 20 17:45:42 2017 +0200
     1.3 @@ -7,26 +7,132 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 +import java.io.{File => JFile}
     1.8 +
     1.9 +
    1.10  object Update_Imports
    1.11  {
    1.12    /* update imports */
    1.13  
    1.14 +  sealed case class Update(range: Text.Range, old_text: String, new_text: String)
    1.15 +  {
    1.16 +    def edits: List[Text.Edit] =
    1.17 +      Text.Edit.replace(range.start, old_text, new_text)
    1.18 +
    1.19 +    override def toString: String =
    1.20 +      range.toString + ": " + old_text + " -> " + new_text
    1.21 +  }
    1.22 +
    1.23 +  def update_name(keywords: Keyword.Keywords, pos: Position.T, update: String => String)
    1.24 +    : Option[(JFile, Update)] =
    1.25 +  {
    1.26 +    val file =
    1.27 +      pos match {
    1.28 +        case Position.File(file) => Path.explode(file).file.getCanonicalFile
    1.29 +        case _ => error("Missing file in position" + Position.here(pos))
    1.30 +      }
    1.31 +
    1.32 +    val text = File.read(file)
    1.33 +
    1.34 +    val range =
    1.35 +      pos match {
    1.36 +        case Position.Range(symbol_range) => Symbol.Text_Chunk(text).decode(symbol_range)
    1.37 +        case _ => error("Missing range in position" + Position.here(pos))
    1.38 +      }
    1.39 +
    1.40 +    Token.read_name(keywords, range.substring(text)) match {
    1.41 +      case Some(tok) =>
    1.42 +        val s1 = tok.source
    1.43 +        val s2 = Token.quote_name(keywords, update(tok.content))
    1.44 +        if (s1 == s2) None else Some((file, Update(range, s1, s2)))
    1.45 +      case None => error("Name token expected" + Position.here(pos))
    1.46 +    }
    1.47 +  }
    1.48 +
    1.49    def update_imports(
    1.50      options: Options,
    1.51      progress: Progress = No_Progress,
    1.52      selection: Sessions.Selection = Sessions.Selection.empty,
    1.53      dirs: List[Path] = Nil,
    1.54      select_dirs: List[Path] = Nil,
    1.55 -    verbose: Boolean = false)
    1.56 +    verbose: Boolean = false): List[(JFile, Update)] =
    1.57    {
    1.58      val full_sessions = Sessions.load(options, dirs, select_dirs)
    1.59      val (selected, selected_sessions) = full_sessions.selection(selection)
    1.60 +
    1.61      val deps =
    1.62        Sessions.deps(selected_sessions, progress = progress, verbose = verbose,
    1.63          global_theories = full_sessions.global_theories)
    1.64  
    1.65 -    // FIXME
    1.66 -    selected.foreach(progress.echo(_))
    1.67 +    selected.flatMap(session_name =>
    1.68 +    {
    1.69 +      val info = full_sessions(session_name)
    1.70 +      val session_base = deps(session_name)
    1.71 +      val resources = new Resources(session_base, default_qualifier = info.theory_qualifier)
    1.72 +      val local_theories = session_base.known.theories_local.iterator.map(_._2).toSet
    1.73 +
    1.74 +      def standard_import(qualifier: String, s: String): String =
    1.75 +      {
    1.76 +        val name = resources.import_name(qualifier, "", s)
    1.77 +        if (!local_theories.contains(name)) s
    1.78 +        if (resources.theory_qualifier(name) != qualifier) name.theory
    1.79 +        else if (Thy_Header.is_base_name(s)) name.theory_base_name
    1.80 +        else s
    1.81 +      }
    1.82 +
    1.83 +      val updates_root =
    1.84 +        for {
    1.85 +          (_, pos) <- info.theories.flatMap(_._2)
    1.86 +          upd <- update_name(Sessions.root_syntax.keywords, pos,
    1.87 +            standard_import(info.theory_qualifier, _))
    1.88 +        } yield upd
    1.89 +
    1.90 +      val updates_theories =
    1.91 +        for {
    1.92 +          (_, name) <- session_base.known.theories_local.toList
    1.93 +          (_, pos) <-
    1.94 +            // FIXME proper UTF8 positions for check_thy
    1.95 +            resources.check_thy_reader(name,
    1.96 +              Scan.char_reader(File.read(Path.explode(name.node))),
    1.97 +              Token.Pos.file(name.node)).imports
    1.98 +          upd <- update_name(session_base.syntax.keywords, pos,
    1.99 +            standard_import(resources.theory_qualifier(name), _))
   1.100 +        } yield upd
   1.101 +
   1.102 +      updates_root ::: updates_theories
   1.103 +    })
   1.104 +  }
   1.105 +
   1.106 +  def apply_updates(updates: List[(JFile, Update)])
   1.107 +  {
   1.108 +    val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _)
   1.109 +    val conflicts =
   1.110 +      file_updates.iterator_list.flatMap({ case (file, upds) =>
   1.111 +        Library.duplicates(upds.sortBy(_.range.start),
   1.112 +          (x: Update, y: Update) => x.range overlaps y.range) match
   1.113 +        {
   1.114 +          case Nil => None
   1.115 +          case bad => Some((file, bad))
   1.116 +        }
   1.117 +      })
   1.118 +    if (conflicts.nonEmpty)
   1.119 +      error(cat_lines(
   1.120 +        conflicts.map({ case (file, bad) =>
   1.121 +          "Conflicting updates for file " + file + bad.mkString("\n  ", "\n  ", "") })))
   1.122 +
   1.123 +    for ((file, upds) <- file_updates.iterator_list) {
   1.124 +      val edits =
   1.125 +        upds.sortBy(upd => - upd.range.start).flatMap(upd =>
   1.126 +          Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text))
   1.127 +      val new_text =
   1.128 +        (File.read(file) /: edits)({ case (text, edit) =>
   1.129 +          edit.edit(text, 0) match {
   1.130 +            case (None, text1) => text1
   1.131 +            case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file)
   1.132 +          }
   1.133 +        })
   1.134 +      File.write_backup(Path.explode(File.standard_path(file)), new_text)
   1.135 +    }
   1.136    }
   1.137  
   1.138  
   1.139 @@ -82,7 +188,10 @@
   1.140  
   1.141        val progress = new Console_Progress(verbose = verbose)
   1.142  
   1.143 -      update_imports(options, progress = progress, selection = selection,
   1.144 -        dirs = dirs, select_dirs = select_dirs, verbose = verbose)
   1.145 +      val updates =
   1.146 +        update_imports(options, progress = progress, selection = selection,
   1.147 +          dirs = dirs, select_dirs = select_dirs, verbose = verbose)
   1.148 +
   1.149 +      apply_updates(updates)
   1.150      })
   1.151  }