--- a/Admin/Release/CHECKLIST Sun Apr 23 14:53:35 2017 +0200
+++ b/Admin/Release/CHECKLIST Sun Apr 23 23:10:33 2017 +0200
@@ -11,6 +11,7 @@
- check sources:
isabelle check_sources '~~' '$AFP_BASE'
+ isabelle imports -M -a -d '~~/src/Benchmarks'
- check ANNOUNCE, README, NEWS, COPYRIGHT, CONTRIBUTORS;
--- a/NEWS Sun Apr 23 14:53:35 2017 +0200
+++ b/NEWS Sun Apr 23 23:10:33 2017 +0200
@@ -201,6 +201,13 @@
a negative value means the current state in the ML heap image remains
unchanged.
+* Command-line tool "isabelle imports" helps to maintain theory imports
+wrt. session structure. Examples:
+
+ isabelle imports -I -a
+ isabelle imports -U -a
+ isabelle imports -M -a -d '~~/src/Benchmarks'
+
New in Isabelle2016-1 (December 2016)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Induct/Infinitely_Branching_Tree.thy Sun Apr 23 23:10:33 2017 +0200
@@ -0,0 +1,108 @@
+(* Title: HOL/Induct/Infinitely_Branching_Tree.thy
+ Author: Stefan Berghofer, TU Muenchen
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+*)
+
+section \<open>Infinitely branching trees\<close>
+
+theory Infinitely_Branching_Tree
+imports Main
+begin
+
+datatype 'a tree =
+ Atom 'a
+ | Branch "nat \<Rightarrow> 'a tree"
+
+primrec map_tree :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a tree \<Rightarrow> 'b tree"
+ where
+ "map_tree f (Atom a) = Atom (f a)"
+ | "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
+
+lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
+ by (induct t) simp_all
+
+primrec exists_tree :: "('a \<Rightarrow> bool) \<Rightarrow> 'a tree \<Rightarrow> bool"
+ where
+ "exists_tree P (Atom a) = P a"
+ | "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
+
+lemma exists_map:
+ "(\<And>x. P x \<Longrightarrow> Q (f x)) \<Longrightarrow>
+ exists_tree P ts \<Longrightarrow> exists_tree Q (map_tree f ts)"
+ by (induct ts) auto
+
+
+subsection\<open>The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.\<close>
+
+datatype brouwer = Zero | Succ brouwer | Lim "nat \<Rightarrow> brouwer"
+
+text \<open>Addition of ordinals\<close>
+primrec add :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
+ where
+ "add i Zero = i"
+ | "add i (Succ j) = Succ (add i j)"
+ | "add i (Lim f) = Lim (\<lambda>n. add i (f n))"
+
+lemma add_assoc: "add (add i j) k = add i (add j k)"
+ by (induct k) auto
+
+text \<open>Multiplication of ordinals\<close>
+primrec mult :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
+ where
+ "mult i Zero = Zero"
+ | "mult i (Succ j) = add (mult i j) i"
+ | "mult i (Lim f) = Lim (\<lambda>n. mult i (f n))"
+
+lemma add_mult_distrib: "mult i (add j k) = add (mult i j) (mult i k)"
+ by (induct k) (auto simp add: add_assoc)
+
+lemma mult_assoc: "mult (mult i j) k = mult i (mult j k)"
+ by (induct k) (auto simp add: add_mult_distrib)
+
+text \<open>We could probably instantiate some axiomatic type classes and use
+ the standard infix operators.\<close>
+
+
+subsection \<open>A WF Ordering for The Brouwer ordinals (Michael Compton)\<close>
+
+text \<open>To use the function package we need an ordering on the Brouwer
+ ordinals. Start with a predecessor relation and form its transitive
+ closure.\<close>
+
+definition brouwer_pred :: "(brouwer \<times> brouwer) set"
+ where "brouwer_pred = (\<Union>i. {(m, n). n = Succ m \<or> (\<exists>f. n = Lim f \<and> m = f i)})"
+
+definition brouwer_order :: "(brouwer \<times> brouwer) set"
+ where "brouwer_order = brouwer_pred\<^sup>+"
+
+lemma wf_brouwer_pred: "wf brouwer_pred"
+ unfolding wf_def brouwer_pred_def
+ apply clarify
+ apply (induct_tac x)
+ apply blast+
+ done
+
+lemma wf_brouwer_order[simp]: "wf brouwer_order"
+ unfolding brouwer_order_def
+ by (rule wf_trancl[OF wf_brouwer_pred])
+
+lemma [simp]: "(j, Succ j) \<in> brouwer_order"
+ by (auto simp add: brouwer_order_def brouwer_pred_def)
+
+lemma [simp]: "(f n, Lim f) \<in> brouwer_order"
+ by (auto simp add: brouwer_order_def brouwer_pred_def)
+
+text \<open>Example of a general function\<close>
+function add2 :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
+ where
+ "add2 i Zero = i"
+ | "add2 i (Succ j) = Succ (add2 i j)"
+ | "add2 i (Lim f) = Lim (\<lambda>n. add2 i (f n))"
+ by pat_completeness auto
+termination
+ by (relation "inv_image brouwer_order snd") auto
+
+lemma add2_assoc: "add2 (add2 i j) k = add2 i (add2 j k)"
+ by (induct k) auto
+
+end
--- a/src/HOL/Induct/Tree.thy Sun Apr 23 14:53:35 2017 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,107 +0,0 @@
-(* Title: HOL/Induct/Tree.thy
- Author: Stefan Berghofer, TU Muenchen
- Author: Lawrence C Paulson, Cambridge University Computer Laboratory
-*)
-
-section \<open>Infinitely branching trees\<close>
-
-theory Tree
-imports Main
-begin
-
-datatype 'a tree =
- Atom 'a
- | Branch "nat \<Rightarrow> 'a tree"
-
-primrec map_tree :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a tree \<Rightarrow> 'b tree"
-where
- "map_tree f (Atom a) = Atom (f a)"
-| "map_tree f (Branch ts) = Branch (\<lambda>x. map_tree f (ts x))"
-
-lemma tree_map_compose: "map_tree g (map_tree f t) = map_tree (g \<circ> f) t"
- by (induct t) simp_all
-
-primrec exists_tree :: "('a \<Rightarrow> bool) \<Rightarrow> 'a tree \<Rightarrow> bool"
-where
- "exists_tree P (Atom a) = P a"
-| "exists_tree P (Branch ts) = (\<exists>x. exists_tree P (ts x))"
-
-lemma exists_map:
- "(\<And>x. P x \<Longrightarrow> Q (f x)) \<Longrightarrow>
- exists_tree P ts \<Longrightarrow> exists_tree Q (map_tree f ts)"
- by (induct ts) auto
-
-
-subsection\<open>The Brouwer ordinals, as in ZF/Induct/Brouwer.thy.\<close>
-
-datatype brouwer = Zero | Succ brouwer | Lim "nat \<Rightarrow> brouwer"
-
-text \<open>Addition of ordinals\<close>
-primrec add :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
-where
- "add i Zero = i"
-| "add i (Succ j) = Succ (add i j)"
-| "add i (Lim f) = Lim (\<lambda>n. add i (f n))"
-
-lemma add_assoc: "add (add i j) k = add i (add j k)"
- by (induct k) auto
-
-text \<open>Multiplication of ordinals\<close>
-primrec mult :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
-where
- "mult i Zero = Zero"
-| "mult i (Succ j) = add (mult i j) i"
-| "mult i (Lim f) = Lim (\<lambda>n. mult i (f n))"
-
-lemma add_mult_distrib: "mult i (add j k) = add (mult i j) (mult i k)"
- by (induct k) (auto simp add: add_assoc)
-
-lemma mult_assoc: "mult (mult i j) k = mult i (mult j k)"
- by (induct k) (auto simp add: add_mult_distrib)
-
-text \<open>We could probably instantiate some axiomatic type classes and use
- the standard infix operators.\<close>
-
-
-subsection \<open>A WF Ordering for The Brouwer ordinals (Michael Compton)\<close>
-
-text \<open>To use the function package we need an ordering on the Brouwer
- ordinals. Start with a predecessor relation and form its transitive
- closure.\<close>
-
-definition brouwer_pred :: "(brouwer \<times> brouwer) set"
- where "brouwer_pred = (\<Union>i. {(m, n). n = Succ m \<or> (\<exists>f. n = Lim f \<and> m = f i)})"
-
-definition brouwer_order :: "(brouwer \<times> brouwer) set"
- where "brouwer_order = brouwer_pred^+"
-
-lemma wf_brouwer_pred: "wf brouwer_pred"
- unfolding wf_def brouwer_pred_def
- apply clarify
- apply (induct_tac x)
- apply blast+
- done
-
-lemma wf_brouwer_order[simp]: "wf brouwer_order"
- unfolding brouwer_order_def
- by (rule wf_trancl[OF wf_brouwer_pred])
-
-lemma [simp]: "(j, Succ j) \<in> brouwer_order"
- by (auto simp add: brouwer_order_def brouwer_pred_def)
-
-lemma [simp]: "(f n, Lim f) \<in> brouwer_order"
- by (auto simp add: brouwer_order_def brouwer_pred_def)
-
-text \<open>Example of a general function\<close>
-function add2 :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
-where
- "add2 i Zero = i"
-| "add2 i (Succ j) = Succ (add2 i j)"
-| "add2 i (Lim f) = Lim (\<lambda>n. add2 i (f n))"
-by pat_completeness auto
-termination by (relation "inv_image brouwer_order snd") auto
-
-lemma add2_assoc: "add2 (add2 i j) k = add2 i (add2 j k)"
- by (induct k) auto
-
-end
--- a/src/HOL/ROOT Sun Apr 23 14:53:35 2017 +0200
+++ b/src/HOL/ROOT Sun Apr 23 23:10:33 2017 +0200
@@ -128,7 +128,7 @@
Term
SList
ABexp
- Tree
+ Infinitely_Branching_Tree
Ordinals
Sigma_Algebra
Comb
@@ -565,6 +565,7 @@
Bubblesort
CTL
Cartouche_Examples
+ Case_Product
Chinese
Classical
Code_Binary_Nat_examples
--- a/src/HOL/ex/Case_Product.thy Sun Apr 23 14:53:35 2017 +0200
+++ b/src/HOL/ex/Case_Product.thy Sun Apr 23 23:10:33 2017 +0200
@@ -10,21 +10,17 @@
begin
text \<open>
- The {@attribute case_product} attribute combines multiple case distinction
+ The @{attribute case_product} attribute combines multiple case distinction
lemmas into a single case distinction lemma by building the product of all
these case distinctions.
\<close>
-lemmas nat_list_exhaust = nat.exhaust[case_product list.exhaust]
+lemmas nat_list_exhaust = nat.exhaust [case_product list.exhaust]
-text \<open>
- The attribute honors preconditions
-\<close>
+text \<open>The attribute honours preconditions.\<close>
-lemmas trancl_acc_cases= trancl.cases[case_product acc.cases]
+lemmas trancl_acc_cases = trancl.cases [case_product acc.cases]
-text \<open>
- Also, case names are generated based on the old names
-\<close>
+text \<open>Also, case names are generated based on the old names.\<close>
end
--- a/src/Pure/General/mercurial.scala Sun Apr 23 14:53:35 2017 +0200
+++ b/src/Pure/General/mercurial.scala Sun Apr 23 23:10:33 2017 +0200
@@ -35,6 +35,19 @@
hg
}
+ def find_repository(start: Path, ssh: Option[SSH.Session] = None): Option[Repository] =
+ {
+ def find(root: Path): Option[Repository] =
+ if (is_repository(root, ssh)) Some(repository(root, ssh = ssh))
+ else if (root.is_root) None
+ else find(root + Path.parent)
+
+ ssh match {
+ case None => find(start.expand)
+ case Some(ssh) => find(ssh.expand_path(start))
+ }
+ }
+
def clone_repository(
source: String, root: Path, options: String = "", ssh: Option[SSH.Session] = None): Repository =
{
--- a/src/Pure/General/path.scala Sun Apr 23 14:53:35 2017 +0200
+++ b/src/Pure/General/path.scala Sun Apr 23 23:10:33 2017 +0200
@@ -119,6 +119,7 @@
{
def is_current: Boolean = elems.isEmpty
def is_absolute: Boolean = elems.nonEmpty && elems.last.isInstanceOf[Path.Root]
+ def is_root: Boolean = elems match { case List(Path.Root(_)) => true case _ => false }
def is_basic: Boolean = elems match { case List(Path.Basic(_)) => true case _ => false }
def +(other: Path): Path = new Path((other.elems :\ elems)(Path.apply_elem))
--- a/src/Pure/System/isabelle_tool.scala Sun Apr 23 14:53:35 2017 +0200
+++ b/src/Pure/System/isabelle_tool.scala Sun Apr 23 23:10:33 2017 +0200
@@ -108,6 +108,7 @@
Build_Stats.isabelle_tool,
Check_Sources.isabelle_tool,
Doc.isabelle_tool,
+ Imports.isabelle_tool,
ML_Process.isabelle_tool,
NEWS.isabelle_tool,
Options.isabelle_tool,
@@ -115,7 +116,6 @@
Remote_DMG.isabelle_tool,
Update_Cartouches.isabelle_tool,
Update_Header.isabelle_tool,
- Update_Imports.isabelle_tool,
Update_Then.isabelle_tool,
Update_Theorems.isabelle_tool,
isabelle.vscode.Build_VSCode.isabelle_tool,
--- a/src/Pure/Thy/sessions.scala Sun Apr 23 14:53:35 2017 +0200
+++ b/src/Pure/Thy/sessions.scala Sun Apr 23 23:10:33 2017 +0200
@@ -274,8 +274,7 @@
val selected_sessions = full_sessions.selection(Selection(sessions = List(session)))._2
if (all_known) {
- val deps = Sessions.deps(
- full_sessions, global_theories = global_theories, all_known = all_known)
+ val deps = Sessions.deps(full_sessions, global_theories = global_theories, all_known = true)
deps(session).copy(known = deps.all_known)
}
else
@@ -449,6 +448,9 @@
def build_topological_order: List[Info] =
build_graph.topological_order.map(apply(_))
+ def imports_ancestors(name: String): List[String] =
+ imports_graph.all_preds(List(name)).tail.reverse
+
def imports_topological_order: List[Info] =
imports_graph.topological_order.map(apply(_))
@@ -629,6 +631,12 @@
if (is_session_dir(dir)) File.pwd() + dir.expand
else error("Bad session root directory: " + dir.toString)
+ def directories(dirs: List[Path], select_dirs: List[Path]): List[(Boolean, Path)] =
+ {
+ val default_dirs = Isabelle_System.components().filter(is_session_dir(_))
+ (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
+ }
+
def load(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil): T =
{
def load_dir(select: Boolean, dir: Path): List[(String, Info)] =
@@ -656,11 +664,9 @@
else Nil
}
- val default_dirs = Isabelle_System.components().filter(is_session_dir(_))
-
make(
for {
- (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
+ (select, dir) <- directories(dirs, select_dirs)
info <- load_dir(select, check_session_dir(dir))
} yield info)
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/imports.scala Sun Apr 23 23:10:33 2017 +0200
@@ -0,0 +1,273 @@
+/* Title: Pure/Tools/imports.scala
+ Author: Makarius
+
+Maintain theory imports wrt. session structure.
+*/
+
+package isabelle
+
+
+import java.io.{File => JFile}
+
+
+object Imports
+{
+ /* manifest */
+
+ def manifest_files(start: Path, pred: JFile => Boolean = _ => true): List[JFile] =
+ Mercurial.find_repository(start) match {
+ case None =>
+ Output.warning("Ignoring directory " + start + " (no Mercurial repository)")
+ Nil
+ case Some(hg) =>
+ val start_path = start.file.getCanonicalFile.toPath
+ for {
+ name <- hg.manifest()
+ file = (hg.root + Path.explode(name)).file
+ if pred(file) && file.getCanonicalFile.toPath.startsWith(start_path)
+ } yield file
+ }
+
+
+ /* update imports */
+
+ sealed case class Update(range: Text.Range, old_text: String, new_text: String)
+ {
+ def edits: List[Text.Edit] =
+ Text.Edit.replace(range.start, old_text, new_text)
+
+ override def toString: String =
+ range.toString + ": " + old_text + " -> " + new_text
+ }
+
+ def update_name(keywords: Keyword.Keywords, pos: Position.T, update: String => String)
+ : Option[(JFile, Update)] =
+ {
+ val file =
+ pos match {
+ case Position.File(file) => Path.explode(file).file.getCanonicalFile
+ case _ => error("Missing file in position" + Position.here(pos))
+ }
+
+ val text = File.read(file)
+
+ val range =
+ pos match {
+ case Position.Range(symbol_range) => Symbol.Text_Chunk(text).decode(symbol_range)
+ case _ => error("Missing range in position" + Position.here(pos))
+ }
+
+ Token.read_name(keywords, range.substring(text)) match {
+ case Some(tok) =>
+ val s1 = tok.source
+ val s2 = Token.quote_name(keywords, update(tok.content))
+ if (s1 == s2) None else Some((file, Update(range, s1, s2)))
+ case None => error("Name token expected" + Position.here(pos))
+ }
+ }
+
+
+ /* collective operations */
+
+ def imports(
+ options: Options,
+ operation_imports: Boolean = false,
+ operation_manifest: Boolean = false,
+ operation_update: Boolean = false,
+ progress: Progress = No_Progress,
+ selection: Sessions.Selection = Sessions.Selection.empty,
+ dirs: List[Path] = Nil,
+ select_dirs: List[Path] = Nil,
+ verbose: Boolean = false) =
+ {
+ val full_sessions = Sessions.load(options, dirs, select_dirs)
+ val (selected, selected_sessions) = full_sessions.selection(selection)
+
+ val deps =
+ Sessions.deps(selected_sessions, progress = progress, verbose = verbose,
+ global_theories = full_sessions.global_theories,
+ all_known = true)
+
+ val root_keywords = Sessions.root_syntax.keywords
+
+
+ if (operation_imports) {
+ progress.echo("\nPotential session imports:")
+ selected.sorted.foreach(session_name =>
+ {
+ val info = full_sessions(session_name)
+ val session_resources = new Resources(deps(session_name))
+
+ val declared_imports =
+ full_sessions.imports_ancestors(session_name).toSet + session_name
+ val extra_imports =
+ (for {
+ (_, a) <- session_resources.session_base.known.theories.iterator
+ if session_resources.theory_qualifier(a) == info.theory_qualifier
+ b <- deps.all_known.get_file(Path.explode(a.node).file)
+ qualifier = session_resources.theory_qualifier(b)
+ if !declared_imports.contains(qualifier)
+ } yield qualifier).toSet
+
+ if (extra_imports.nonEmpty) {
+ progress.echo("session " + Token.quote_name(root_keywords, session_name) + ": " +
+ extra_imports.toList.sorted.map(Token.quote_name(root_keywords, _)).mkString(" "))
+ }
+ })
+ }
+
+ if (operation_manifest) {
+ progress.echo("\nManifest check:")
+ val unused_files =
+ for {
+ (_, dir) <- Sessions.directories(dirs, select_dirs)
+ file <- manifest_files(dir, file => file.getName.endsWith(".thy"))
+ if deps.all_known.get_file(file).isEmpty
+ } yield file
+ unused_files.foreach(file => progress.echo("unused file " + quote(file.toString)))
+ }
+
+ if (operation_update) {
+ progress.echo("\nUpdate theory imports:")
+ val updates =
+ selected.flatMap(session_name =>
+ {
+ val info = full_sessions(session_name)
+ val session_base = deps(session_name)
+ val session_resources = new Resources(session_base)
+ val imports_resources = new Resources(session_base.get_imports)
+
+ def standard_import(qualifier: String, dir: String, s: String): String =
+ {
+ val name = imports_resources.import_name(qualifier, dir, s)
+ val file = Path.explode(name.node).file
+ val s1 =
+ imports_resources.session_base.known.get_file(file) match {
+ case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
+ name1.theory
+ case Some(name1) if Thy_Header.is_base_name(s) =>
+ name1.theory_base_name
+ case _ => s
+ }
+ val name2 = imports_resources.import_name(qualifier, dir, s1)
+ if (name.node == name2.node) s1 else s
+ }
+
+ val updates_root =
+ for {
+ (_, pos) <- info.theories.flatMap(_._2)
+ upd <- update_name(root_keywords, pos,
+ standard_import(info.theory_qualifier, info.dir.implode, _))
+ } yield upd
+
+ val updates_theories =
+ for {
+ (_, name) <- session_base.known.theories_local.toList
+ (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
+ upd <- update_name(session_base.syntax.keywords, pos,
+ standard_import(session_resources.theory_qualifier(name), name.master_dir, _))
+ } yield upd
+
+ updates_root ::: updates_theories
+ })
+
+ val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _)
+ val conflicts =
+ file_updates.iterator_list.flatMap({ case (file, upds) =>
+ Library.duplicates(upds.sortBy(_.range.start),
+ (x: Update, y: Update) => x.range overlaps y.range) match
+ {
+ case Nil => None
+ case bad => Some((file, bad))
+ }
+ })
+ if (conflicts.nonEmpty)
+ error(cat_lines(
+ conflicts.map({ case (file, bad) =>
+ "Conflicting updates for file " + file + bad.mkString("\n ", "\n ", "") })))
+
+ for ((file, upds) <- file_updates.iterator_list.toList.sortBy(p => p._1.toString)) {
+ progress.echo("file " + quote(file.toString))
+ val edits =
+ upds.sortBy(upd => - upd.range.start).flatMap(upd =>
+ Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text))
+ val new_text =
+ (File.read(file) /: edits)({ case (text, edit) =>
+ edit.edit(text, 0) match {
+ case (None, text1) => text1
+ case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file)
+ }
+ })
+ File.write_backup2(Path.explode(File.standard_path(file)), new_text)
+ }
+ }
+ }
+
+
+ /* Isabelle tool wrapper */
+
+ val isabelle_tool =
+ Isabelle_Tool("imports", "maintain theory imports wrt. session structure", args =>
+ {
+ var select_dirs: List[Path] = Nil
+ var operation_imports = false
+ var operation_manifest = false
+ var requirements = false
+ var operation_update = false
+ var exclude_session_groups: List[String] = Nil
+ var all_sessions = false
+ var dirs: List[Path] = Nil
+ var session_groups: List[String] = Nil
+ var options = Options.init()
+ var verbose = false
+ var exclude_sessions: List[String] = Nil
+
+ val getopts = Getopts("""
+Usage: isabelle imports [OPTIONS] [SESSIONS ...]
+
+ Options are:
+ -D DIR include session directory and select its sessions
+ -I operation: report potential session imports
+ -M operation: Mercurial manifest check for imported theory files
+ -R operate on requirements of selected sessions
+ -U operation: update theory imports to use session qualifiers
+ -X NAME exclude sessions from group NAME and all descendants
+ -a select all sessions
+ -d DIR include session directory
+ -g NAME select session group NAME
+ -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
+ -v verbose
+ -x NAME exclude session NAME and all descendants
+
+ Maintain theory imports wrt. session structure. At least one operation
+ needs to be specified (see options -I -M -U).
+""",
+ "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
+ "I" -> (_ => operation_imports = true),
+ "M" -> (_ => operation_manifest = true),
+ "R" -> (_ => requirements = true),
+ "U" -> (_ => operation_update = true),
+ "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
+ "a" -> (_ => all_sessions = true),
+ "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
+ "g:" -> (arg => session_groups = session_groups ::: List(arg)),
+ "o:" -> (arg => options = options + arg),
+ "v" -> (_ => verbose = true),
+ "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
+
+ val sessions = getopts(args)
+ if (args.isEmpty || !(operation_imports || operation_manifest || operation_update))
+ getopts.usage()
+
+ val selection =
+ Sessions.Selection(requirements, all_sessions, exclude_session_groups,
+ exclude_sessions, session_groups, sessions)
+
+ val progress = new Console_Progress(verbose = verbose)
+
+ imports(options, operation_imports = operation_imports,
+ operation_manifest = operation_manifest, operation_update = operation_update,
+ progress = progress, selection = selection, dirs = dirs, select_dirs = select_dirs,
+ verbose = verbose)
+ })
+}
--- a/src/Pure/Tools/update_imports.scala Sun Apr 23 14:53:35 2017 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,206 +0,0 @@
-/* Title: Pure/Tools/update_imports.scala
- Author: Makarius
-
-Update theory imports to use session qualifiers.
-*/
-
-package isabelle
-
-
-import java.io.{File => JFile}
-
-
-object Update_Imports
-{
- /* update imports */
-
- sealed case class Update(range: Text.Range, old_text: String, new_text: String)
- {
- def edits: List[Text.Edit] =
- Text.Edit.replace(range.start, old_text, new_text)
-
- override def toString: String =
- range.toString + ": " + old_text + " -> " + new_text
- }
-
- def update_name(keywords: Keyword.Keywords, pos: Position.T, update: String => String)
- : Option[(JFile, Update)] =
- {
- val file =
- pos match {
- case Position.File(file) => Path.explode(file).file.getCanonicalFile
- case _ => error("Missing file in position" + Position.here(pos))
- }
-
- val text = File.read(file)
-
- val range =
- pos match {
- case Position.Range(symbol_range) => Symbol.Text_Chunk(text).decode(symbol_range)
- case _ => error("Missing range in position" + Position.here(pos))
- }
-
- Token.read_name(keywords, range.substring(text)) match {
- case Some(tok) =>
- val s1 = tok.source
- val s2 = Token.quote_name(keywords, update(tok.content))
- if (s1 == s2) None else Some((file, Update(range, s1, s2)))
- case None => error("Name token expected" + Position.here(pos))
- }
- }
-
- def update_imports(
- options: Options,
- progress: Progress = No_Progress,
- selection: Sessions.Selection = Sessions.Selection.empty,
- dirs: List[Path] = Nil,
- select_dirs: List[Path] = Nil,
- verbose: Boolean = false): List[(JFile, Update)] =
- {
- val full_sessions = Sessions.load(options, dirs, select_dirs)
- val (selected, selected_sessions) = full_sessions.selection(selection)
-
- val deps =
- Sessions.deps(selected_sessions, progress = progress, verbose = verbose,
- global_theories = full_sessions.global_theories)
-
- selected.flatMap(session_name =>
- {
- val info = full_sessions(session_name)
- val session_base = deps(session_name)
- val session_resources = new Resources(session_base)
- val imports_resources = new Resources(session_base.get_imports)
-
- val local_theories =
- (for {
- (_, name) <- session_base.known.theories_local.iterator
- if session_resources.theory_qualifier(name) == info.theory_qualifier
- } yield name).toSet
-
- def standard_import(qualifier: String, dir: String, s: String): String =
- {
- val name = imports_resources.import_name(qualifier, dir, s)
- val file = Path.explode(name.node).file
- val s1 =
- imports_resources.session_base.known.get_file(file) match {
- case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
- name1.theory
- case Some(name1) if Thy_Header.is_base_name(s) =>
- name1.theory_base_name
- case _ => s
- }
- val name2 = imports_resources.import_name(qualifier, dir, s1)
- if (name.node == name2.node) s1 else s
- }
-
- val updates_root =
- for {
- (_, pos) <- info.theories.flatMap(_._2)
- upd <- update_name(Sessions.root_syntax.keywords, pos,
- standard_import(info.theory_qualifier, info.dir.implode, _))
- } yield upd
-
- val updates_theories =
- for {
- (_, name) <- session_base.known.theories_local.toList
- (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
- upd <- update_name(session_base.syntax.keywords, pos,
- standard_import(session_resources.theory_qualifier(name), name.master_dir, _))
- } yield upd
-
- updates_root ::: updates_theories
- })
- }
-
- def apply_updates(updates: List[(JFile, Update)])
- {
- val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _)
- val conflicts =
- file_updates.iterator_list.flatMap({ case (file, upds) =>
- Library.duplicates(upds.sortBy(_.range.start),
- (x: Update, y: Update) => x.range overlaps y.range) match
- {
- case Nil => None
- case bad => Some((file, bad))
- }
- })
- if (conflicts.nonEmpty)
- error(cat_lines(
- conflicts.map({ case (file, bad) =>
- "Conflicting updates for file " + file + bad.mkString("\n ", "\n ", "") })))
-
- for ((file, upds) <- file_updates.iterator_list) {
- val edits =
- upds.sortBy(upd => - upd.range.start).flatMap(upd =>
- Text.Edit.replace(upd.range.start, upd.old_text, upd.new_text))
- val new_text =
- (File.read(file) /: edits)({ case (text, edit) =>
- edit.edit(text, 0) match {
- case (None, text1) => text1
- case (Some(_), _) => error("Failed to apply edit " + edit + " to file " + file)
- }
- })
- File.write_backup2(Path.explode(File.standard_path(file)), new_text)
- }
- }
-
-
- /* Isabelle tool wrapper */
-
- val isabelle_tool =
- Isabelle_Tool("update_imports", "update theory imports to use session qualifiers", args =>
- {
- var select_dirs: List[Path] = Nil
- var requirements = false
- var exclude_session_groups: List[String] = Nil
- var all_sessions = false
- var dirs: List[Path] = Nil
- var session_groups: List[String] = Nil
- var options = Options.init()
- var verbose = false
- var exclude_sessions: List[String] = Nil
-
- val getopts = Getopts("""
-Usage: isabelle update_imports [OPTIONS] [SESSIONS ...]
-
- Options are:
- -D DIR include session directory and select its sessions
- -R operate on requirements of selected sessions
- -X NAME exclude sessions from group NAME and all descendants
- -a select all sessions
- -d DIR include session directory
- -g NAME select session group NAME
- -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME)
- -v verbose
- -x NAME exclude session NAME and all descendants
-
- Update theory imports to use session qualifiers.
-
- Old versions of files are preserved by appending "~~".
-""",
- "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
- "R" -> (_ => requirements = true),
- "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
- "a" -> (_ => all_sessions = true),
- "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
- "g:" -> (arg => session_groups = session_groups ::: List(arg)),
- "o:" -> (arg => options = options + arg),
- "v" -> (_ => verbose = true),
- "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
-
- val sessions = getopts(args)
- if (args.isEmpty) getopts.usage()
-
- val selection =
- Sessions.Selection(requirements, all_sessions, exclude_session_groups,
- exclude_sessions, session_groups, sessions)
-
- val progress = new Console_Progress(verbose = verbose)
-
- val updates =
- update_imports(options, progress = progress, selection = selection,
- dirs = dirs, select_dirs = select_dirs, verbose = verbose)
-
- apply_updates(updates)
- })
-}
--- a/src/Pure/build-jars Sun Apr 23 14:53:35 2017 +0200
+++ b/src/Pure/build-jars Sun Apr 23 23:10:33 2017 +0200
@@ -135,6 +135,7 @@
Tools/check_keywords.scala
Tools/debugger.scala
Tools/doc.scala
+ Tools/imports.scala
Tools/main.scala
Tools/print_operation.scala
Tools/profiling_report.scala
@@ -143,7 +144,6 @@
Tools/task_statistics.scala
Tools/update_cartouches.scala
Tools/update_header.scala
- Tools/update_imports.scala
Tools/update_then.scala
Tools/update_theorems.scala
library.scala