src/Pure/Tools/update_imports.scala
author wenzelm
Wed Apr 19 21:32:46 2017 +0200 (2017-04-19)
changeset 65518 bc8fa59211b7
child 65526 41dda3a292e6
permissions -rw-r--r--
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm@65518
     1
/*  Title:      Pure/Tools/update_imports.scala
wenzelm@65518
     2
    Author:     Makarius
wenzelm@65518
     3
wenzelm@65518
     4
Update theory imports to use session qualifiers.
wenzelm@65518
     5
*/
wenzelm@65518
     6
wenzelm@65518
     7
package isabelle
wenzelm@65518
     8
wenzelm@65518
     9
wenzelm@65518
    10
object Update_Imports
wenzelm@65518
    11
{
wenzelm@65518
    12
  /* update imports */
wenzelm@65518
    13
wenzelm@65518
    14
  def update_imports(
wenzelm@65518
    15
    options: Options,
wenzelm@65518
    16
    progress: Progress = No_Progress,
wenzelm@65518
    17
    selection: Sessions.Selection = Sessions.Selection.empty,
wenzelm@65518
    18
    dirs: List[Path] = Nil,
wenzelm@65518
    19
    select_dirs: List[Path] = Nil,
wenzelm@65518
    20
    verbose: Boolean = false)
wenzelm@65518
    21
  {
wenzelm@65518
    22
    val full_sessions = Sessions.load(options, dirs, select_dirs)
wenzelm@65518
    23
    val (selected, selected_sessions) = full_sessions.selection(selection)
wenzelm@65518
    24
    val deps =
wenzelm@65518
    25
      Sessions.deps(selected_sessions, progress = progress, verbose = verbose,
wenzelm@65518
    26
        global_theories = full_sessions.global_theories)
wenzelm@65518
    27
wenzelm@65518
    28
    // FIXME
wenzelm@65518
    29
    selected.foreach(progress.echo(_))
wenzelm@65518
    30
  }
wenzelm@65518
    31
wenzelm@65518
    32
wenzelm@65518
    33
  /* Isabelle tool wrapper */
wenzelm@65518
    34
wenzelm@65518
    35
  val isabelle_tool =
wenzelm@65518
    36
    Isabelle_Tool("update_imports", "update theory imports to use session qualifiers", args =>
wenzelm@65518
    37
    {
wenzelm@65518
    38
      var select_dirs: List[Path] = Nil
wenzelm@65518
    39
      var requirements = false
wenzelm@65518
    40
      var exclude_session_groups: List[String] = Nil
wenzelm@65518
    41
      var all_sessions = false
wenzelm@65518
    42
      var dirs: List[Path] = Nil
wenzelm@65518
    43
      var session_groups: List[String] = Nil
wenzelm@65518
    44
      var options = Options.init()
wenzelm@65518
    45
      var verbose = false
wenzelm@65518
    46
      var exclude_sessions: List[String] = Nil
wenzelm@65518
    47
wenzelm@65518
    48
      val getopts = Getopts("""
wenzelm@65518
    49
Usage: isabelle update_imports [OPTIONS] [SESSIONS ...]
wenzelm@65518
    50
wenzelm@65518
    51
  Options are:
wenzelm@65518
    52
    -D DIR       include session directory and select its sessions
wenzelm@65518
    53
    -R           operate on requirements of selected sessions
wenzelm@65518
    54
    -X NAME      exclude sessions from group NAME and all descendants
wenzelm@65518
    55
    -a           select all sessions
wenzelm@65518
    56
    -d DIR       include session directory
wenzelm@65518
    57
    -g NAME      select session group NAME
wenzelm@65518
    58
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
wenzelm@65518
    59
    -v           verbose
wenzelm@65518
    60
    -x NAME      exclude session NAME and all descendants
wenzelm@65518
    61
wenzelm@65518
    62
  Update theory imports to use session qualifiers.
wenzelm@65518
    63
wenzelm@65518
    64
  Old versions of files are preserved by appending "~~".
wenzelm@65518
    65
""",
wenzelm@65518
    66
      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
wenzelm@65518
    67
      "R" -> (_ => requirements = true),
wenzelm@65518
    68
      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
wenzelm@65518
    69
      "a" -> (_ => all_sessions = true),
wenzelm@65518
    70
      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
wenzelm@65518
    71
      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
wenzelm@65518
    72
      "o:" -> (arg => options = options + arg),
wenzelm@65518
    73
      "v" -> (_ => verbose = true),
wenzelm@65518
    74
      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
wenzelm@65518
    75
wenzelm@65518
    76
      val sessions = getopts(args)
wenzelm@65518
    77
      if (args.isEmpty) getopts.usage()
wenzelm@65518
    78
wenzelm@65518
    79
      val selection =
wenzelm@65518
    80
        Sessions.Selection(requirements, all_sessions, exclude_session_groups,
wenzelm@65518
    81
          exclude_sessions, session_groups, sessions)
wenzelm@65518
    82
wenzelm@65518
    83
      val progress = new Console_Progress(verbose = verbose)
wenzelm@65518
    84
wenzelm@65518
    85
      update_imports(options, progress = progress, selection = selection,
wenzelm@65518
    86
        dirs = dirs, select_dirs = select_dirs, verbose = verbose)
wenzelm@65518
    87
    })
wenzelm@65518
    88
}