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