# HG changeset patch # User desharna # Date 1671794050 -3600 # Node ID 907b5c4d13321a1cac6d6435d3f4ad4731cbc162 # Parent c507162fe36e02c4fc638f2ef0267751e17f245e# Parent 3f41f3c3696c34d1c56d9af29f5dabe79fd034de merged diff -r c507162fe36e -r 907b5c4d1332 src/Pure/Admin/build_doc.scala --- 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]]( diff -r c507162fe36e -r 907b5c4d1332 src/Pure/PIDE/document_editor.scala --- 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 diff -r c507162fe36e -r 907b5c4d1332 src/Pure/PIDE/editor.scala --- 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)) diff -r c507162fe36e -r 907b5c4d1332 src/Pure/PIDE/resources.scala --- 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 diff -r c507162fe36e -r 907b5c4d1332 src/Pure/Thy/document_build.scala --- 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) } diff -r c507162fe36e -r 907b5c4d1332 src/Tools/VSCode/src/vscode_resources.scala --- 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) diff -r c507162fe36e -r 907b5c4d1332 src/Tools/jEdit/src/jedit_resources.scala --- 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) { diff -r c507162fe36e -r 907b5c4d1332 src/Tools/jEdit/src/jedit_sessions.scala --- 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,