|
1 /* Title: Pure/Tools/update.scala |
|
2 Author: Makarius |
|
3 |
|
4 Update theory sources based on PIDE markup. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 object Update |
|
11 { |
|
12 def update(options: Options, logic: String, |
|
13 progress: Progress = No_Progress, |
|
14 log: Logger = No_Logger, |
|
15 dirs: List[Path] = Nil, |
|
16 select_dirs: List[Path] = Nil, |
|
17 system_mode: Boolean = false, |
|
18 selection: Sessions.Selection = Sessions.Selection.empty) |
|
19 { |
|
20 Build.build_logic(options, logic, build_heap = true, progress = progress, |
|
21 dirs = dirs ::: select_dirs, system_mode = system_mode, strict = true) |
|
22 |
|
23 val dump_options = Dump.make_options(options) |
|
24 |
|
25 val deps = |
|
26 Dump.dependencies(dump_options, progress = progress, |
|
27 dirs = dirs, select_dirs = select_dirs, selection = selection)._1 |
|
28 |
|
29 val resources = |
|
30 Headless.Resources.make(dump_options, logic, progress = progress, log = log, |
|
31 session_dirs = dirs ::: select_dirs, |
|
32 include_sessions = deps.sessions_structure.imports_topological_order) |
|
33 |
|
34 def update_xml(xml: XML.Body): XML.Body = |
|
35 xml flatMap { |
|
36 case XML.Wrapped_Elem(markup, body1, body2) => |
|
37 if (markup.name == Markup.UPDATE) update_xml(body1) else update_xml(body2) |
|
38 case XML.Elem(_, body) => update_xml(body) |
|
39 case t => List(t) |
|
40 } |
|
41 |
|
42 Dump.session(deps, resources, progress = progress, |
|
43 process_theory = |
|
44 (deps: Sessions.Deps, snapshot: Document.Snapshot, status: Document_Status.Node_Status) => |
|
45 { |
|
46 for ((node_name, node) <- snapshot.nodes) { |
|
47 val xml = |
|
48 snapshot.state.markup_to_XML(snapshot.version, node_name, |
|
49 Text.Range.full, Markup.Elements(Markup.UPDATE)) |
|
50 |
|
51 val source1 = Symbol.encode(XML.content(update_xml(xml))) |
|
52 if (source1 != Symbol.encode(node.source)) { |
|
53 progress.echo("Updating " + node_name.path) |
|
54 File.write(node_name.path, source1) |
|
55 } |
|
56 } |
|
57 }) |
|
58 } |
|
59 |
|
60 |
|
61 /* Isabelle tool wrapper */ |
|
62 |
|
63 val isabelle_tool = |
|
64 Isabelle_Tool("update", "update theory sources based on PIDE markup", args => |
|
65 { |
|
66 var base_sessions: List[String] = Nil |
|
67 var select_dirs: List[Path] = Nil |
|
68 var requirements = false |
|
69 var exclude_session_groups: List[String] = Nil |
|
70 var all_sessions = false |
|
71 var dirs: List[Path] = Nil |
|
72 var session_groups: List[String] = Nil |
|
73 var logic = Isabelle_System.getenv("ISABELLE_LOGIC") |
|
74 var options = Options.init() |
|
75 var system_mode = false |
|
76 var verbose = false |
|
77 var exclude_sessions: List[String] = Nil |
|
78 |
|
79 val getopts = Getopts(""" |
|
80 Usage: isabelle update [OPTIONS] [SESSIONS ...] |
|
81 |
|
82 Options are: |
|
83 -B NAME include session NAME and all descendants |
|
84 -D DIR include session directory and select its sessions |
|
85 -R operate on requirements of selected sessions |
|
86 -X NAME exclude sessions from group NAME and all descendants |
|
87 -a select all sessions |
|
88 -d DIR include session directory |
|
89 -g NAME select session group NAME |
|
90 -l NAME logic session name (default ISABELLE_LOGIC=""" + quote(logic) + """) |
|
91 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
92 -s system build mode for logic image |
|
93 -u OPT overide update option: shortcut for "-o update_OPT" |
|
94 -v verbose |
|
95 -x NAME exclude session NAME and all descendants |
|
96 |
|
97 Update theory sources based on PIDE markup. |
|
98 """, |
|
99 "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), |
|
100 "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), |
|
101 "R" -> (_ => requirements = true), |
|
102 "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), |
|
103 "a" -> (_ => all_sessions = true), |
|
104 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
|
105 "g:" -> (arg => session_groups = session_groups ::: List(arg)), |
|
106 "l:" -> (arg => logic = arg), |
|
107 "o:" -> (arg => options = options + arg), |
|
108 "s" -> (_ => system_mode = true), |
|
109 "u:" -> (arg => options = options + ("update_" + arg)), |
|
110 "v" -> (_ => verbose = true), |
|
111 "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) |
|
112 |
|
113 val sessions = getopts(args) |
|
114 |
|
115 val progress = new Console_Progress(verbose = verbose) |
|
116 |
|
117 progress.interrupt_handler { |
|
118 update(options, logic, |
|
119 progress = progress, |
|
120 dirs = dirs, |
|
121 select_dirs = select_dirs, |
|
122 selection = Sessions.Selection( |
|
123 requirements = requirements, |
|
124 all_sessions = all_sessions, |
|
125 base_sessions = base_sessions, |
|
126 exclude_session_groups = exclude_session_groups, |
|
127 exclude_sessions = exclude_sessions, |
|
128 session_groups = session_groups, |
|
129 sessions = sessions)) |
|
130 } |
|
131 }) |
|
132 } |