# HG changeset patch
# User wenzelm
# Date 1672494860 -3600
# Node ID d431a9340163afb750323d36eb3974f440affe61
# Parent  4d19dc723a6dfc92e2da477648c5fd4911cfc0ba
more systematic Sessions.illegal_theory, based on File_Format.theory_excluded;

diff -r 4d19dc723a6d -r d431a9340163 src/Pure/Thy/bibtex.scala
--- 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
diff -r 4d19dc723a6d -r d431a9340163 src/Pure/Thy/file_format.scala
--- 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,
diff -r 4d19dc723a6d -r d431a9340163 src/Pure/Thy/sessions.scala
--- 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"
   }