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