wrapper for "isabelle update_imports" with selection options like "isabelle build";
authorwenzelm
Wed Apr 19 21:32:46 2017 +0200 (2017-04-19)
changeset 65518bc8fa59211b7
parent 65517 1544e61e5314
child 65519 d244d8f8e13f
wrapper for "isabelle update_imports" with selection options like "isabelle build";
src/Pure/System/isabelle_tool.scala
src/Pure/Tools/update_imports.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/System/isabelle_tool.scala	Wed Apr 19 20:10:34 2017 +0200
     1.2 +++ b/src/Pure/System/isabelle_tool.scala	Wed Apr 19 21:32:46 2017 +0200
     1.3 @@ -115,6 +115,7 @@
     1.4        Remote_DMG.isabelle_tool,
     1.5        Update_Cartouches.isabelle_tool,
     1.6        Update_Header.isabelle_tool,
     1.7 +      Update_Imports.isabelle_tool,
     1.8        Update_Then.isabelle_tool,
     1.9        Update_Theorems.isabelle_tool,
    1.10        isabelle.vscode.Build_VSCode.isabelle_tool,
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Tools/update_imports.scala	Wed Apr 19 21:32:46 2017 +0200
     2.3 @@ -0,0 +1,88 @@
     2.4 +/*  Title:      Pure/Tools/update_imports.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Update theory imports to use session qualifiers.
     2.8 +*/
     2.9 +
    2.10 +package isabelle
    2.11 +
    2.12 +
    2.13 +object Update_Imports
    2.14 +{
    2.15 +  /* update imports */
    2.16 +
    2.17 +  def update_imports(
    2.18 +    options: Options,
    2.19 +    progress: Progress = No_Progress,
    2.20 +    selection: Sessions.Selection = Sessions.Selection.empty,
    2.21 +    dirs: List[Path] = Nil,
    2.22 +    select_dirs: List[Path] = Nil,
    2.23 +    verbose: Boolean = false)
    2.24 +  {
    2.25 +    val full_sessions = Sessions.load(options, dirs, select_dirs)
    2.26 +    val (selected, selected_sessions) = full_sessions.selection(selection)
    2.27 +    val deps =
    2.28 +      Sessions.deps(selected_sessions, progress = progress, verbose = verbose,
    2.29 +        global_theories = full_sessions.global_theories)
    2.30 +
    2.31 +    // FIXME
    2.32 +    selected.foreach(progress.echo(_))
    2.33 +  }
    2.34 +
    2.35 +
    2.36 +  /* Isabelle tool wrapper */
    2.37 +
    2.38 +  val isabelle_tool =
    2.39 +    Isabelle_Tool("update_imports", "update theory imports to use session qualifiers", args =>
    2.40 +    {
    2.41 +      var select_dirs: List[Path] = Nil
    2.42 +      var requirements = false
    2.43 +      var exclude_session_groups: List[String] = Nil
    2.44 +      var all_sessions = false
    2.45 +      var dirs: List[Path] = Nil
    2.46 +      var session_groups: List[String] = Nil
    2.47 +      var options = Options.init()
    2.48 +      var verbose = false
    2.49 +      var exclude_sessions: List[String] = Nil
    2.50 +
    2.51 +      val getopts = Getopts("""
    2.52 +Usage: isabelle update_imports [OPTIONS] [SESSIONS ...]
    2.53 +
    2.54 +  Options are:
    2.55 +    -D DIR       include session directory and select its sessions
    2.56 +    -R           operate on requirements of selected sessions
    2.57 +    -X NAME      exclude sessions from group NAME and all descendants
    2.58 +    -a           select all sessions
    2.59 +    -d DIR       include session directory
    2.60 +    -g NAME      select session group NAME
    2.61 +    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    2.62 +    -v           verbose
    2.63 +    -x NAME      exclude session NAME and all descendants
    2.64 +
    2.65 +  Update theory imports to use session qualifiers.
    2.66 +
    2.67 +  Old versions of files are preserved by appending "~~".
    2.68 +""",
    2.69 +      "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
    2.70 +      "R" -> (_ => requirements = true),
    2.71 +      "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
    2.72 +      "a" -> (_ => all_sessions = true),
    2.73 +      "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    2.74 +      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
    2.75 +      "o:" -> (arg => options = options + arg),
    2.76 +      "v" -> (_ => verbose = true),
    2.77 +      "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
    2.78 +
    2.79 +      val sessions = getopts(args)
    2.80 +      if (args.isEmpty) getopts.usage()
    2.81 +
    2.82 +      val selection =
    2.83 +        Sessions.Selection(requirements, all_sessions, exclude_session_groups,
    2.84 +          exclude_sessions, session_groups, sessions)
    2.85 +
    2.86 +      val progress = new Console_Progress(verbose = verbose)
    2.87 +
    2.88 +      update_imports(options, progress = progress, selection = selection,
    2.89 +        dirs = dirs, select_dirs = select_dirs, verbose = verbose)
    2.90 +    })
    2.91 +}
     3.1 --- a/src/Pure/build-jars	Wed Apr 19 20:10:34 2017 +0200
     3.2 +++ b/src/Pure/build-jars	Wed Apr 19 21:32:46 2017 +0200
     3.3 @@ -143,6 +143,7 @@
     3.4    Tools/task_statistics.scala
     3.5    Tools/update_cartouches.scala
     3.6    Tools/update_header.scala
     3.7 +  Tools/update_imports.scala
     3.8    Tools/update_then.scala
     3.9    Tools/update_theorems.scala
    3.10    library.scala