--- a/src/Pure/Thy/export.scala Sun Aug 14 11:11:11 2022 +0100
+++ b/src/Pure/Thy/export.scala Sun Aug 14 18:38:40 2022 +0200
@@ -23,7 +23,6 @@
val DOCUMENT_CITATIONS = DOCUMENT_PREFIX + "citations"
val THEORY_PREFIX: String = "theory/"
val PROOFS_PREFIX: String = "proofs/"
- val THEORY_PARENTS: String = THEORY_PREFIX + "parents"
def explode_name(s: String): List[String] = space_explode('/', s)
def implode_name(elems: Iterable[String]): String = elems.mkString("/")
@@ -88,8 +87,7 @@
def read_theory_names(db: SQL.Database, session_name: String): List[String] = {
val select =
- Data.table.select(List(Data.theory_name),
- Data.where_equal(session_name, name = THEORY_PARENTS)) +
+ Data.table.select(List(Data.theory_name), Data.where_equal(session_name), distinct = true) +
" ORDER BY " + Data.theory_name
db.using_statement(select)(stmt =>
stmt.execute_query().iterator(_.string(Data.theory_name)).toList)
@@ -363,26 +361,27 @@
private def select[A](
session: String,
- select1: Entry_Name => Option[A],
- select2: Session_Database => List[A]
+ select: Session_Database => List[A],
+ project: Entry_Name => A,
+ sort_key: A => String
): List[A] = {
- def sel(name: String): List[A] =
+ def result(name: String): List[A] =
if (name == Sessions.DRAFT) {
(for {
snapshot <- document_snapshot.iterator
entry_name <- snapshot.all_exports.keysIterator
- res <- select1(entry_name).iterator
- } yield entry_name -> res).toList.sortBy(_._1.compound_name).map(_._2)
+ } yield project(entry_name)).toSet.toList.sortBy(sort_key)
}
- else { session_database(name).map(select2).getOrElse(Nil) }
- if (session.nonEmpty) sel(session) else session_stack.flatMap(sel)
+ else session_database(name).map(select).getOrElse(Nil)
+
+ if (session.nonEmpty) result(session) else session_stack.flatMap(result)
}
def entry_names(session: String = session_name): List[Entry_Name] =
- select(session, Some(_), _.entry_names)
+ select(session, _.entry_names, identity, _.compound_name)
def theory_names(session: String = session_name): List[String] =
- select(session, a => if(a.name == THEORY_PARENTS) Some(a.theory) else None, _.theory_names)
+ select(session, _.theory_names, _.theory, identity)
def get(theory: String, name: String): Option[Entry] =
{
--- a/src/Pure/Thy/export_theory.ML Sun Aug 14 11:11:11 2022 +0100
+++ b/src/Pure/Thy/export_theory.ML Sun Aug 14 18:38:40 2022 +0200
@@ -156,7 +156,7 @@
val parents = Theory.parents_of thy;
val _ =
Export.export thy \<^path_binding>\<open>theory/parents\<close>
- (XML.Encode.string (terminate_lines (map Context.theory_long_name parents)));
+ (XML.Encode.string (cat_lines (map Context.theory_long_name parents) ^ "\n"));
(* spec rules *)
--- a/src/Pure/Thy/export_theory.scala Sun Aug 14 11:11:11 2022 +0100
+++ b/src/Pure/Thy/export_theory.scala Sun Aug 14 18:38:40 2022 +0200
@@ -26,10 +26,11 @@
def read_session(
session_context: Export.Session_Context,
+ session_stack: Boolean = false,
progress: Progress = new Progress
): Session = {
val thys =
- for (theory <- session_context.theory_names()) yield {
+ for (theory <- theory_names(session_context, session_stack = session_stack)) yield {
progress.echo("Reading theory " + theory)
read_theory(session_context.theory(theory))
}
@@ -101,9 +102,20 @@
}
def read_theory_parents(theory_context: Export.Theory_Context): Option[List[String]] =
- theory_context.get(Export.THEORY_PARENTS)
+ theory_context.get(Export.THEORY_PREFIX + "parents")
.map(entry => Library.trim_split_lines(entry.uncompressed.text))
+ def theory_names(
+ session_context: Export.Session_Context,
+ session_stack: Boolean = false
+ ): List[String] = {
+ val session = if (session_stack) "" else session_context.session_name
+ for {
+ theory <- session_context.theory_names(session = session)
+ if read_theory_parents(session_context.theory(theory)).isDefined
+ } yield theory
+ }
+
def no_theory: Theory =
Theory("", Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Map.empty)
--- a/src/Pure/library.ML Sun Aug 14 11:11:11 2022 +0100
+++ b/src/Pure/library.ML Sun Aug 14 18:38:40 2022 +0200
@@ -145,7 +145,6 @@
val commas: string list -> string
val commas_quote: string list -> string
val cat_lines: string list -> string
- val terminate_lines: string list -> string
val space_explode: string -> string -> string list
val split_lines: string -> string list
val plain_words: string -> string
@@ -749,8 +748,6 @@
val cat_lines = space_implode "\n";
-fun terminate_lines lines = cat_lines lines ^ "\n";
-
(*space_explode "." "h.e..l.lo" = ["h", "e", "", "l", "lo"]*)
fun space_explode _ "" = []
| space_explode sep s = String.fields (fn c => str c = sep) s;
--- a/src/Pure/library.scala Sun Aug 14 11:11:11 2022 +0100
+++ b/src/Pure/library.scala Sun Aug 14 18:38:40 2022 +0200
@@ -94,8 +94,10 @@
/* lines */
- def terminate_lines(lines: IterableOnce[String]): String =
- lines.iterator.mkString("", "\n", "\n")
+ def terminate_lines(lines: IterableOnce[String]): String = {
+ val it = lines.iterator
+ if (it.isEmpty) "" else it.mkString("", "\n", "\n")
+ }
def cat_lines(lines: IterableOnce[String]): String =
lines.iterator.mkString("\n")