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