# HG changeset patch
# User wenzelm
# Date 1671384637 -3600
# Node ID 8ad17c4669da1ea6a271b6b8ee8b0acd74d083d6
# Parent  e95b9c9e17ff7ad8b7db57b5c4a2a81ca979a49c
clarified state and process;
support to load document session_background (which can take 1-2s in AFP);

diff -r e95b9c9e17ff -r 8ad17c4669da src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Sun Dec 18 16:01:37 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Sun Dec 18 18:30:37 2022 +0100
@@ -32,15 +32,21 @@
   }
 
   object State {
-    def empty(): State = State()
-    def finish(result: Result): State = State(output = result.output)
+    def init(): State = State()
   }
 
   sealed case class State(
     progress: Progress = new Progress,
     process: Future[Unit] = Future.value(()),
-    output: List[XML.Tree] = Nil,
-    status: Status.Value = Status.FINISHED)
+    status: Status.Value = Status.FINISHED,
+    output: List[XML.Tree] = Nil
+  ) {
+    def run(progress: Progress, process: Future[Unit]): State =
+      copy(progress = progress, process = process, status = Status.RUNNING)
+
+    def finish(result: Result): State = State(output = result.output)
+    def finish(msg: XML.Tree): State = finish(Result(output = List(msg)))
+  }
 }
 
 class Document_Dockable(view: View, position: String) extends Dockable(view, position) {
@@ -51,7 +57,7 @@
 
   /* component state -- owned by GUI thread */
 
-  private val current_state = Synchronized(Document_Dockable.State.empty())
+  private val current_state = Synchronized(Document_Dockable.State.init())
 
   private val process_indicator = new Process_Indicator
   private val pretty_text_area = new Pretty_Text_Area(view)
@@ -121,12 +127,38 @@
   private def init_state(): Unit =
     current_state.change { _ => Document_Dockable.State(progress = log_progress()) }
 
+  private def load_document(session: String): Boolean = {
+    current_state.change_result { st =>
+      if (st.process.is_finished) {
+        val options = PIDE.options.value
+        val progress = log_progress()
+        val process =
+          Future.thread[Unit](name = "Document_Dockable.load_document") {
+            try {
+              val session_background =
+                Document_Build.session_background(
+                  options, session, dirs = JEdit_Sessions.session_dirs)
+              PIDE.editor.document_editor_setup(Some(session_background))
+              GUI_Thread.later { show_state(); show_page(theories_page) }
+            }
+            catch {
+              case exn: Throwable if !Exn.is_interrupt(exn) =>
+                current_state.change(_.finish(Protocol.error_message(Exn.message(exn))))
+                GUI_Thread.later { show_state(); show_page(output_page) }
+            }
+          }
+        (true, st.run(progress, process))
+      }
+      else (false, st)
+    }
+  }
+
   private def build_document(): Unit = {
     current_state.change { st =>
       if (st.process.is_finished) {
         val progress = log_progress()
         val process =
-          Future.thread[Unit](name = "document_build") {
+          Future.thread[Unit](name = "Document_Dockable.build_document") {
             show_page(theories_page)
             Time.seconds(2.0).sleep()
 
@@ -145,14 +177,13 @@
                 case Exn.Res(_) => Protocol.writeln_message("OK")
                 case Exn.Exn(exn) => Protocol.error_message(Exn.message(exn))
               }
-            val result = Document_Dockable.Result(output = List(msg))
-            current_state.change(_ => Document_Dockable.State.finish(result))
+            current_state.change(_.finish(msg))
             show_state()
 
             show_page(if (Exn.is_interrupt_exn(res)) theories_page else output_page)
             GUI_Thread.later { progress.load() }
           }
-        st.copy(progress = progress, process = process, status = Document_Dockable.Status.RUNNING)
+        st.run(progress, process)
       }
       else st
     }
@@ -162,15 +193,16 @@
 
   /* controls */
 
+  private val document_session =
+    JEdit_Sessions.document_selector(PIDE.options, standalone = true)
+
   private lazy val delay_load: Delay =
     Delay.last(PIDE.session.load_delay, gui = true) {
-      val models = Document_Model.get_models()
-      val thy_files = PIDE.resources.resolve_dependencies(models, Nil)
+      for (session <- document_session.selection_value) {
+        if (!load_document(session)) delay_load.invoke()
+      }
     }
 
-  private val document_session =
-    JEdit_Sessions.document_selector(PIDE.options, standalone = true)
-
   document_session.reactions += { case SelectionChanged(_) => delay_load.invoke() }
 
   private val build_button =