src/Pure/Tools/imports.scala
author wenzelm
Sun Apr 23 16:18:31 2017 +0200 (2017-04-23)
changeset 65558 479406635409
parent 65557 29c69a599743
child 65561 741b1d3930c0
permissions -rw-r--r--
support for multiple operations via options;
     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   /* 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 apply_updates(updates: List[(JFile, Update)])
    53   {
    54     val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _)
    55     val conflicts =
    56       file_updates.iterator_list.flatMap({ case (file, upds) =>
    57         Library.duplicates(upds.sortBy(_.range.start),
    58           (x: Update, y: Update) => x.range overlaps y.range) match
    59         {
    60           case Nil => None
    61           case bad => Some((file, bad))
    62         }
    63       })
    64     if (conflicts.nonEmpty)
    65       error(cat_lines(
    66         conflicts.map({ case (file, bad) =>
    67           "Conflicting updates for file " + file + bad.mkString("\n  ", "\n  ", "") })))
    68 
    69     for ((file, upds) <- file_updates.iterator_list) {
    70       val edits =
    71         upds.sortBy(upd => - upd.range.start).flatMap(upd =>
    72           Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text))
    73       val new_text =
    74         (File.read(file) /: edits)({ case (text, edit) =>
    75           edit.edit(text, 0) match {
    76             case (None, text1) => text1
    77             case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file)
    78           }
    79         })
    80       File.write_backup2(Path.explode(File.standard_path(file)), new_text)
    81     }
    82   }
    83 
    84   def imports(
    85     options: Options,
    86     operation_update: Boolean = false,
    87     progress: Progress = No_Progress,
    88     selection: Sessions.Selection = Sessions.Selection.empty,
    89     dirs: List[Path] = Nil,
    90     select_dirs: List[Path] = Nil,
    91     verbose: Boolean = false) =
    92   {
    93     val full_sessions = Sessions.load(options, dirs, select_dirs)
    94     val (selected, selected_sessions) = full_sessions.selection(selection)
    95 
    96     val deps =
    97       Sessions.deps(selected_sessions, progress = progress, verbose = verbose,
    98         global_theories = full_sessions.global_theories)
    99 
   100     if (operation_update) {
   101       val updates =
   102         selected.flatMap(session_name =>
   103         {
   104           val info = full_sessions(session_name)
   105           val session_base = deps(session_name)
   106           val session_resources = new Resources(session_base)
   107           val imports_resources = new Resources(session_base.get_imports)
   108 
   109           val local_theories =
   110             (for {
   111               (_, name) <- session_base.known.theories_local.iterator
   112               if session_resources.theory_qualifier(name) == info.theory_qualifier
   113             } yield name).toSet
   114 
   115           def standard_import(qualifier: String, dir: String, s: String): String =
   116           {
   117             val name = imports_resources.import_name(qualifier, dir, s)
   118             val file = Path.explode(name.node).file
   119             val s1 =
   120               imports_resources.session_base.known.get_file(file) match {
   121                 case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
   122                   name1.theory
   123                 case Some(name1) if Thy_Header.is_base_name(s) =>
   124                   name1.theory_base_name
   125                 case _ => s
   126               }
   127             val name2 = imports_resources.import_name(qualifier, dir, s1)
   128             if (name.node == name2.node) s1 else s
   129           }
   130 
   131           val updates_root =
   132             for {
   133               (_, pos) <- info.theories.flatMap(_._2)
   134               upd <- update_name(Sessions.root_syntax.keywords, pos,
   135                 standard_import(info.theory_qualifier, info.dir.implode, _))
   136             } yield upd
   137 
   138           val updates_theories =
   139             for {
   140               (_, name) <- session_base.known.theories_local.toList
   141               (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
   142               upd <- update_name(session_base.syntax.keywords, pos,
   143                 standard_import(session_resources.theory_qualifier(name), name.master_dir, _))
   144             } yield upd
   145 
   146           updates_root ::: updates_theories
   147         })
   148       apply_updates(updates)
   149     }
   150   }
   151 
   152 
   153   /* Isabelle tool wrapper */
   154 
   155   val isabelle_tool =
   156     Isabelle_Tool("imports", "maintain theory imports wrt. session structure", args =>
   157     {
   158       var select_dirs: List[Path] = Nil
   159       var requirements = false
   160       var operation_update = false
   161       var exclude_session_groups: List[String] = Nil
   162       var all_sessions = false
   163       var dirs: List[Path] = Nil
   164       var session_groups: List[String] = Nil
   165       var options = Options.init()
   166       var verbose = false
   167       var exclude_sessions: List[String] = Nil
   168 
   169       val getopts = Getopts("""
   170 Usage: isabelle imports [OPTIONS] [SESSIONS ...]
   171 
   172   Options are:
   173     -D DIR       include session directory and select its sessions
   174     -R           operate on requirements of selected sessions
   175     -U           operation: update theory imports to use session qualifiers
   176     -X NAME      exclude sessions from group NAME and all descendants
   177     -a           select all sessions
   178     -d DIR       include session directory
   179     -g NAME      select session group NAME
   180     -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
   181     -v           verbose
   182     -x NAME      exclude session NAME and all descendants
   183 
   184   Maintain theory imports wrt. session structure. At least one operation
   185   needs to be specified (see option -U).
   186 """,
   187       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
   188       "R" -> (_ => requirements = true),
   189       "U" -> (_ => operation_update = true),
   190       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   191       "a" -> (_ => all_sessions = true),
   192       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   193       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
   194       "o:" -> (arg => options = options + arg),
   195       "v" -> (_ => verbose = true),
   196       "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
   197 
   198       val sessions = getopts(args)
   199       if (args.isEmpty || !operation_update) getopts.usage()
   200 
   201       val selection =
   202         Sessions.Selection(requirements, all_sessions, exclude_session_groups,
   203           exclude_sessions, session_groups, sessions)
   204 
   205       val progress = new Console_Progress(verbose = verbose)
   206 
   207       imports(options, operation_update = operation_update, progress = progress,
   208         selection = selection, dirs = dirs, select_dirs = select_dirs, verbose = verbose)
   209     })
   210 }