--- a/src/Pure/PIDE/command.scala Mon Dec 19 12:00:56 2022 +0100
+++ b/src/Pure/PIDE/command.scala Mon Dec 19 14:09:37 2022 +0100
@@ -340,7 +340,7 @@
props match {
case Markup.Serial(i) =>
val markup_message =
- cache.elem(Protocol.make_message(body, kind = name, props = props))
+ cache.elem(Protocol.make_message(body, name, props = props))
val message_markup =
cache.elem(XML.elem(Markup(name, props.filter(p => p._1 == Markup.SERIAL))))
--- a/src/Pure/PIDE/document_editor.scala Mon Dec 19 12:00:56 2022 +0100
+++ b/src/Pure/PIDE/document_editor.scala Mon Dec 19 14:09:37 2022 +0100
@@ -45,10 +45,10 @@
/* global state */
sealed case class State(
- session_info: Option[Sessions.Info] = None,
+ session_background: Option[Sessions.Background] = None,
views: Set[AnyRef] = Set.empty,
) {
- def is_active: Boolean = session_info.isDefined && views.nonEmpty
+ def is_active: Boolean = session_background.isDefined && views.nonEmpty
def register_view(id: AnyRef): State = copy(views = views + id)
def unregister_view(id: AnyRef): State = copy(views = views - id)
--- a/src/Pure/PIDE/editor.scala Mon Dec 19 12:00:56 2022 +0100
+++ b/src/Pure/PIDE/editor.scala Mon Dec 19 14:09:37 2022 +0100
@@ -20,8 +20,12 @@
protected val document_editor: Synchronized[Document_Editor.State] =
Synchronized(Document_Editor.State())
+ def document_editor_session: Option[Sessions.Background] =
+ document_editor.value.session_background
def document_editor_active: Boolean =
document_editor.value.is_active
+ def document_editor_setup(background: Option[Sessions.Background]): Unit =
+ document_editor.change(_.copy(session_background = background))
def document_editor_init(id: AnyRef): Unit =
document_editor.change(_.register_view(id))
def document_editor_exit(id: AnyRef): Unit =
--- a/src/Pure/PIDE/protocol.scala Mon Dec 19 12:00:56 2022 +0100
+++ b/src/Pure/PIDE/protocol.scala Mon Dec 19 14:09:37 2022 +0100
@@ -202,13 +202,16 @@
text1 + text2
}
- def make_message(body: XML.Body,
- kind: String = Markup.WRITELN,
- props: Properties.T = Nil
- ): XML.Elem = XML.Elem(Markup(Markup.message(kind), props), body)
+ def make_message(body: XML.Body, kind: String, props: Properties.T = Nil): XML.Elem =
+ XML.Elem(Markup(Markup.message(kind), props), body)
- def warning_message(body: XML.Body): XML.Elem = make_message(body, kind = Markup.WARNING)
- def error_message(body: XML.Body): XML.Elem = make_message(body, kind = Markup.ERROR)
+ def writeln_message(body: XML.Body): XML.Elem = make_message(body, Markup.WRITELN)
+ def warning_message(body: XML.Body): XML.Elem = make_message(body, Markup.WARNING)
+ def error_message(body: XML.Body): XML.Elem = make_message(body, Markup.ERROR)
+
+ def writeln_message(msg: String): XML.Elem = writeln_message(XML.string(msg))
+ def warning_message(msg: String): XML.Elem = warning_message(XML.string(msg))
+ def error_message(msg: String): XML.Elem = error_message(XML.string(msg))
/* ML profiling */
--- a/src/Pure/PIDE/query_operation.scala Mon Dec 19 12:00:56 2022 +0100
+++ b/src/Pure/PIDE/query_operation.scala Mon Dec 19 14:09:37 2022 +0100
@@ -119,7 +119,7 @@
XML.Elem(_, List(XML.Elem(markup, body))) <- results
if Markup.messages.contains(markup.name)
body1 = resolve_sendback(body)
- } yield Protocol.make_message(body1, kind = markup.name, props = markup.properties)
+ } yield Protocol.make_message(body1, markup.name, props = markup.properties)
/* status */
--- a/src/Pure/Thy/document_build.scala Mon Dec 19 12:00:56 2022 +0100
+++ b/src/Pure/Thy/document_build.scala Mon Dec 19 14:09:37 2022 +0100
@@ -109,7 +109,21 @@
}
- /* context */
+ /* background context */
+
+ def session_background(
+ options: Options,
+ session: String,
+ dirs: List[Path] = Nil,
+ progress: Progress = new Progress
+ ): Sessions.Background = {
+ Sessions.load_structure(options + "document=pdf", dirs = dirs).
+ selection_deps(Sessions.Selection.session(session), progress = progress).
+ background(session)
+ }
+
+
+ /* document context */
val texinputs: Path = Path.explode("~~/lib/texinputs")
@@ -507,17 +521,12 @@
dirs = dirs, progress = progress, verbose = verbose_build)
if (!build_results.ok) error("Failed to build session " + quote(session))
- val deps =
- Sessions.load_structure(options + "document=pdf", dirs = dirs).
- selection_deps(Sessions.Selection.session(session))
-
- val session_background = deps.background(session)
-
if (output_sources.isEmpty && output_pdf.isEmpty) {
progress.echo_warning("No output directory")
}
- using(Export.open_session_context(build_results.store, session_background)) {
+ val background = session_background(options, session, dirs = dirs)
+ using(Export.open_session_context(build_results.store, background)) {
session_context =>
build_documents(
context(session_context, progress = progress),
--- a/src/Pure/Thy/sessions.scala Mon Dec 19 12:00:56 2022 +0100
+++ b/src/Pure/Thy/sessions.scala Mon Dec 19 14:09:37 2022 +0100
@@ -102,6 +102,9 @@
nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax
}
+
+ /* background context */
+
sealed case class Background(
base: Base,
sessions_structure: Structure = Structure.empty,
--- a/src/Pure/Tools/debugger.scala Mon Dec 19 12:00:56 2022 +0100
+++ b/src/Pure/Tools/debugger.scala Mon Dec 19 14:09:37 2022 +0100
@@ -123,7 +123,7 @@
case Markup.Debugger_Output(thread_name) =>
Symbol.decode_yxml_failsafe(msg.text) match {
case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
- val message = Protocol.make_message(body, kind = name, props = props)
+ val message = Protocol.make_message(body, name, props = props)
debugger.add_output(thread_name, i -> session.cache.elem(message))
true
case _ => false
--- a/src/Tools/jEdit/src/document_dockable.scala Mon Dec 19 12:00:56 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala Mon Dec 19 14:09: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()
@@ -142,17 +174,16 @@
}
val msg =
res match {
- case Exn.Res(_) => Protocol.make_message(XML.string("OK"))
- case Exn.Exn(exn) => Protocol.error_message(XML.string(Exn.message(exn)))
+ 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 =
--- a/src/Tools/jEdit/src/jedit_sessions.scala Mon Dec 19 12:00:56 2022 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Mon Dec 19 14:09:37 2022 +0100
@@ -94,7 +94,7 @@
load()
}
- def logic_selector(options: Options_Variable, standalone: Boolean = false): JEdit_Options.Entry =
+ def logic_selector(options: Options_Variable, standalone: Boolean = false): Selector =
GUI_Thread.require {
val sessions = sessions_structure(options = options.value)
val all_sessions = sessions.imports_topological_order
@@ -108,7 +108,7 @@
all_sessions.sorted.map(GUI.Selector.item))
}
- def document_selector(options: Options_Variable, standalone: Boolean = false): JEdit_Options.Entry =
+ 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