author | wenzelm |
Fri, 21 Apr 2017 15:26:24 +0200 | |
changeset 65534 | b6250ee6ce79 |
parent 65533 | 4a7e794944df |
child 65536 | 23c2450ae027 |
permissions | -rw-r--r-- |
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Pure/Tools/update_imports.scala |
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 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
4 |
Update theory imports to use session qualifiers. |
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 |
||
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
13 |
object Update_Imports |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
14 |
{ |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
15 |
/* update imports */ |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
16 |
|
65526 | 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 |
||
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
52 |
def update_imports( |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
53 |
options: Options, |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
54 |
progress: Progress = No_Progress, |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
55 |
selection: Sessions.Selection = Sessions.Selection.empty, |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
56 |
dirs: List[Path] = Nil, |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
57 |
select_dirs: List[Path] = Nil, |
65526 | 58 |
verbose: Boolean = false): List[(JFile, Update)] = |
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
59 |
{ |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
60 |
val full_sessions = Sessions.load(options, dirs, select_dirs) |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
61 |
val (selected, selected_sessions) = full_sessions.selection(selection) |
65526 | 62 |
|
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
63 |
val deps = |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
64 |
Sessions.deps(selected_sessions, progress = progress, verbose = verbose, |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
65 |
global_theories = full_sessions.global_theories) |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
66 |
|
65526 | 67 |
selected.flatMap(session_name => |
68 |
{ |
|
69 |
val info = full_sessions(session_name) |
|
70 |
val session_base = deps(session_name) |
|
65532 | 71 |
val resources = new Resources(session_base) |
65534
b6250ee6ce79
clarified local_theories: exclude ancestor sessions;
wenzelm
parents:
65533
diff
changeset
|
72 |
val local_theories = |
b6250ee6ce79
clarified local_theories: exclude ancestor sessions;
wenzelm
parents:
65533
diff
changeset
|
73 |
(for { |
b6250ee6ce79
clarified local_theories: exclude ancestor sessions;
wenzelm
parents:
65533
diff
changeset
|
74 |
(_, name) <- session_base.known.theories_local.iterator |
b6250ee6ce79
clarified local_theories: exclude ancestor sessions;
wenzelm
parents:
65533
diff
changeset
|
75 |
if resources.theory_qualifier(name) == info.theory_qualifier |
b6250ee6ce79
clarified local_theories: exclude ancestor sessions;
wenzelm
parents:
65533
diff
changeset
|
76 |
} yield name).toSet |
65526 | 77 |
|
65533 | 78 |
def standard_import(qualifier: String, dir: String, s: String): String = |
65526 | 79 |
{ |
65533 | 80 |
val name = resources.import_name(qualifier, dir, s) |
65526 | 81 |
if (!local_theories.contains(name)) s |
82 |
if (resources.theory_qualifier(name) != qualifier) name.theory |
|
83 |
else if (Thy_Header.is_base_name(s)) name.theory_base_name |
|
84 |
else s |
|
85 |
} |
|
86 |
||
87 |
val updates_root = |
|
88 |
for { |
|
89 |
(_, pos) <- info.theories.flatMap(_._2) |
|
90 |
upd <- update_name(Sessions.root_syntax.keywords, pos, |
|
65533 | 91 |
standard_import(info.theory_qualifier, info.dir.implode, _)) |
65526 | 92 |
} yield upd |
93 |
||
94 |
val updates_theories = |
|
95 |
for { |
|
96 |
(_, name) <- session_base.known.theories_local.toList |
|
97 |
(_, pos) <- |
|
98 |
// FIXME proper UTF8 positions for check_thy |
|
99 |
resources.check_thy_reader(name, |
|
100 |
Scan.char_reader(File.read(Path.explode(name.node))), |
|
101 |
Token.Pos.file(name.node)).imports |
|
102 |
upd <- update_name(session_base.syntax.keywords, pos, |
|
65533 | 103 |
standard_import(resources.theory_qualifier(name), name.master_dir, _)) |
65526 | 104 |
} yield upd |
105 |
||
106 |
updates_root ::: updates_theories |
|
107 |
}) |
|
108 |
} |
|
109 |
||
110 |
def apply_updates(updates: List[(JFile, Update)]) |
|
111 |
{ |
|
112 |
val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _) |
|
113 |
val conflicts = |
|
114 |
file_updates.iterator_list.flatMap({ case (file, upds) => |
|
115 |
Library.duplicates(upds.sortBy(_.range.start), |
|
116 |
(x: Update, y: Update) => x.range overlaps y.range) match |
|
117 |
{ |
|
118 |
case Nil => None |
|
119 |
case bad => Some((file, bad)) |
|
120 |
} |
|
121 |
}) |
|
122 |
if (conflicts.nonEmpty) |
|
123 |
error(cat_lines( |
|
124 |
conflicts.map({ case (file, bad) => |
|
125 |
"Conflicting updates for file " + file + bad.mkString("\n ", "\n ", "") }))) |
|
126 |
||
127 |
for ((file, upds) <- file_updates.iterator_list) { |
|
128 |
val edits = |
|
129 |
upds.sortBy(upd => - upd.range.start).flatMap(upd => |
|
130 |
Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text)) |
|
131 |
val new_text = |
|
132 |
(File.read(file) /: edits)({ case (text, edit) => |
|
133 |
edit.edit(text, 0) match { |
|
134 |
case (None, text1) => text1 |
|
135 |
case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file) |
|
136 |
} |
|
137 |
}) |
|
138 |
File.write_backup(Path.explode(File.standard_path(file)), new_text) |
|
139 |
} |
|
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
140 |
} |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
141 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
142 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
143 |
/* Isabelle tool wrapper */ |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
144 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
145 |
val isabelle_tool = |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
146 |
Isabelle_Tool("update_imports", "update theory imports to use session qualifiers", args => |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
147 |
{ |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
148 |
var select_dirs: List[Path] = Nil |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
149 |
var requirements = false |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
150 |
var exclude_session_groups: List[String] = Nil |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
151 |
var all_sessions = false |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
152 |
var dirs: List[Path] = Nil |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
153 |
var session_groups: List[String] = Nil |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
154 |
var options = Options.init() |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
155 |
var verbose = false |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
156 |
var exclude_sessions: List[String] = Nil |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
157 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
158 |
val getopts = Getopts(""" |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
159 |
Usage: isabelle update_imports [OPTIONS] [SESSIONS ...] |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
160 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
161 |
Options are: |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
162 |
-D DIR include session directory and select its sessions |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
163 |
-R operate on requirements of selected sessions |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
164 |
-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
|
165 |
-a select all sessions |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
166 |
-d DIR include session directory |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
167 |
-g NAME select session group NAME |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
168 |
-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
|
169 |
-v verbose |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
170 |
-x NAME exclude session NAME and all descendants |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
171 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
172 |
Update theory imports to use session qualifiers. |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
173 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
174 |
Old versions of files are preserved by appending "~~". |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
175 |
""", |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
176 |
"D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
177 |
"R" -> (_ => requirements = true), |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
178 |
"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
|
179 |
"a" -> (_ => all_sessions = true), |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
180 |
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
181 |
"g:" -> (arg => session_groups = session_groups ::: List(arg)), |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
182 |
"o:" -> (arg => options = options + arg), |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
183 |
"v" -> (_ => verbose = true), |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
184 |
"x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
185 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
186 |
val sessions = getopts(args) |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
187 |
if (args.isEmpty) getopts.usage() |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
188 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
189 |
val selection = |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
190 |
Sessions.Selection(requirements, all_sessions, exclude_session_groups, |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
191 |
exclude_sessions, session_groups, sessions) |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
192 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
193 |
val progress = new Console_Progress(verbose = verbose) |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
194 |
|
65526 | 195 |
val updates = |
196 |
update_imports(options, progress = progress, selection = selection, |
|
197 |
dirs = dirs, select_dirs = select_dirs, verbose = verbose) |
|
198 |
||
199 |
apply_updates(updates) |
|
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
200 |
}) |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
201 |
} |