src/Pure/Tools/imports.scala
author wenzelm
Thu Aug 31 19:06:14 2017 +0200 (22 months ago)
changeset 66575 191048506504
parent 66571 0fdeb24e535e
child 66671 41b64e53b6a1
permissions -rw-r--r--
clarified signature: provide all_known information uniformly (it is subject to Sessions.T selection);
     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   /* repository files */
    16 
    17   def repository_files(progress: Progress, start: Path, pred: JFile => Boolean = _ => true)
    18       : List[JFile] =
    19     Mercurial.find_repository(start) match {
    20       case None =>
    21         progress.echo_warning("Ignoring directory " + start + " (no Mercurial repository)")
    22         Nil
    23       case Some(hg) =>
    24         val start_path = start.canonical_file.toPath
    25         for {
    26           name <- hg.known_files()
    27           file = (hg.root + Path.explode(name)).file
    28           if pred(file) && File.canonical(file).toPath.startsWith(start_path)
    29         } yield file
    30     }
    31 
    32 
    33   /* update imports */
    34 
    35   sealed case class Update(range: Text.Range, old_text: String, new_text: String)
    36   {
    37     def edits: List[Text.Edit] =
    38       Text.Edit.replace(range.start, old_text, new_text)
    39 
    40     override def toString: String =
    41       range.toString + ": " + old_text + " -> " + new_text
    42   }
    43 
    44   def update_name(keywords: Keyword.Keywords, pos: Position.T, update: String => String)
    45     : Option[(JFile, Update)] =
    46   {
    47     val file =
    48       pos match {
    49         case Position.File(file) => Path.explode(file).canonical_file
    50         case _ => error("Missing file in position" + Position.here(pos))
    51       }
    52 
    53     val text = File.read(file)
    54 
    55     val range =
    56       pos match {
    57         case Position.Range(symbol_range) => Symbol.Text_Chunk(text).decode(symbol_range)
    58         case _ => error("Missing range in position" + Position.here(pos))
    59       }
    60 
    61     Token.read_name(keywords, range.substring(text)) match {
    62       case Some(tok) =>
    63         val s1 = tok.source
    64         val s2 = Token.quote_name(keywords, update(tok.content))
    65         if (s1 == s2) None else Some((file, Update(range, s1, s2)))
    66       case None => error("Name token expected" + Position.here(pos))
    67     }
    68   }
    69 
    70 
    71   /* collective operations */
    72 
    73   def imports(
    74     options: Options,
    75     operation_imports: Boolean = false,
    76     operation_repository_files: Boolean = false,
    77     operation_update: Boolean = false,
    78     update_message: String = "",
    79     progress: Progress = No_Progress,
    80     selection: Sessions.Selection = Sessions.Selection.empty,
    81     dirs: List[Path] = Nil,
    82     select_dirs: List[Path] = Nil,
    83     verbose: Boolean = false) =
    84   {
    85     val full_sessions = Sessions.load(options, dirs, select_dirs)
    86     val (selected, selected_sessions) = full_sessions.selection(selection)
    87 
    88     val deps =
    89       Sessions.deps(selected_sessions, progress = progress, verbose = verbose,
    90         global_theories = full_sessions.global_theories).check_errors
    91 
    92     val root_keywords = Sessions.root_syntax.keywords
    93 
    94 
    95     if (operation_imports) {
    96       progress.echo("\nPotential session imports:")
    97       selected.flatMap(session_name =>
    98       {
    99         val info = full_sessions(session_name)
   100         val session_resources = new Resources(deps(session_name))
   101 
   102         val declared_imports =
   103           full_sessions.imports_ancestors(session_name).toSet + session_name
   104         val extra_imports =
   105           (for {
   106             (_, a) <- session_resources.session_base.known.theories.iterator
   107             if session_resources.theory_qualifier(a) == info.theory_qualifier
   108             b <- deps.all_known.get_file(Path.explode(a.node).file)
   109             qualifier = session_resources.theory_qualifier(b)
   110             if !declared_imports.contains(qualifier)
   111           } yield qualifier).toSet
   112 
   113         if (extra_imports.isEmpty) None
   114         else Some((session_name, extra_imports.toList.sorted, declared_imports.size))
   115       }).sortBy(_._3).foreach({ case (session_name, extra_imports, _) =>
   116         progress.echo("session " + Token.quote_name(root_keywords, session_name) + ": " +
   117           extra_imports.map(Token.quote_name(root_keywords, _)).mkString(" "))
   118       })
   119     }
   120 
   121     if (operation_repository_files) {
   122       progress.echo("\nMercurial files check:")
   123       val unused_files =
   124         for {
   125           (_, dir) <- Sessions.directories(dirs, select_dirs)
   126           file <- repository_files(progress, dir, file => file.getName.endsWith(".thy"))
   127           if deps.all_known.get_file(file).isEmpty
   128         } yield file
   129       unused_files.foreach(file => progress.echo("unused file " + quote(file.toString)))
   130     }
   131 
   132     if (operation_update) {
   133       progress.echo("\nUpdate theory imports" + update_message + ":")
   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_base = session_base.get_imports
   141           val imports_resources = new Resources(imports_base)
   142 
   143           def standard_import(qualifier: String, dir: String, s: String): String =
   144           {
   145             val name = imports_resources.import_name(qualifier, dir, s)
   146             val s1 =
   147               if (imports_base.loaded_theory(name)) name.theory
   148               else {
   149                 imports_base.known.get_file(Path.explode(name.node).file) match {
   150                   case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
   151                     name1.theory
   152                   case Some(name1) if Thy_Header.is_base_name(s) =>
   153                     name1.theory_base_name
   154                   case _ => s
   155                 }
   156               }
   157             val name2 = imports_resources.import_name(qualifier, dir, s1)
   158             if (name.node == name2.node) s1 else s
   159           }
   160 
   161           val updates_root =
   162             for {
   163               (_, pos) <- info.theories.flatMap(_._2)
   164               upd <- update_name(root_keywords, pos,
   165                 standard_import(info.theory_qualifier, info.dir.implode, _))
   166             } yield upd
   167 
   168           val updates_theories =
   169             for {
   170               (_, name) <- session_base.known.theories_local.toList
   171               if session_resources.theory_qualifier(name) == info.theory_qualifier
   172               (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
   173               upd <- update_name(session_base.syntax.keywords, pos,
   174                 standard_import(session_resources.theory_qualifier(name), name.master_dir, _))
   175             } yield upd
   176 
   177           updates_root ::: updates_theories
   178         })
   179 
   180       val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _)
   181       val conflicts =
   182         file_updates.iterator_list.flatMap({ case (file, upds) =>
   183           Library.duplicates(upds.sortBy(_.range.start),
   184             (x: Update, y: Update) => x.range overlaps y.range) match
   185           {
   186             case Nil => None
   187             case bad => Some((file, bad))
   188           }
   189         })
   190       if (conflicts.nonEmpty)
   191         error(cat_lines(
   192           conflicts.map({ case (file, bad) =>
   193             "Conflicting updates for file " + file + bad.mkString("\n  ", "\n  ", "") })))
   194 
   195       for ((file, upds) <- file_updates.iterator_list.toList.sortBy(p => p._1.toString)) {
   196         progress.echo("file " + quote(file.toString))
   197         val edits =
   198           upds.sortBy(upd => - upd.range.start).flatMap(upd =>
   199             Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text))
   200         val new_text =
   201           (File.read(file) /: edits)({ case (text, edit) =>
   202             edit.edit(text, 0) match {
   203               case (None, text1) => text1
   204               case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file)
   205             }
   206           })
   207         File.write_backup2(Path.explode(File.standard_path(file)), new_text)
   208       }
   209     }
   210   }
   211 
   212 
   213   /* Isabelle tool wrapper */
   214 
   215   val isabelle_tool =
   216     Isabelle_Tool("imports", "maintain theory imports wrt. session structure", args =>
   217     {
   218       var select_dirs: List[Path] = Nil
   219       var operation_imports = false
   220       var operation_repository_files = false
   221       var requirements = false
   222       var operation_update = false
   223       var exclude_session_groups: List[String] = Nil
   224       var all_sessions = false
   225       var dirs: List[Path] = Nil
   226       var session_groups: List[String] = Nil
   227       var incremental_update = false
   228       var options = Options.init()
   229       var verbose = false
   230       var exclude_sessions: List[String] = Nil
   231 
   232       val getopts = Getopts("""
   233 Usage: isabelle imports [OPTIONS] [SESSIONS ...]
   234 
   235   Options are:
   236     -D DIR       include session directory and select its sessions
   237     -I           operation: report potential session imports
   238     -M           operation: Mercurial files check for imported theory files
   239     -R           operate on requirements of selected sessions
   240     -U           operation: update theory imports to use session qualifiers
   241     -X NAME      exclude sessions from group NAME and all descendants
   242     -a           select all sessions
   243     -d DIR       include session directory
   244     -g NAME      select session group NAME
   245     -i           incremental update according to session graph structure
   246     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   247     -v           verbose
   248     -x NAME      exclude session NAME and all descendants
   249 
   250   Maintain theory imports wrt. session structure. At least one operation
   251   needs to be specified (see options -I -M -U).
   252 """,
   253       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
   254       "I" -> (_ => operation_imports = true),
   255       "M" -> (_ => operation_repository_files = true),
   256       "R" -> (_ => requirements = true),
   257       "U" -> (_ => operation_update = true),
   258       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   259       "a" -> (_ => all_sessions = true),
   260       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   261       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
   262       "i" -> (_ => incremental_update = true),
   263       "o:" -> (arg => options = options + arg),
   264       "v" -> (_ => verbose = true),
   265       "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
   266 
   267       val sessions = getopts(args)
   268       if (args.isEmpty || !(operation_imports || operation_repository_files || operation_update))
   269         getopts.usage()
   270 
   271       val selection =
   272         Sessions.Selection(requirements, all_sessions, exclude_session_groups,
   273           exclude_sessions, session_groups, sessions)
   274 
   275       val progress = new Console_Progress(verbose = verbose)
   276 
   277       if (operation_imports || operation_repository_files ||
   278           operation_update && !incremental_update)
   279       {
   280         imports(options, operation_imports = operation_imports,
   281           operation_repository_files = operation_repository_files,
   282           operation_update = operation_update,
   283           progress = progress, selection = selection, dirs = dirs, select_dirs = select_dirs,
   284           verbose = verbose)
   285       }
   286       else if (operation_update && incremental_update) {
   287         val (selected, selected_sessions) =
   288           Sessions.load(options, dirs, select_dirs).selection(selection)
   289         selected_sessions.imports_topological_order.foreach(info =>
   290         {
   291           imports(options, operation_update = operation_update, progress = progress,
   292             update_message = " for session " + quote(info.name),
   293             selection = Sessions.Selection(sessions = List(info.name)),
   294             dirs = dirs ::: select_dirs, verbose = verbose)
   295         })
   296       }
   297     })
   298 }