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 import java.io.{File => JFile} |
|
11 |
|
12 |
|
13 object Update_Imports |
|
14 { |
|
15 /* update imports */ |
|
16 |
|
17 sealed case class Update(range: Text.Range, old_text: String, new_text: String) |
|
18 { |
|
19 def edits: List[Text.Edit] = |
|
20 Text.Edit.replace(range.start, old_text, new_text) |
|
21 |
|
22 override def toString: String = |
|
23 range.toString + ": " + old_text + " -> " + new_text |
|
24 } |
|
25 |
|
26 def update_name(keywords: Keyword.Keywords, pos: Position.T, update: String => String) |
|
27 : Option[(JFile, Update)] = |
|
28 { |
|
29 val file = |
|
30 pos match { |
|
31 case Position.File(file) => Path.explode(file).file.getCanonicalFile |
|
32 case _ => error("Missing file in position" + Position.here(pos)) |
|
33 } |
|
34 |
|
35 val text = File.read(file) |
|
36 |
|
37 val range = |
|
38 pos match { |
|
39 case Position.Range(symbol_range) => Symbol.Text_Chunk(text).decode(symbol_range) |
|
40 case _ => error("Missing range in position" + Position.here(pos)) |
|
41 } |
|
42 |
|
43 Token.read_name(keywords, range.substring(text)) match { |
|
44 case Some(tok) => |
|
45 val s1 = tok.source |
|
46 val s2 = Token.quote_name(keywords, update(tok.content)) |
|
47 if (s1 == s2) None else Some((file, Update(range, s1, s2))) |
|
48 case None => error("Name token expected" + Position.here(pos)) |
|
49 } |
|
50 } |
|
51 |
|
52 def update_imports( |
|
53 options: Options, |
|
54 progress: Progress = No_Progress, |
|
55 selection: Sessions.Selection = Sessions.Selection.empty, |
|
56 dirs: List[Path] = Nil, |
|
57 select_dirs: List[Path] = Nil, |
|
58 verbose: Boolean = false): List[(JFile, Update)] = |
|
59 { |
|
60 val full_sessions = Sessions.load(options, dirs, select_dirs) |
|
61 val (selected, selected_sessions) = full_sessions.selection(selection) |
|
62 |
|
63 val deps = |
|
64 Sessions.deps(selected_sessions, progress = progress, verbose = verbose, |
|
65 global_theories = full_sessions.global_theories) |
|
66 |
|
67 selected.flatMap(session_name => |
|
68 { |
|
69 val info = full_sessions(session_name) |
|
70 val session_base = deps(session_name) |
|
71 val session_resources = new Resources(session_base) |
|
72 val imports_resources = new Resources(session_base.get_imports) |
|
73 |
|
74 val local_theories = |
|
75 (for { |
|
76 (_, name) <- session_base.known.theories_local.iterator |
|
77 if session_resources.theory_qualifier(name) == info.theory_qualifier |
|
78 } yield name).toSet |
|
79 |
|
80 def standard_import(qualifier: String, dir: String, s: String): String = |
|
81 { |
|
82 val name = imports_resources.import_name(qualifier, dir, s) |
|
83 val file = Path.explode(name.node).file |
|
84 val s1 = |
|
85 imports_resources.session_base.known.get_file(file) match { |
|
86 case Some(name1) if session_resources.theory_qualifier(name1) != qualifier => |
|
87 name1.theory |
|
88 case Some(name1) if Thy_Header.is_base_name(s) => |
|
89 name1.theory_base_name |
|
90 case _ => s |
|
91 } |
|
92 val name2 = imports_resources.import_name(qualifier, dir, s1) |
|
93 if (name.node == name2.node) s1 else s |
|
94 } |
|
95 |
|
96 val updates_root = |
|
97 for { |
|
98 (_, pos) <- info.theories.flatMap(_._2) |
|
99 upd <- update_name(Sessions.root_syntax.keywords, pos, |
|
100 standard_import(info.theory_qualifier, info.dir.implode, _)) |
|
101 } yield upd |
|
102 |
|
103 val updates_theories = |
|
104 for { |
|
105 (_, name) <- session_base.known.theories_local.toList |
|
106 (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports |
|
107 upd <- update_name(session_base.syntax.keywords, pos, |
|
108 standard_import(session_resources.theory_qualifier(name), name.master_dir, _)) |
|
109 } yield upd |
|
110 |
|
111 updates_root ::: updates_theories |
|
112 }) |
|
113 } |
|
114 |
|
115 def apply_updates(updates: List[(JFile, Update)]) |
|
116 { |
|
117 val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _) |
|
118 val conflicts = |
|
119 file_updates.iterator_list.flatMap({ case (file, upds) => |
|
120 Library.duplicates(upds.sortBy(_.range.start), |
|
121 (x: Update, y: Update) => x.range overlaps y.range) match |
|
122 { |
|
123 case Nil => None |
|
124 case bad => Some((file, bad)) |
|
125 } |
|
126 }) |
|
127 if (conflicts.nonEmpty) |
|
128 error(cat_lines( |
|
129 conflicts.map({ case (file, bad) => |
|
130 "Conflicting updates for file " + file + bad.mkString("\n ", "\n ", "") }))) |
|
131 |
|
132 for ((file, upds) <- file_updates.iterator_list) { |
|
133 val edits = |
|
134 upds.sortBy(upd => - upd.range.start).flatMap(upd => |
|
135 Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text)) |
|
136 val new_text = |
|
137 (File.read(file) /: edits)({ case (text, edit) => |
|
138 edit.edit(text, 0) match { |
|
139 case (None, text1) => text1 |
|
140 case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file) |
|
141 } |
|
142 }) |
|
143 File.write_backup2(Path.explode(File.standard_path(file)), new_text) |
|
144 } |
|
145 } |
|
146 |
|
147 |
|
148 /* Isabelle tool wrapper */ |
|
149 |
|
150 val isabelle_tool = |
|
151 Isabelle_Tool("update_imports", "update theory imports to use session qualifiers", args => |
|
152 { |
|
153 var select_dirs: List[Path] = Nil |
|
154 var requirements = false |
|
155 var exclude_session_groups: List[String] = Nil |
|
156 var all_sessions = false |
|
157 var dirs: List[Path] = Nil |
|
158 var session_groups: List[String] = Nil |
|
159 var options = Options.init() |
|
160 var verbose = false |
|
161 var exclude_sessions: List[String] = Nil |
|
162 |
|
163 val getopts = Getopts(""" |
|
164 Usage: isabelle update_imports [OPTIONS] [SESSIONS ...] |
|
165 |
|
166 Options are: |
|
167 -D DIR include session directory and select its sessions |
|
168 -R operate on requirements of selected sessions |
|
169 -X NAME exclude sessions from group NAME and all descendants |
|
170 -a select all sessions |
|
171 -d DIR include session directory |
|
172 -g NAME select session group NAME |
|
173 -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) |
|
174 -v verbose |
|
175 -x NAME exclude session NAME and all descendants |
|
176 |
|
177 Update theory imports to use session qualifiers. |
|
178 |
|
179 Old versions of files are preserved by appending "~~". |
|
180 """, |
|
181 "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), |
|
182 "R" -> (_ => requirements = true), |
|
183 "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), |
|
184 "a" -> (_ => all_sessions = true), |
|
185 "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
|
186 "g:" -> (arg => session_groups = session_groups ::: List(arg)), |
|
187 "o:" -> (arg => options = options + arg), |
|
188 "v" -> (_ => verbose = true), |
|
189 "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) |
|
190 |
|
191 val sessions = getopts(args) |
|
192 if (args.isEmpty) getopts.usage() |
|
193 |
|
194 val selection = |
|
195 Sessions.Selection(requirements, all_sessions, exclude_session_groups, |
|
196 exclude_sessions, session_groups, sessions) |
|
197 |
|
198 val progress = new Console_Progress(verbose = verbose) |
|
199 |
|
200 val updates = |
|
201 update_imports(options, progress = progress, selection = selection, |
|
202 dirs = dirs, select_dirs = select_dirs, verbose = verbose) |
|
203 |
|
204 apply_updates(updates) |
|
205 }) |
|
206 } |
|