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