author | wenzelm |
Sun, 17 Sep 2017 17:37:40 +0200 | |
changeset 66671 | 41b64e53b6a1 |
parent 66575 | 191048506504 |
child 66716 | 8737b866bd1c |
permissions | -rw-r--r-- |
65557 | 1 |
/* Title: Pure/Tools/imports.scala |
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
3 |
|
65557 | 4 |
Maintain theory imports wrt. session structure. |
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
5 |
*/ |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
6 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
7 |
package isabelle |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
8 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
9 |
|
65526 | 10 |
import java.io.{File => JFile} |
11 |
||
12 |
||
65557 | 13 |
object Imports |
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
14 |
{ |
65824 | 15 |
/* repository files */ |
65561 | 16 |
|
65830 | 17 |
def repository_files(progress: Progress, start: Path, pred: JFile => Boolean = _ => true) |
18 |
: List[JFile] = |
|
65561 | 19 |
Mercurial.find_repository(start) match { |
20 |
case None => |
|
65830 | 21 |
progress.echo_warning("Ignoring directory " + start + " (no Mercurial repository)") |
65561 | 22 |
Nil |
23 |
case Some(hg) => |
|
65833 | 24 |
val start_path = start.canonical_file.toPath |
65561 | 25 |
for { |
65824 | 26 |
name <- hg.known_files() |
65561 | 27 |
file = (hg.root + Path.explode(name)).file |
66234 | 28 |
if pred(file) && File.canonical(file).toPath.startsWith(start_path) |
65561 | 29 |
} yield file |
30 |
} |
|
31 |
||
32 |
||
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
33 |
/* update imports */ |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
34 |
|
65526 | 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 { |
|
65833 | 49 |
case Position.File(file) => Path.explode(file).canonical_file |
65526 | 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 |
||
65561 | 70 |
|
71 |
/* collective operations */ |
|
72 |
||
65558 | 73 |
def imports( |
74 |
options: Options, |
|
65566 | 75 |
operation_imports: Boolean = false, |
65824 | 76 |
operation_repository_files: Boolean = false, |
65558 | 77 |
operation_update: Boolean = false, |
66449
1be102db1598
support for incremental update according to session graph structure;
wenzelm
parents:
66234
diff
changeset
|
78 |
update_message: String = "", |
65558 | 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, |
|
66575
191048506504
clarified signature: provide all_known information uniformly (it is subject to Sessions.T selection);
wenzelm
parents:
66571
diff
changeset
|
90 |
global_theories = full_sessions.global_theories).check_errors |
65561 | 91 |
|
65566 | 92 |
val root_keywords = Sessions.root_syntax.keywords |
93 |
||
94 |
||
95 |
if (operation_imports) { |
|
96 |
progress.echo("\nPotential session imports:") |
|
66033 | 97 |
selected.flatMap(session_name => |
65566 | 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 |
||
66033 | 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(" ")) |
|
65566 | 118 |
}) |
119 |
} |
|
120 |
||
65824 | 121 |
if (operation_repository_files) { |
66671 | 122 |
progress.echo("\nMercurial repository check:") |
65561 | 123 |
val unused_files = |
124 |
for { |
|
125 |
(_, dir) <- Sessions.directories(dirs, select_dirs) |
|
65830 | 126 |
file <- repository_files(progress, dir, file => file.getName.endsWith(".thy")) |
65561 | 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 |
} |
|
65558 | 131 |
|
132 |
if (operation_update) { |
|
66449
1be102db1598
support for incremental update according to session graph structure;
wenzelm
parents:
66234
diff
changeset
|
133 |
progress.echo("\nUpdate theory imports" + update_message + ":") |
65558 | 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) |
|
66028 | 140 |
val imports_base = session_base.get_imports |
141 |
val imports_resources = new Resources(imports_base) |
|
65558 | 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 = |
|
66029 | 147 |
if (imports_base.loaded_theory(name)) name.theory |
66025 | 148 |
else { |
66028 | 149 |
imports_base.known.get_file(Path.explode(name.node).file) match { |
66025 | 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 |
} |
|
65558 | 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) |
|
65566 | 164 |
upd <- update_name(root_keywords, pos, |
65558 | 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 |
|
66030 | 171 |
if session_resources.theory_qualifier(name) == info.theory_qualifier |
65558 | 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 |
}) |
|
65564 | 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 |
||
65566 | 195 |
for ((file, upds) <- file_updates.iterator_list.toList.sortBy(p => p._1.toString)) { |
65564 | 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 |
} |
|
65558 | 209 |
} |
210 |
} |
|
211 |
||
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
212 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
213 |
/* Isabelle tool wrapper */ |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
214 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
215 |
val isabelle_tool = |
65557 | 216 |
Isabelle_Tool("imports", "maintain theory imports wrt. session structure", args => |
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
217 |
{ |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
218 |
var select_dirs: List[Path] = Nil |
65566 | 219 |
var operation_imports = false |
65824 | 220 |
var operation_repository_files = false |
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
221 |
var requirements = false |
65558 | 222 |
var operation_update = false |
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
223 |
var exclude_session_groups: List[String] = Nil |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
224 |
var all_sessions = false |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
225 |
var dirs: List[Path] = Nil |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
226 |
var session_groups: List[String] = Nil |
66449
1be102db1598
support for incremental update according to session graph structure;
wenzelm
parents:
66234
diff
changeset
|
227 |
var incremental_update = false |
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
228 |
var options = Options.init() |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
229 |
var verbose = false |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
230 |
var exclude_sessions: List[String] = Nil |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
231 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
232 |
val getopts = Getopts(""" |
65557 | 233 |
Usage: isabelle imports [OPTIONS] [SESSIONS ...] |
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
234 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
235 |
Options are: |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
236 |
-D DIR include session directory and select its sessions |
65566 | 237 |
-I operation: report potential session imports |
66671 | 238 |
-M operation: Mercurial repository check for theory files |
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
239 |
-R operate on requirements of selected sessions |
65558 | 240 |
-U operation: update theory imports to use session qualifiers |
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
241 |
-X NAME exclude sessions from group NAME and all descendants |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
242 |
-a select all sessions |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
243 |
-d DIR include session directory |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
244 |
-g NAME select session group NAME |
66449
1be102db1598
support for incremental update according to session graph structure;
wenzelm
parents:
66234
diff
changeset
|
245 |
-i incremental update according to session graph structure |
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
246 |
-o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
247 |
-v verbose |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
248 |
-x NAME exclude session NAME and all descendants |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
249 |
|
65558 | 250 |
Maintain theory imports wrt. session structure. At least one operation |
65566 | 251 |
needs to be specified (see options -I -M -U). |
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
252 |
""", |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
253 |
"D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), |
65566 | 254 |
"I" -> (_ => operation_imports = true), |
65824 | 255 |
"M" -> (_ => operation_repository_files = true), |
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
256 |
"R" -> (_ => requirements = true), |
65558 | 257 |
"U" -> (_ => operation_update = true), |
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
258 |
"X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
259 |
"a" -> (_ => all_sessions = true), |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
260 |
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
261 |
"g:" -> (arg => session_groups = session_groups ::: List(arg)), |
66449
1be102db1598
support for incremental update according to session graph structure;
wenzelm
parents:
66234
diff
changeset
|
262 |
"i" -> (_ => incremental_update = true), |
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
263 |
"o:" -> (arg => options = options + arg), |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
264 |
"v" -> (_ => verbose = true), |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
265 |
"x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
266 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
267 |
val sessions = getopts(args) |
65824 | 268 |
if (args.isEmpty || !(operation_imports || operation_repository_files || operation_update)) |
65561 | 269 |
getopts.usage() |
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
270 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
271 |
val selection = |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
272 |
Sessions.Selection(requirements, all_sessions, exclude_session_groups, |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
273 |
exclude_sessions, session_groups, sessions) |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
274 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
275 |
val progress = new Console_Progress(verbose = verbose) |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
276 |
|
66449
1be102db1598
support for incremental update according to session graph structure;
wenzelm
parents:
66234
diff
changeset
|
277 |
if (operation_imports || operation_repository_files || |
1be102db1598
support for incremental update according to session graph structure;
wenzelm
parents:
66234
diff
changeset
|
278 |
operation_update && !incremental_update) |
1be102db1598
support for incremental update according to session graph structure;
wenzelm
parents:
66234
diff
changeset
|
279 |
{ |
1be102db1598
support for incremental update according to session graph structure;
wenzelm
parents:
66234
diff
changeset
|
280 |
imports(options, operation_imports = operation_imports, |
1be102db1598
support for incremental update according to session graph structure;
wenzelm
parents:
66234
diff
changeset
|
281 |
operation_repository_files = operation_repository_files, |
1be102db1598
support for incremental update according to session graph structure;
wenzelm
parents:
66234
diff
changeset
|
282 |
operation_update = operation_update, |
1be102db1598
support for incremental update according to session graph structure;
wenzelm
parents:
66234
diff
changeset
|
283 |
progress = progress, selection = selection, dirs = dirs, select_dirs = select_dirs, |
1be102db1598
support for incremental update according to session graph structure;
wenzelm
parents:
66234
diff
changeset
|
284 |
verbose = verbose) |
1be102db1598
support for incremental update according to session graph structure;
wenzelm
parents:
66234
diff
changeset
|
285 |
} |
1be102db1598
support for incremental update according to session graph structure;
wenzelm
parents:
66234
diff
changeset
|
286 |
else if (operation_update && incremental_update) { |
1be102db1598
support for incremental update according to session graph structure;
wenzelm
parents:
66234
diff
changeset
|
287 |
val (selected, selected_sessions) = |
1be102db1598
support for incremental update according to session graph structure;
wenzelm
parents:
66234
diff
changeset
|
288 |
Sessions.load(options, dirs, select_dirs).selection(selection) |
1be102db1598
support for incremental update according to session graph structure;
wenzelm
parents:
66234
diff
changeset
|
289 |
selected_sessions.imports_topological_order.foreach(info => |
1be102db1598
support for incremental update according to session graph structure;
wenzelm
parents:
66234
diff
changeset
|
290 |
{ |
1be102db1598
support for incremental update according to session graph structure;
wenzelm
parents:
66234
diff
changeset
|
291 |
imports(options, operation_update = operation_update, progress = progress, |
1be102db1598
support for incremental update according to session graph structure;
wenzelm
parents:
66234
diff
changeset
|
292 |
update_message = " for session " + quote(info.name), |
1be102db1598
support for incremental update according to session graph structure;
wenzelm
parents:
66234
diff
changeset
|
293 |
selection = Sessions.Selection(sessions = List(info.name)), |
1be102db1598
support for incremental update according to session graph structure;
wenzelm
parents:
66234
diff
changeset
|
294 |
dirs = dirs ::: select_dirs, verbose = verbose) |
1be102db1598
support for incremental update according to session graph structure;
wenzelm
parents:
66234
diff
changeset
|
295 |
}) |
1be102db1598
support for incremental update according to session graph structure;
wenzelm
parents:
66234
diff
changeset
|
296 |
} |
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
297 |
}) |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
298 |
} |