author | wenzelm |
Sun, 23 Apr 2017 15:59:51 +0200 | |
changeset 65557 | 29c69a599743 |
parent 65542 | src/Pure/Tools/update_imports.scala@6a00518bbfcc |
child 65558 | 479406635409 |
permissions | -rw-r--r-- |
65557 | 1 |
/* Title: Pure/Tools/imports.scala |
65518
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 |
|
65557 | 4 |
Maintain theory imports wrt. session structure. |
65518
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 |
||
65557 | 13 |
object Imports |
65518
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) |
|
65540
2b73ed8bf4d9
proper imports_resources for import_name: avoid self-referential name resolution;
wenzelm
parents:
65539
diff
changeset
|
71 |
val session_resources = new Resources(session_base) |
2b73ed8bf4d9
proper imports_resources for import_name: avoid self-referential name resolution;
wenzelm
parents:
65539
diff
changeset
|
72 |
val imports_resources = new Resources(session_base.get_imports) |
2b73ed8bf4d9
proper imports_resources for import_name: avoid self-referential name resolution;
wenzelm
parents:
65539
diff
changeset
|
73 |
|
65534
b6250ee6ce79
clarified local_theories: exclude ancestor sessions;
wenzelm
parents:
65533
diff
changeset
|
74 |
val local_theories = |
b6250ee6ce79
clarified local_theories: exclude ancestor sessions;
wenzelm
parents:
65533
diff
changeset
|
75 |
(for { |
b6250ee6ce79
clarified local_theories: exclude ancestor sessions;
wenzelm
parents:
65533
diff
changeset
|
76 |
(_, name) <- session_base.known.theories_local.iterator |
65540
2b73ed8bf4d9
proper imports_resources for import_name: avoid self-referential name resolution;
wenzelm
parents:
65539
diff
changeset
|
77 |
if session_resources.theory_qualifier(name) == info.theory_qualifier |
65534
b6250ee6ce79
clarified local_theories: exclude ancestor sessions;
wenzelm
parents:
65533
diff
changeset
|
78 |
} yield name).toSet |
65526 | 79 |
|
65533 | 80 |
def standard_import(qualifier: String, dir: String, s: String): String = |
65526 | 81 |
{ |
65540
2b73ed8bf4d9
proper imports_resources for import_name: avoid self-referential name resolution;
wenzelm
parents:
65539
diff
changeset
|
82 |
val name = imports_resources.import_name(qualifier, dir, s) |
65542
6a00518bbfcc
clarified standard_import: based on Known.get_file as in PIDE editors;
wenzelm
parents:
65540
diff
changeset
|
83 |
val file = Path.explode(name.node).file |
65536 | 84 |
val s1 = |
65542
6a00518bbfcc
clarified standard_import: based on Known.get_file as in PIDE editors;
wenzelm
parents:
65540
diff
changeset
|
85 |
imports_resources.session_base.known.get_file(file) match { |
6a00518bbfcc
clarified standard_import: based on Known.get_file as in PIDE editors;
wenzelm
parents:
65540
diff
changeset
|
86 |
case Some(name1) if session_resources.theory_qualifier(name1) != qualifier => |
6a00518bbfcc
clarified standard_import: based on Known.get_file as in PIDE editors;
wenzelm
parents:
65540
diff
changeset
|
87 |
name1.theory |
6a00518bbfcc
clarified standard_import: based on Known.get_file as in PIDE editors;
wenzelm
parents:
65540
diff
changeset
|
88 |
case Some(name1) if Thy_Header.is_base_name(s) => |
6a00518bbfcc
clarified standard_import: based on Known.get_file as in PIDE editors;
wenzelm
parents:
65540
diff
changeset
|
89 |
name1.theory_base_name |
6a00518bbfcc
clarified standard_import: based on Known.get_file as in PIDE editors;
wenzelm
parents:
65540
diff
changeset
|
90 |
case _ => s |
6a00518bbfcc
clarified standard_import: based on Known.get_file as in PIDE editors;
wenzelm
parents:
65540
diff
changeset
|
91 |
} |
6a00518bbfcc
clarified standard_import: based on Known.get_file as in PIDE editors;
wenzelm
parents:
65540
diff
changeset
|
92 |
val name2 = imports_resources.import_name(qualifier, dir, s1) |
6a00518bbfcc
clarified standard_import: based on Known.get_file as in PIDE editors;
wenzelm
parents:
65540
diff
changeset
|
93 |
if (name.node == name2.node) s1 else s |
65526 | 94 |
} |
95 |
||
96 |
val updates_root = |
|
97 |
for { |
|
98 |
(_, pos) <- info.theories.flatMap(_._2) |
|
99 |
upd <- update_name(Sessions.root_syntax.keywords, pos, |
|
65533 | 100 |
standard_import(info.theory_qualifier, info.dir.implode, _)) |
65526 | 101 |
} yield upd |
102 |
||
103 |
val updates_theories = |
|
104 |
for { |
|
105 |
(_, name) <- session_base.known.theories_local.toList |
|
65540
2b73ed8bf4d9
proper imports_resources for import_name: avoid self-referential name resolution;
wenzelm
parents:
65539
diff
changeset
|
106 |
(_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports |
65526 | 107 |
upd <- update_name(session_base.syntax.keywords, pos, |
65540
2b73ed8bf4d9
proper imports_resources for import_name: avoid self-referential name resolution;
wenzelm
parents:
65539
diff
changeset
|
108 |
standard_import(session_resources.theory_qualifier(name), name.master_dir, _)) |
65526 | 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 |
}) |
|
65537 | 143 |
File.write_backup2(Path.explode(File.standard_path(file)), new_text) |
65526 | 144 |
} |
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
145 |
} |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
146 |
|
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 |
/* Isabelle tool wrapper */ |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
149 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
150 |
val isabelle_tool = |
65557 | 151 |
Isabelle_Tool("imports", "maintain theory imports wrt. session structure", args => |
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
152 |
{ |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
153 |
var select_dirs: List[Path] = Nil |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
154 |
var requirements = false |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
155 |
var exclude_session_groups: List[String] = Nil |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
156 |
var all_sessions = false |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
157 |
var dirs: List[Path] = Nil |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
158 |
var session_groups: List[String] = Nil |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
159 |
var options = Options.init() |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
160 |
var verbose = false |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
161 |
var exclude_sessions: List[String] = Nil |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
162 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
163 |
val getopts = Getopts(""" |
65557 | 164 |
Usage: isabelle imports [OPTIONS] [SESSIONS ...] |
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
165 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
166 |
Options are: |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
167 |
-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
|
168 |
-R operate on requirements of selected sessions |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
169 |
-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
|
170 |
-a select all sessions |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
171 |
-d DIR include session directory |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
172 |
-g NAME select session group NAME |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
173 |
-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
|
174 |
-v verbose |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
175 |
-x NAME exclude session NAME and all descendants |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
176 |
|
65557 | 177 |
Maintain theory imports wrt. session structure. |
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
178 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
179 |
Old versions of files are preserved by appending "~~". |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
180 |
""", |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
181 |
"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
|
182 |
"R" -> (_ => requirements = true), |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
183 |
"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
|
184 |
"a" -> (_ => all_sessions = true), |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
185 |
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
186 |
"g:" -> (arg => session_groups = session_groups ::: List(arg)), |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
187 |
"o:" -> (arg => options = options + arg), |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
188 |
"v" -> (_ => verbose = true), |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
189 |
"x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg))) |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
190 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
191 |
val sessions = getopts(args) |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
192 |
if (args.isEmpty) getopts.usage() |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
193 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
194 |
val selection = |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
195 |
Sessions.Selection(requirements, all_sessions, exclude_session_groups, |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
196 |
exclude_sessions, session_groups, sessions) |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
197 |
|
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
198 |
val progress = new Console_Progress(verbose = verbose) |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
199 |
|
65526 | 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) |
|
65518
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
205 |
}) |
bc8fa59211b7
wrapper for "isabelle update_imports" with selection options like "isabelle build";
wenzelm
parents:
diff
changeset
|
206 |
} |