--- a/src/HOL/Wfrec.thy Thu Nov 11 15:34:02 2021 +0100
+++ b/src/HOL/Wfrec.thy Fri Nov 12 00:28:00 2021 +0100
@@ -84,6 +84,9 @@
finally show "wfrec R F x = F (wfrec R F) x" .
qed
+lemma wfrec_def_adm: "f \<equiv> wfrec R F \<Longrightarrow> wf R \<Longrightarrow> adm_wf R F \<Longrightarrow> f = F f"
+ using wfrec_fixpoint by simp
+
subsection \<open>Wellfoundedness of \<open>same_fst\<close>\<close>
--- a/src/HOL/Zorn.thy Thu Nov 11 15:34:02 2021 +0100
+++ b/src/HOL/Zorn.thy Fri Nov 12 00:28:00 2021 +0100
@@ -4,10 +4,9 @@
Author: Christian Sternagel, JAIST
Zorn's Lemma (ported from Larry Paulson's Zorn.thy in ZF).
-The well-ordering theorem.
*)
-section \<open>Zorn's Lemma\<close>
+section \<open>Zorn's Lemma and the Well-ordering Theorem\<close>
theory Zorn
imports Order_Relation Hilbert_Choice
@@ -155,16 +154,8 @@
then show ?case
proof
assume "Y \<subseteq> X"
- with * and \<open>Y \<in> \<C>\<close> have "X = Y \<or> suc Y \<subseteq> X" by blast
- then show ?thesis
- proof
- assume "X = Y"
- then show ?thesis by simp
- next
- assume "suc Y \<subseteq> X"
- then have "suc Y \<subseteq> suc X" by (rule subset_suc)
- then show ?thesis by simp
- qed
+ with * and \<open>Y \<in> \<C>\<close> subset_suc show ?thesis
+ by fastforce
next
assume "suc X \<subseteq> Y"
with \<open>Y \<subseteq> suc X\<close> show ?thesis by blast
@@ -186,20 +177,11 @@
then show False
proof
assume "Y \<subseteq> x"
- with * [OF \<open>Y \<in> \<C>\<close>] have "x = Y \<or> suc Y \<subseteq> x" by blast
- then show False
- proof
- assume "x = Y"
- with \<open>y \<in> x\<close> and \<open>y \<notin> Y\<close> show False by blast
- next
- assume "suc Y \<subseteq> x"
- with \<open>x \<in> X\<close> have "suc Y \<subseteq> \<Union>X" by blast
- with \<open>\<not> suc Y \<subseteq> \<Union>X\<close> show False by contradiction
- qed
+ with * [OF \<open>Y \<in> \<C>\<close>] \<open>y \<in> x\<close> \<open>y \<notin> Y\<close> \<open>x \<in> X\<close> \<open>\<not> suc Y \<subseteq> \<Union>X\<close> show False
+ by blast
next
assume "suc x \<subseteq> Y"
- moreover from suc_subset and \<open>y \<in> x\<close> have "y \<in> suc x" by blast
- ultimately show False using \<open>y \<notin> Y\<close> by blast
+ with \<open>y \<notin> Y\<close> suc_subset \<open>y \<in> x\<close> show False by blast
qed
qed
qed
@@ -874,11 +856,6 @@
with 1 show ?thesis by auto
qed
-(* Move this to Hilbert Choice and wfrec to Wellfounded*)
-
-lemma wfrec_def_adm: "f \<equiv> wfrec R F \<Longrightarrow> wf R \<Longrightarrow> adm_wf R F \<Longrightarrow> f = F f"
- using wfrec_fixpoint by simp
-
lemma dependent_wf_choice:
fixes P :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
assumes "wf R"
@@ -894,7 +871,7 @@
show "P f x (f x)"
proof (subst (2) wfrec_def_adm[OF f_def \<open>wf R\<close>])
show "adm_wf R (\<lambda>f x. SOME r. P f x r)"
- by (auto simp add: adm_wf_def intro!: arg_cong[where f=Eps] ext adm)
+ by (auto simp: adm_wf_def intro!: arg_cong[where f=Eps] adm)
show "P f x (Eps (P f x))"
using P by (rule someI_ex) fact
qed
--- a/src/Pure/PIDE/document_status.scala Thu Nov 11 15:34:02 2021 +0100
+++ b/src/Pure/PIDE/document_status.scala Fri Nov 12 00:28:00 2021 +0100
@@ -268,7 +268,7 @@
val update_iterator =
for {
name <- domain.getOrElse(nodes1.domain).iterator
- if !resources.is_hidden(name) && !resources.session_base.loaded_theory(name)
+ if !Resources.hidden_node(name) && !resources.session_base.loaded_theory(name)
st = Document_Status.Node_Status.make(state, version, name)
if !rep.isDefinedAt(name) || rep(name) != st
} yield (name -> st)
--- a/src/Pure/PIDE/resources.scala Thu Nov 11 15:34:02 2021 +0100
+++ b/src/Pure/PIDE/resources.scala Fri Nov 12 00:28:00 2021 +0100
@@ -16,6 +16,15 @@
{
def empty: Resources =
new Resources(Sessions.Structure.empty, Sessions.Structure.empty.bootstrap)
+
+ def file_node(file: Path, dir: String = "", theory: String = ""): Document.Node.Name =
+ empty.file_node(file, dir = dir, theory = theory)
+
+ def hidden_node(name: Document.Node.Name): Boolean =
+ !name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name)
+
+ def html_document(snapshot: Document.Snapshot): Option[Presentation.HTML_Document] =
+ File_Format.registry.get(snapshot.node_name).flatMap(_.html_document(snapshot))
}
class Resources(
@@ -60,12 +69,6 @@
def make_theory_content(thy_name: Document.Node.Name): Option[String] =
File_Format.registry.get_theory(thy_name).flatMap(_.make_theory_content(resources, thy_name))
- def is_hidden(name: Document.Node.Name): Boolean =
- !name.is_theory || name.theory == Sessions.root_name || File_Format.registry.is_theory(name)
-
- def html_document(snapshot: Document.Snapshot): Option[Presentation.HTML_Document] =
- File_Format.registry.get(snapshot.node_name).flatMap(_.html_document(snapshot))
-
/* file-system operations */
--- a/src/Pure/Thy/html.scala Thu Nov 11 15:34:02 2021 +0100
+++ b/src/Pure/Thy/html.scala Fri Nov 12 00:28:00 2021 +0100
@@ -420,7 +420,8 @@
base match {
case None => ""
case Some(base_dir) =>
- File.path(dir.absolute.java_path.relativize(base_dir.absolute.java_path).toFile).implode
+ val path = File.path(dir.absolute.java_path.relativize(base_dir.absolute.java_path).toFile)
+ if (path.is_current) "" else path.implode + "/"
}
def isabelle_css: Path = Path.explode("~~/etc/isabelle.css")
--- a/src/Pure/Thy/presentation.scala Thu Nov 11 15:34:02 2021 +0100
+++ b/src/Pure/Thy/presentation.scala Fri Nov 12 00:28:00 2021 +0100
@@ -50,9 +50,6 @@
def source(body: XML.Body): XML.Tree = HTML.pre("source", body)
- def physical_ref(range: Text.Range): String =
- "offset_" + range.start + ".." + range.stop
-
def contents(heading: String, items: List[XML.Body], css_class: String = "contents")
: List[XML.Elem] =
{
@@ -97,9 +94,92 @@
type Entity = Export_Theory.Entity[Export_Theory.No_Content]
- case class Entity_Context(node: Document.Node.Name)
+ object Entity_Context
{
- val seen_ranges: mutable.Set[Symbol.Range] = mutable.Set.empty
+ val empty: Entity_Context = new Entity_Context
+
+ def make(
+ session: String,
+ deps: Sessions.Deps,
+ node: Document.Node.Name,
+ theory_exports: Map[String, Export_Theory.Theory]): Entity_Context =
+ new Entity_Context {
+ private val seen_ranges: mutable.Set[Symbol.Range] = mutable.Set.empty
+
+ override def make_def(range: Symbol.Range, body: XML.Body): Option[XML.Elem] =
+ {
+ body match {
+ case List(XML.Elem(Markup("span", List("id" -> _)), _)) => None
+ case _ =>
+ Some {
+ val entities =
+ theory_exports.get(node.theory).flatMap(_.entity_by_range.get(range))
+ .getOrElse(Nil)
+ val body1 =
+ if (seen_ranges.contains(range)) {
+ HTML.entity_def(HTML.span(HTML.id(offset_id(range)), body))
+ }
+ else HTML.span(body)
+ entities.map(_.kname).foldLeft(body1) {
+ case (elem, id) => HTML.entity_def(HTML.span(HTML.id(id), List(elem)))
+ }
+ }
+ }
+ }
+
+ private def offset_id(range: Text.Range): String =
+ "offset_" + range.start + ".." + range.stop
+
+ private def physical_ref(thy_name: String, props: Properties.T): Option[String] =
+ {
+ for {
+ range <- Position.Def_Range.unapply(props)
+ if thy_name == node.theory
+ } yield {
+ seen_ranges += range
+ offset_id(range)
+ }
+ }
+
+ private def logical_ref(thy_name: String, kind: String, name: String): Option[String] =
+ for {
+ thy <- theory_exports.get(thy_name)
+ entity <- thy.entity_by_kind_name.get((kind, name))
+ } yield entity.kname
+
+ override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] =
+ {
+ (props, props, props, props, props) match {
+ case (Markup.Kind(Markup.THEORY), Markup.Name(theory), Position.Def_File(thy_file), _, _) =>
+ val node_name = Resources.file_node(Path.explode(thy_file), theory = theory)
+ node_relative(deps, session, node_name).map(html_dir =>
+ HTML.link(html_dir + html_name(node_name), body))
+ case (Markup.Ref(_), Position.Def_File(def_file), Position.Def_Theory(def_theory),
+ Markup.Kind(kind), Markup.Name(name)) =>
+ val file_path = Path.explode(def_file)
+ val proper_thy_name =
+ proper_string(def_theory) orElse
+ (if (File.eq(node.path, file_path)) Some(node.theory) else None)
+ for {
+ thy_name <- proper_thy_name
+ node_name = Resources.file_node(file_path, theory = thy_name)
+ html_dir <- node_relative(deps, session, node_name)
+ html_file = node_file(node_name)
+ html_ref <-
+ logical_ref(thy_name, kind, name) orElse physical_ref(thy_name, props)
+ } yield {
+ HTML.entity_ref(HTML.link(html_dir + html_file + "#" + html_ref, body))
+ }
+ case _ => None
+ }
+ }
+ }
+ }
+
+ class Entity_Context
+ {
+ def make_def(range: Symbol.Range, body: XML.Body): Option[XML.Elem] = None
+ def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] = None
}
@@ -110,14 +190,10 @@
HTML.descr.name)
def make_html(
- name: Document.Node.Name,
+ entity_context: Entity_Context,
elements: Elements,
- entity_anchor: (Entity_Context, Symbol.Range, XML.Body) => Option[XML.Tree],
- entity_link: (Entity_Context, Properties.T, XML.Body) => Option[XML.Tree],
xml: XML.Body): XML.Body =
{
- val context = Entity_Context(name)
-
def html_div(html: XML.Body): Boolean =
html exists {
case XML.Elem(markup, body) => div_elements.contains(markup.name) || html_div(body)
@@ -142,7 +218,7 @@
case XML.Elem(Markup(Markup.ENTITY, props @ Markup.Kind(kind)), body) =>
val (body1, offset) = html_body(body, end_offset)
if (elements.entity(kind)) {
- entity_link(context, props, body1) match {
+ entity_context.make_ref(props, body1) match {
case Some(link) => (List(link), offset)
case None => (body1, offset)
}
@@ -180,7 +256,7 @@
case XML.Text(text) =>
val offset = end_offset - Symbol.length(text)
val body = HTML.text(Symbol.decode(text))
- entity_anchor(context, Text.Range(offset, end_offset), body) match {
+ entity_context.make_def(Text.Range(offset, end_offset), body) match {
case Some(body1) => (List(body1), offset)
case None => (body, offset)
}
@@ -193,7 +269,6 @@
/* PIDE HTML document */
def html_document(
- resources: Resources,
snapshot: Document.Snapshot,
html_context: HTML_Context,
elements: Elements,
@@ -209,12 +284,12 @@
html_context.html_document(title, body, fonts_css)
}
else {
- resources.html_document(snapshot) getOrElse {
+ Resources.html_document(snapshot) getOrElse {
val title =
if (name.is_theory) "Theory " + quote(name.theory_base_name)
else "File " + Symbol.cartouche_decoded(name.path.file_name)
val xml = snapshot.xml_markup(elements = elements.html)
- val body = make_html(name, elements, (_, _, _) => None, (_, _, _) => None, xml)
+ val body = make_html(Entity_Context.empty, elements, xml)
html_context.html_document(title, body, fonts_css)
}
}
@@ -345,7 +420,10 @@
def html_name(name: Document.Node.Name): String = Path.explode(name.theory_base_name).html.implode
def html_path(path: Path): String = (files_path + path.squash.html).implode
- def session_relative(deps: Sessions.Deps, session0: String, session1: String): Option[String] =
+ private def node_file(node: Document.Node.Name): String =
+ if (node.node.endsWith(".thy")) html_name(node) else html_path(Path.explode(node.node))
+
+ private def session_relative(deps: Sessions.Deps, session0: String, session1: String): Option[String] =
{
for {
info0 <- deps.sessions_structure.get(session0)
@@ -376,7 +454,6 @@
}
def session_html(
- resources: Resources,
session: String,
deps: Sessions.Deps,
db_context: Sessions.Database_Context,
@@ -455,6 +532,9 @@
thy_name -> theory
}).toMap
+ def entity_context(name: Document.Node.Name): Entity_Context =
+ Entity_Context.make(session, deps, name, theory_exports)
+
val theories: List[XML.Body] =
{
sealed case class Seen_File(
@@ -465,73 +545,6 @@
}
var seen_files = List.empty[Seen_File]
- def node_file(node: Document.Node.Name): String =
- if (node.node.endsWith(".thy")) html_name(node) else html_path(Path.explode(node.node))
-
- def entity_anchor(
- context: Entity_Context, range: Symbol.Range, body: XML.Body): Option[XML.Elem] =
- {
- body match {
- case List(XML.Elem(Markup("span", List("id" -> _)), _)) => None
- case _ =>
- Some {
- val entities =
- theory_exports.get(context.node.theory).flatMap(_.entity_by_range.get(range))
- .getOrElse(Nil)
- val body1 =
- if (context.seen_ranges.contains(range)) {
- HTML.entity_def(HTML.span(HTML.id(html_context.physical_ref(range)), body))
- }
- else HTML.span(body)
- entities.map(_.kname).foldLeft(body1) {
- case (elem, id) => HTML.entity_def(HTML.span(HTML.id(id), List(elem)))
- }
- }
- }
- }
-
- def logical_ref(thy_name: String, kind: String, name: String): Option[String] =
- for {
- thy <- theory_exports.get(thy_name)
- entity <- thy.entity_by_kind_name.get((kind, name))
- } yield entity.kname
-
- def physical_ref(
- context: Entity_Context, thy_name: String, props: Properties.T): Option[String] =
- {
- for {
- range <- Position.Def_Range.unapply(props)
- if thy_name == context.node.theory
- } yield {
- context.seen_ranges += range
- html_context.physical_ref(range)
- }
- }
-
- def entity_link(
- context: Entity_Context, props: Properties.T, body: XML.Body): Option[XML.Elem] =
- {
- (props, props, props, props, props) match {
- case (Markup.Kind(Markup.THEORY), Markup.Name(theory), Position.Def_File(thy_file), _, _) =>
- val node_name = resources.file_node(Path.explode(thy_file), theory = theory)
- node_relative(deps, session, node_name).map(html_dir =>
- HTML.link(html_dir + html_name(node_name), body))
- case (Markup.Ref(_), Position.Def_File(thy_file), Position.Def_Theory(def_theory),
- Markup.Kind(kind), Markup.Name(name)) =>
- val thy_name = if (def_theory.nonEmpty) def_theory else context.node.theory
- val node_name = resources.file_node(Path.explode(thy_file), theory = thy_name)
- for {
- html_dir <- node_relative(deps, session, node_name)
- html_file = node_file(node_name)
- html_ref <-
- logical_ref(thy_name, kind, name) orElse physical_ref(context, thy_name, props)
- } yield {
- HTML.entity_ref(HTML.link(html_dir + html_file + "#" + html_ref, body))
- }
- case _ => None
- }
- }
-
sealed case class Theory(
name: Document.Node.Name,
command: Command,
@@ -542,7 +555,7 @@
{
progress.expose_interrupt()
- for (command <- Build_Job.read_theory(db_context, resources, hierarchy, name.theory))
+ for (command <- Build_Job.read_theory(db_context, hierarchy, name.theory))
yield {
if (verbose) progress.echo("Presenting theory " + name)
val snapshot = Document.State.init.snippet(command)
@@ -561,12 +574,12 @@
if (verbose) progress.echo("Presenting file " + src_path)
(src_path, html_context.source(
- make_html(name, thy_elements, entity_anchor, entity_link, xml)))
+ make_html(entity_context(name), thy_elements, xml)))
}
val html =
html_context.source(
- make_html(name, thy_elements, entity_anchor, entity_link,
+ make_html(entity_context(name), thy_elements,
snapshot.xml_markup(elements = thy_elements.html)))
Theory(name, command, files_html, html)
--- a/src/Pure/Tools/build.scala Thu Nov 11 15:34:02 2021 +0100
+++ b/src/Pure/Tools/build.scala Fri Nov 12 00:28:00 2021 +0100
@@ -506,7 +506,6 @@
Presentation.update_chapter(presentation_dir, chapter, entries)
}
- val resources = Resources.empty
val html_context = Presentation.html_context(cache = store.cache)
using(store.open_database_context())(db_context =>
@@ -514,7 +513,7 @@
progress.expose_interrupt()
progress.echo("Presenting " + info.name + " ...")
Presentation.session_html(
- resources, info.name, deps, db_context, progress = progress,
+ info.name, deps, db_context, progress = progress,
verbose = verbose, html_context = html_context,
Presentation.elements1, presentation = presentation)
})
--- a/src/Pure/Tools/build_job.scala Thu Nov 11 15:34:02 2021 +0100
+++ b/src/Pure/Tools/build_job.scala Fri Nov 12 00:28:00 2021 +0100
@@ -18,7 +18,6 @@
def read_theory(
db_context: Sessions.Database_Context,
- resources: Resources,
session_hierarchy: List[String],
theory: String,
unicode_symbols: Boolean = false): Option[Command] =
@@ -33,7 +32,7 @@
(read(Export.DOCUMENT_ID).text, split_lines(read(Export.FILES).text)) match {
case (Value.Long(id), thy_file :: blobs_files) =>
- val node_name = resources.file_node(Path.explode(thy_file), theory = theory)
+ val node_name = Resources.file_node(Path.explode(thy_file), theory = theory)
val results =
Command.Results.make(
@@ -44,7 +43,7 @@
blobs_files.map(file =>
{
val path = Path.explode(file)
- val name = resources.file_node(path)
+ val name = Resources.file_node(path)
val src_path = File.relative_path(node_name.master_dir_path, path).getOrElse(path)
Command.Blob(name, src_path, None)
})
@@ -95,8 +94,7 @@
unicode_symbols: Boolean = false): Unit =
{
val store = Sessions.store(options)
- val resources = Resources.empty
- val session = new Session(options, resources)
+ val session = new Session(options, Resources.empty)
using(store.open_database_context())(db_context =>
{
@@ -118,8 +116,7 @@
if (theories.isEmpty) used_theories else used_theories.filter(theories.toSet)
for (thy <- print_theories) {
val thy_heading = "\nTheory " + quote(thy) + ":"
- read_theory(db_context, resources, List(session_name), thy,
- unicode_symbols = unicode_symbols)
+ read_theory(db_context, List(session_name), thy, unicode_symbols = unicode_symbols)
match {
case None => progress.echo(thy_heading + " MISSING")
case Some(command) =>
--- a/src/Pure/Tools/profiling_report.scala Thu Nov 11 15:34:02 2021 +0100
+++ b/src/Pure/Tools/profiling_report.scala Fri Nov 12 00:28:00 2021 +0100
@@ -17,7 +17,6 @@
progress: Progress = new Progress): Unit =
{
val store = Sessions.store(options)
- val resources = Resources.empty
using(store.open_database_context())(db_context =>
{
@@ -34,7 +33,7 @@
(for {
thy <- used_theories.iterator
if theories.isEmpty || theories.contains(thy)
- command <- Build_Job.read_theory(db_context, resources, List(session), thy).iterator
+ command <- Build_Job.read_theory(db_context, List(session), thy).iterator
snapshot = Document.State.init.snippet(command)
(Protocol.ML_Profiling(report), _) <- snapshot.messages.iterator
} yield if (clean_name) report.clean_name else report).toList
--- a/src/Tools/VSCode/src/preview_panel.scala Thu Nov 11 15:34:02 2021 +0100
+++ b/src/Tools/VSCode/src/preview_panel.scala Fri Nov 12 00:28:00 2021 +0100
@@ -33,8 +33,7 @@
else {
val html_context = Presentation.html_context()
val document =
- Presentation.html_document(
- resources, snapshot, html_context, Presentation.elements2)
+ Presentation.html_document(snapshot, html_context, Presentation.elements2)
channel.write(LSP.Preview_Response(file, column, document.title, document.content))
m - file
}
--- a/src/Tools/jEdit/src/document_model.scala Thu Nov 11 15:34:02 2021 +0100
+++ b/src/Tools/jEdit/src/document_model.scala Fri Nov 12 00:28:00 2021 +0100
@@ -327,7 +327,7 @@
val html_context = Presentation.html_context()
val document =
Presentation.html_document(
- PIDE.resources, snapshot, html_context, Presentation.elements2,
+ snapshot, html_context, Presentation.elements2,
plain_text = query.startsWith(plain_text_prefix),
fonts_css = HTML.fonts_css_dir(http_root))
HTTP.Response.html(document.content)