support for incremental update according to session graph structure;
authorwenzelm
Thu Aug 17 21:12:55 2017 +0200 (21 months ago)
changeset 664491be102db1598
parent 66448 97ad7a583457
child 66450 a8299195ed82
support for incremental update according to session graph structure;
NEWS
src/Pure/Tools/imports.scala
     1.1 --- a/NEWS	Thu Aug 17 18:19:16 2017 +0200
     1.2 +++ b/NEWS	Thu Aug 17 21:12:55 2017 +0200
     1.3 @@ -277,6 +277,7 @@
     1.4  
     1.5    isabelle imports -I -a
     1.6    isabelle imports -U -a
     1.7 +  isabelle imports -U -i -a
     1.8    isabelle imports -M -a -d '~~/src/Benchmarks'
     1.9  
    1.10  * Isabelle/Scala: the SQL module supports access to relational
     2.1 --- a/src/Pure/Tools/imports.scala	Thu Aug 17 18:19:16 2017 +0200
     2.2 +++ b/src/Pure/Tools/imports.scala	Thu Aug 17 21:12:55 2017 +0200
     2.3 @@ -75,6 +75,7 @@
     2.4      operation_imports: Boolean = false,
     2.5      operation_repository_files: Boolean = false,
     2.6      operation_update: Boolean = false,
     2.7 +    update_message: String = "",
     2.8      progress: Progress = No_Progress,
     2.9      selection: Sessions.Selection = Sessions.Selection.empty,
    2.10      dirs: List[Path] = Nil,
    2.11 @@ -130,7 +131,7 @@
    2.12      }
    2.13  
    2.14      if (operation_update) {
    2.15 -      progress.echo("\nUpdate theory imports:")
    2.16 +      progress.echo("\nUpdate theory imports" + update_message + ":")
    2.17        val updates =
    2.18          selected.flatMap(session_name =>
    2.19          {
    2.20 @@ -224,6 +225,7 @@
    2.21        var all_sessions = false
    2.22        var dirs: List[Path] = Nil
    2.23        var session_groups: List[String] = Nil
    2.24 +      var incremental_update = false
    2.25        var options = Options.init()
    2.26        var verbose = false
    2.27        var exclude_sessions: List[String] = Nil
    2.28 @@ -241,6 +243,7 @@
    2.29      -a           select all sessions
    2.30      -d DIR       include session directory
    2.31      -g NAME      select session group NAME
    2.32 +    -i           incremental update according to session graph structure
    2.33      -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
    2.34      -v           verbose
    2.35      -x NAME      exclude session NAME and all descendants
    2.36 @@ -257,6 +260,7 @@
    2.37        "a" -> (_ => all_sessions = true),
    2.38        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
    2.39        "g:" -> (arg => session_groups = session_groups ::: List(arg)),
    2.40 +      "i" -> (_ => incremental_update = true),
    2.41        "o:" -> (arg => options = options + arg),
    2.42        "v" -> (_ => verbose = true),
    2.43        "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
    2.44 @@ -271,9 +275,25 @@
    2.45  
    2.46        val progress = new Console_Progress(verbose = verbose)
    2.47  
    2.48 -      imports(options, operation_imports = operation_imports,
    2.49 -        operation_repository_files = operation_repository_files, operation_update = operation_update,
    2.50 -        progress = progress, selection = selection, dirs = dirs, select_dirs = select_dirs,
    2.51 -        verbose = verbose)
    2.52 +      if (operation_imports || operation_repository_files ||
    2.53 +          operation_update && !incremental_update)
    2.54 +      {
    2.55 +        imports(options, operation_imports = operation_imports,
    2.56 +          operation_repository_files = operation_repository_files,
    2.57 +          operation_update = operation_update,
    2.58 +          progress = progress, selection = selection, dirs = dirs, select_dirs = select_dirs,
    2.59 +          verbose = verbose)
    2.60 +      }
    2.61 +      else if (operation_update && incremental_update) {
    2.62 +        val (selected, selected_sessions) =
    2.63 +          Sessions.load(options, dirs, select_dirs).selection(selection)
    2.64 +        selected_sessions.imports_topological_order.foreach(info =>
    2.65 +        {
    2.66 +          imports(options, operation_update = operation_update, progress = progress,
    2.67 +            update_message = " for session " + quote(info.name),
    2.68 +            selection = Sessions.Selection(sessions = List(info.name)),
    2.69 +            dirs = dirs ::: select_dirs, verbose = verbose)
    2.70 +        })
    2.71 +      }
    2.72      })
    2.73  }