--- a/src/Pure/Thy/bibtex.scala Sat Dec 31 12:38:48 2022 +0100
+++ b/src/Pure/Thy/bibtex.scala Sat Dec 31 14:54:20 2022 +0100
@@ -28,6 +28,7 @@
override def theory_content(name: String): String =
"""theory "bib" imports Pure begin bibtex_file """ +
Outer_Syntax.quote_string(name) + """ end"""
+ override def theory_excluded(name: String): Boolean = name == "bib"
override def html_document(snapshot: Document.Snapshot): Option[Browser_Info.HTML_Document] = {
val name = snapshot.node_name
--- a/src/Pure/Thy/file_format.scala Sat Dec 31 12:38:48 2022 +0100
+++ b/src/Pure/Thy/file_format.scala Sat Dec 31 14:54:20 2022 +0100
@@ -28,6 +28,8 @@
def get_theory(name: Document.Node.Name): Option[File_Format] = get(name.theory)
def is_theory(name: Document.Node.Name): Boolean = get_theory(name).isDefined
+ def theory_excluded(name: String): Boolean = file_formats.exists(_.theory_excluded(name))
+
def parse_data(name: String, text: String): AnyRef =
get(name) match {
case Some(file_format) => file_format.parse_data(name, text)
@@ -74,6 +76,7 @@
def theory_suffix: String = ""
def theory_content(name: String): String = ""
+ def theory_excluded(name: String): Boolean = false
def make_theory_name(
resources: Resources,
--- a/src/Pure/Thy/sessions.scala Sat Dec 31 12:38:48 2022 +0100
+++ b/src/Pure/Thy/sessions.scala Sat Dec 31 14:54:20 2022 +0100
@@ -32,7 +32,8 @@
def is_pure(name: String): Boolean = name == Thy_Header.PURE
def illegal_session(name: String): Boolean = name == "" || name == DRAFT
- def illegal_theory(name: String): Boolean = name == root_name || name == "bib"
+ def illegal_theory(name: String): Boolean =
+ name == root_name || isabelle.File_Format.registry.theory_excluded(name)
/* ROOTS file format */
@@ -51,6 +52,7 @@
override def theory_content(name: String): String =
"""theory "ROOTS" imports Pure begin ROOTS_file """ +
Outer_Syntax.quote_string(name) + """ end"""
+ override def theory_excluded(name: String): Boolean = name == "ROOTS"
}