--- a/src/Pure/Admin/build_doc.scala Thu Dec 22 21:55:51 2022 +0100
+++ b/src/Pure/Admin/build_doc.scala Fri Dec 23 12:14:10 2022 +0100
@@ -43,8 +43,7 @@
if (!build_results.ok) error("Build failed")
progress.echo("Build started for documentation " + commas_quote(documents))
- val doc_options = options + "document=pdf"
- val deps = Sessions.load_structure(doc_options).selection_deps(selection)
+ val deps = Sessions.load_structure(options + "document").selection_deps(selection)
val errs =
Par_List.map[(String, String), Option[String]](
--- a/src/Pure/PIDE/document_editor.scala Thu Dec 22 21:55:51 2022 +0100
+++ b/src/Pure/PIDE/document_editor.scala Fri Dec 23 12:14:10 2022 +0100
@@ -50,12 +50,6 @@
) {
def is_active: Boolean = session_background.isDefined && views.nonEmpty
- def is_required(name: Document.Node.Name): Boolean =
- is_active && selection.contains(name) && all_document_theories.contains(name)
-
- def required: List[Document.Node.Name] =
- if (is_active) all_document_theories.filter(selection) else Nil
-
def all_document_theories: List[Document.Node.Name] =
session_background match {
case Some(background) => background.base.all_document_theories
--- a/src/Pure/PIDE/editor.scala Thu Dec 22 21:55:51 2022 +0100
+++ b/src/Pure/PIDE/editor.scala Fri Dec 23 12:14:10 2022 +0100
@@ -29,17 +29,36 @@
val st1 = f(st)
val changed =
st.active_document_theories != st1.active_document_theories ||
- st.required != st1.required
+ st.selection != st1.selection
(changed, st1)
}
if (changed) document_state_changed()
}
def document_session(): Option[Sessions.Background] = document_state().session_background
- def document_required(): List[Document.Node.Name] = document_state().required
- def document_node_required(name: Document.Node.Name): Boolean = document_state().is_required(name)
- def document_theories(): List[Document.Node.Name] = document_state().active_document_theories
+ def document_required(): List[Document.Node.Name] = {
+ val st = document_state()
+ if (st.is_active) {
+ for {
+ a <- st.all_document_theories
+ b = session.resources.migrate_name(a)
+ if st.selection(b)
+ } yield b
+ }
+ else Nil
+ }
+
+ def document_node_required(name: Document.Node.Name): Boolean = {
+ val st = document_state()
+ st.is_active &&
+ st.selection.contains(name) &&
+ st.all_document_theories.exists(a => session.resources.migrate_name(a) == name)
+ }
+
+ def document_theories(): List[Document.Node.Name] =
+ document_state().active_document_theories.map(session.resources.migrate_name)
+
def document_selection(): Set[Document.Node.Name] = document_state().selection
def document_setup(background: Option[Sessions.Background]): Unit =
@@ -52,7 +71,10 @@
): Unit = document_state_change(_.select(names, set = set, toggle = toggle))
def document_select_all(set: Boolean = false): Unit =
- document_state_change(st => st.select(st.active_document_theories, set = set))
+ document_state_change { st =>
+ val domain = st.active_document_theories.map(session.resources.migrate_name)
+ st.select(domain, set = set)
+ }
def document_init(id: AnyRef): Unit = document_state_change(_.register_view(id))
def document_exit(id: AnyRef): Unit = document_state_change(_.unregister_view(id))
--- a/src/Pure/PIDE/resources.scala Thu Dec 22 21:55:51 2022 +0100
+++ b/src/Pure/PIDE/resources.scala Fri Dec 23 12:14:10 2022 +0100
@@ -70,6 +70,8 @@
/* file-system operations */
+ def migrate_name(name: Document.Node.Name): Document.Node.Name = name
+
def append(dir: String, source_path: Path): String =
(Path.explode(dir) + source_path).expand.implode
--- a/src/Pure/Thy/document_build.scala Thu Dec 22 21:55:51 2022 +0100
+++ b/src/Pure/Thy/document_build.scala Fri Dec 23 12:14:10 2022 +0100
@@ -118,7 +118,7 @@
progress: Progress = new Progress,
verbose: Boolean = false
): Sessions.Background = {
- Sessions.load_structure(options + "document=pdf", dirs = dirs).
+ Sessions.load_structure(options + "document", dirs = dirs).
selection_deps(Sessions.Selection.session(session), progress = progress, verbose = verbose).
background(session)
}
@@ -185,7 +185,7 @@
def session_document_theories: List[Document.Node.Name] = base.proper_session_theories
def all_document_theories: List[Document.Node.Name] = base.all_document_theories
- lazy val document_latex: List[File.Content_XML] =
+ lazy val document_latex: List[(File.Content_XML, String)] =
for (name <- all_document_theories)
yield {
val path = Path.basic(tex_name(name))
@@ -195,7 +195,8 @@
YXML.parse_body(entry.text)
}
else Nil
- File.content(path, content)
+ val file_pos = name.path.implode_symbolic
+ (File.content(path, content), file_pos)
}
lazy val session_graph: File.Content = {
@@ -263,8 +264,8 @@
session_tex.write(doc_dir)
- for (content <- document_latex) {
- content.output(latex_output(_, file_pos = content.path.implode_symbolic))
+ for ((content, file_pos) <- document_latex) {
+ content.output(latex_output(_, file_pos = file_pos))
.write(doc_dir)
}
--- a/src/Tools/VSCode/src/vscode_resources.scala Thu Dec 22 21:55:51 2022 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala Fri Dec 23 12:14:10 2022 +0100
@@ -100,6 +100,9 @@
}
}
+ override def migrate_name(standard_name: Document.Node.Name): Document.Node.Name =
+ node_name(Path.explode(standard_name.node).canonical_file)
+
override def append(dir: String, source_path: Path): String = {
val path = source_path.expand
if (dir == "" || path.is_absolute) File.platform_path(path)
--- a/src/Tools/jEdit/src/jedit_resources.scala Thu Dec 22 21:55:51 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala Fri Dec 23 12:14:10 2022 +0100
@@ -50,6 +50,9 @@
if (name.is_theory) Some(name) else None
}
+ override def migrate_name(standard_name: Document.Node.Name): Document.Node.Name =
+ node_name(File.platform_path(Path.explode(standard_name.node).canonical))
+
override def append(dir: String, source_path: Path): String = {
val path = source_path.expand
if (dir == "" || path.is_absolute) {
--- a/src/Tools/jEdit/src/jedit_sessions.scala Thu Dec 22 21:55:51 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Fri Dec 23 12:14:10 2022 +0100
@@ -113,8 +113,9 @@
def document_selector(options: Options_Variable, standalone: Boolean = false): Selector =
GUI_Thread.require {
- val sessions = sessions_structure(options = options.value)
- val all_sessions = sessions.build_topological_order.sorted
+ val sessions = sessions_structure(options = options.value + "document")
+ val all_sessions =
+ sessions.build_topological_order.filter(name => sessions(name).documents.nonEmpty).sorted
val doc_sessions = all_sessions.filter(name => sessions(name).doc_group)
new Selector(options, "editor_document_session", standalone,