# 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" }