src/Pure/Tools/imports.scala
changeset 65557 29c69a599743
parent 65542 6a00518bbfcc
child 65558 479406635409
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Tools/imports.scala	Sun Apr 23 15:59:51 2017 +0200
     1.3 @@ -0,0 +1,206 @@
     1.4 +/*  Title:      Pure/Tools/imports.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Maintain theory imports wrt. session structure.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +import java.io.{File => JFile}
    1.14 +
    1.15 +
    1.16 +object Imports
    1.17 +{
    1.18 +  /* update imports */
    1.19 +
    1.20 +  sealed case class Update(range: Text.Range, old_text: String, new_text: String)
    1.21 +  {
    1.22 +    def edits: List[Text.Edit] =
    1.23 +      Text.Edit.replace(range.start, old_text, new_text)
    1.24 +
    1.25 +    override def toString: String =
    1.26 +      range.toString + ": " + old_text + " -> " + new_text
    1.27 +  }
    1.28 +
    1.29 +  def update_name(keywords: Keyword.Keywords, pos: Position.T, update: String => String)
    1.30 +    : Option[(JFile, Update)] =
    1.31 +  {
    1.32 +    val file =
    1.33 +      pos match {
    1.34 +        case Position.File(file) => Path.explode(file).file.getCanonicalFile
    1.35 +        case _ => error("Missing file in position" + Position.here(pos))
    1.36 +      }
    1.37 +
    1.38 +    val text = File.read(file)
    1.39 +
    1.40 +    val range =
    1.41 +      pos match {
    1.42 +        case Position.Range(symbol_range) => Symbol.Text_Chunk(text).decode(symbol_range)
    1.43 +        case _ => error("Missing range in position" + Position.here(pos))
    1.44 +      }
    1.45 +
    1.46 +    Token.read_name(keywords, range.substring(text)) match {
    1.47 +      case Some(tok) =>
    1.48 +        val s1 = tok.source
    1.49 +        val s2 = Token.quote_name(keywords, update(tok.content))
    1.50 +        if (s1 == s2) None else Some((file, Update(range, s1, s2)))
    1.51 +      case None => error("Name token expected" + Position.here(pos))
    1.52 +    }
    1.53 +  }
    1.54 +
    1.55 +  def update_imports(
    1.56 +    options: Options,
    1.57 +    progress: Progress = No_Progress,
    1.58 +    selection: Sessions.Selection = Sessions.Selection.empty,
    1.59 +    dirs: List[Path] = Nil,
    1.60 +    select_dirs: List[Path] = Nil,
    1.61 +    verbose: Boolean = false): List[(JFile, Update)] =
    1.62 +  {
    1.63 +    val full_sessions = Sessions.load(options, dirs, select_dirs)
    1.64 +    val (selected, selected_sessions) = full_sessions.selection(selection)
    1.65 +
    1.66 +    val deps =
    1.67 +      Sessions.deps(selected_sessions, progress = progress, verbose = verbose,
    1.68 +        global_theories = full_sessions.global_theories)
    1.69 +
    1.70 +    selected.flatMap(session_name =>
    1.71 +    {
    1.72 +      val info = full_sessions(session_name)
    1.73 +      val session_base = deps(session_name)
    1.74 +      val session_resources = new Resources(session_base)
    1.75 +      val imports_resources = new Resources(session_base.get_imports)
    1.76 +
    1.77 +      val local_theories =
    1.78 +        (for {
    1.79 +          (_, name) <- session_base.known.theories_local.iterator
    1.80 +          if session_resources.theory_qualifier(name) == info.theory_qualifier
    1.81 +        } yield name).toSet
    1.82 +
    1.83 +      def standard_import(qualifier: String, dir: String, s: String): String =
    1.84 +      {
    1.85 +        val name = imports_resources.import_name(qualifier, dir, s)
    1.86 +        val file = Path.explode(name.node).file
    1.87 +        val s1 =
    1.88 +          imports_resources.session_base.known.get_file(file) match {
    1.89 +            case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
    1.90 +              name1.theory
    1.91 +            case Some(name1) if Thy_Header.is_base_name(s) =>
    1.92 +              name1.theory_base_name
    1.93 +            case _ => s
    1.94 +          }
    1.95 +        val name2 = imports_resources.import_name(qualifier, dir, s1)
    1.96 +        if (name.node == name2.node) s1 else s
    1.97 +      }
    1.98 +
    1.99 +      val updates_root =
   1.100 +        for {
   1.101 +          (_, pos) <- info.theories.flatMap(_._2)
   1.102 +          upd <- update_name(Sessions.root_syntax.keywords, pos,
   1.103 +            standard_import(info.theory_qualifier, info.dir.implode, _))
   1.104 +        } yield upd
   1.105 +
   1.106 +      val updates_theories =
   1.107 +        for {
   1.108 +          (_, name) <- session_base.known.theories_local.toList
   1.109 +          (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
   1.110 +          upd <- update_name(session_base.syntax.keywords, pos,
   1.111 +            standard_import(session_resources.theory_qualifier(name), name.master_dir, _))
   1.112 +        } yield upd
   1.113 +
   1.114 +      updates_root ::: updates_theories
   1.115 +    })
   1.116 +  }
   1.117 +
   1.118 +  def apply_updates(updates: List[(JFile, Update)])
   1.119 +  {
   1.120 +    val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _)
   1.121 +    val conflicts =
   1.122 +      file_updates.iterator_list.flatMap({ case (file, upds) =>
   1.123 +        Library.duplicates(upds.sortBy(_.range.start),
   1.124 +          (x: Update, y: Update) => x.range overlaps y.range) match
   1.125 +        {
   1.126 +          case Nil => None
   1.127 +          case bad => Some((file, bad))
   1.128 +        }
   1.129 +      })
   1.130 +    if (conflicts.nonEmpty)
   1.131 +      error(cat_lines(
   1.132 +        conflicts.map({ case (file, bad) =>
   1.133 +          "Conflicting updates for file " + file + bad.mkString("\n  ", "\n  ", "") })))
   1.134 +
   1.135 +    for ((file, upds) <- file_updates.iterator_list) {
   1.136 +      val edits =
   1.137 +        upds.sortBy(upd => - upd.range.start).flatMap(upd =>
   1.138 +          Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text))
   1.139 +      val new_text =
   1.140 +        (File.read(file) /: edits)({ case (text, edit) =>
   1.141 +          edit.edit(text, 0) match {
   1.142 +            case (None, text1) => text1
   1.143 +            case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file)
   1.144 +          }
   1.145 +        })
   1.146 +      File.write_backup2(Path.explode(File.standard_path(file)), new_text)
   1.147 +    }
   1.148 +  }
   1.149 +
   1.150 +
   1.151 +  /* Isabelle tool wrapper */
   1.152 +
   1.153 +  val isabelle_tool =
   1.154 +    Isabelle_Tool("imports", "maintain theory imports wrt. session structure", args =>
   1.155 +    {
   1.156 +      var select_dirs: List[Path] = Nil
   1.157 +      var requirements = false
   1.158 +      var exclude_session_groups: List[String] = Nil
   1.159 +      var all_sessions = false
   1.160 +      var dirs: List[Path] = Nil
   1.161 +      var session_groups: List[String] = Nil
   1.162 +      var options = Options.init()
   1.163 +      var verbose = false
   1.164 +      var exclude_sessions: List[String] = Nil
   1.165 +
   1.166 +      val getopts = Getopts("""
   1.167 +Usage: isabelle imports [OPTIONS] [SESSIONS ...]
   1.168 +
   1.169 +  Options are:
   1.170 +    -D DIR       include session directory and select its sessions
   1.171 +    -R           operate on requirements of selected sessions
   1.172 +    -X NAME      exclude sessions from group NAME and all descendants
   1.173 +    -a           select all sessions
   1.174 +    -d DIR       include session directory
   1.175 +    -g NAME      select session group NAME
   1.176 +    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   1.177 +    -v           verbose
   1.178 +    -x NAME      exclude session NAME and all descendants
   1.179 +
   1.180 +  Maintain theory imports wrt. session structure.
   1.181 +
   1.182 +  Old versions of files are preserved by appending "~~".
   1.183 +""",
   1.184 +      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
   1.185 +      "R" -> (_ => requirements = true),
   1.186 +      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   1.187 +      "a" -> (_ => all_sessions = true),
   1.188 +      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   1.189 +      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
   1.190 +      "o:" -> (arg => options = options + arg),
   1.191 +      "v" -> (_ => verbose = true),
   1.192 +      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
   1.193 +
   1.194 +      val sessions = getopts(args)
   1.195 +      if (args.isEmpty) getopts.usage()
   1.196 +
   1.197 +      val selection =
   1.198 +        Sessions.Selection(requirements, all_sessions, exclude_session_groups,
   1.199 +          exclude_sessions, session_groups, sessions)
   1.200 +
   1.201 +      val progress = new Console_Progress(verbose = verbose)
   1.202 +
   1.203 +      val updates =
   1.204 +        update_imports(options, progress = progress, selection = selection,
   1.205 +          dirs = dirs, select_dirs = select_dirs, verbose = verbose)
   1.206 +
   1.207 +      apply_updates(updates)
   1.208 +    })
   1.209 +}