--- a/src/Pure/ML/ml_console.scala Wed Dec 21 12:30:48 2022 +0000
+++ b/src/Pure/ML/ml_console.scala Wed Dec 21 15:41:45 2022 +0100
@@ -60,7 +60,7 @@
if (rc != Process_Result.RC.ok) sys.exit(rc)
}
- val background =
+ val session_background =
if (raw_ml_system) {
Sessions.Background(
base = Sessions.Base.bootstrap,
@@ -73,7 +73,7 @@
// process loop
val process =
- ML_Process(options, background, store,
+ ML_Process(store, options, session_background,
logic = logic, args = List("-i"), redirect = true,
modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
raw_ml_system = raw_ml_system)
--- a/src/Pure/ML/ml_process.scala Wed Dec 21 12:30:48 2022 +0000
+++ b/src/Pure/ML/ml_process.scala Wed Dec 21 15:41:45 2022 +0100
@@ -12,9 +12,10 @@
object ML_Process {
- def apply(options: Options,
+ def apply(
+ store: Sessions.Store,
+ options: Options,
session_background: Sessions.Background,
- store: Sessions.Store,
logic: String = "",
raw_ml_system: Boolean = false,
use_prelude: List[String] = Nil,
@@ -168,10 +169,10 @@
val more_args = getopts(args)
if (args.isEmpty || more_args.nonEmpty) getopts.usage()
+ val store = Sessions.store(options)
val session_background = Sessions.background(options, logic, dirs = dirs).check_errors
- val store = Sessions.store(options)
val result =
- ML_Process(options, session_background, store,
+ ML_Process(store, options, session_background,
logic = logic, args = eval_args, modes = modes).result(
progress_stdout = Output.writeln(_, stdout = true),
progress_stderr = Output.writeln(_))
--- a/src/Pure/PIDE/document_editor.scala Wed Dec 21 12:30:48 2022 +0000
+++ b/src/Pure/PIDE/document_editor.scala Wed Dec 21 15:41:45 2022 +0100
@@ -1,7 +1,7 @@
/* Title: Pure/PIDE/document_editor.scala
Author: Makarius
-Central resources for interactive document preparation.
+Central resources and configuration for interactive document preparation.
*/
package isabelle
@@ -32,17 +32,16 @@
override def echo(msg: String): Unit = { syslog += msg; delay.invoke() }
- def load(): Unit = GUI_Thread.require {
- val path = document_output().log
- val text = if (path.is_file) File.read(path) else ""
- GUI_Thread.later { delay.revoke(); update(text) }
+ def finish(text: String): Unit = GUI_Thread.require {
+ delay.revoke()
+ update(text)
}
GUI_Thread.later { update() }
}
- /* global state */
+ /* configuration state */
sealed case class State(
session_background: Option[Sessions.Background] = None,
--- a/src/Pure/PIDE/editor.scala Wed Dec 21 12:30:48 2022 +0000
+++ b/src/Pure/PIDE/editor.scala Wed Dec 21 15:41:45 2022 +0100
@@ -27,7 +27,10 @@
val changed =
document_editor.change_result { st =>
val st1 = f(st)
- (st.required != st1.required, st1)
+ val changed =
+ st.active_document_theories != st1.active_document_theories ||
+ st.required != st1.required
+ (changed, st1)
}
if (changed) document_state_changed()
}
@@ -37,6 +40,7 @@
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_selection(): Set[Document.Node.Name] = document_state().selection
def document_setup(background: Option[Sessions.Background]): Unit =
document_state_change(_.copy(session_background = background))
--- a/src/Pure/PIDE/headless.scala Wed Dec 21 12:30:48 2022 +0000
+++ b/src/Pure/PIDE/headless.scala Wed Dec 21 15:41:45 2022 +0100
@@ -622,7 +622,7 @@
val session = new Session(session_name, options, resources)
progress.echo("Starting session " + session_name + " ...")
- Isabelle_Process.start(session, options, session_background, store,
+ Isabelle_Process.start(store, options, session, session_background,
logic = session_name, modes = print_mode).await_startup()
session
--- a/src/Pure/System/isabelle_process.scala Wed Dec 21 12:30:48 2022 +0000
+++ b/src/Pure/System/isabelle_process.scala Wed Dec 21 15:41:45 2022 +0100
@@ -13,10 +13,10 @@
object Isabelle_Process {
def start(
- session: Session,
+ store: Sessions.Store,
options: Options,
+ session: Session,
session_background: Sessions.Background,
- store: Sessions.Store,
logic: String = "",
raw_ml_system: Boolean = false,
use_prelude: List[String] = Nil,
@@ -28,10 +28,11 @@
val channel = System_Channel()
val process =
try {
- val channel_options =
- options.string.update("system_channel_address", channel.address).
+ val ml_options =
+ options.
+ string.update("system_channel_address", channel.address).
string.update("system_channel_password", channel.password)
- ML_Process(channel_options, session_background, store,
+ ML_Process(store, ml_options, session_background,
logic = logic, raw_ml_system = raw_ml_system,
use_prelude = use_prelude, eval_main = eval_main,
modes = modes, cwd = cwd, env = env)
--- a/src/Pure/Thy/document_build.scala Wed Dec 21 12:30:48 2022 +0000
+++ b/src/Pure/Thy/document_build.scala Wed Dec 21 15:41:45 2022 +0100
@@ -135,13 +135,15 @@
def context(
session_context: Export.Session_Context,
document_session: Option[Sessions.Base] = None,
+ document_selection: Document.Node.Name => Boolean = _ => true,
progress: Progress = new Progress
- ): Context = new Context(session_context, document_session, progress)
+ ): Context = new Context(session_context, document_session, document_selection, progress)
final class Context private[Document_Build](
val session_context: Export.Session_Context,
document_session: Option[Sessions.Base],
- val progress: Progress = new Progress
+ document_selection: Document.Node.Name => Boolean,
+ val progress: Progress
) {
context =>
@@ -187,8 +189,12 @@
for (name <- all_document_theories)
yield {
val path = Path.basic(tex_name(name))
- val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true)
- val content = YXML.parse_body(entry.text)
+ val content =
+ if (document_selection(name)) {
+ val entry = session_context(name.theory, Export.DOCUMENT_LATEX, permissive = true)
+ YXML.parse_body(entry.text)
+ }
+ else Nil
File.content(path, content)
}
@@ -526,8 +532,8 @@
progress.echo_warning("No output directory")
}
- val background = session_background(options, session, dirs = dirs)
- using(Export.open_session_context(build_results.store, background)) {
+ val session_background = Document_Build.session_background(options, session, dirs = dirs)
+ using(Export.open_session_context(build_results.store, session_background)) {
session_context =>
build_documents(
context(session_context, progress = progress),
--- a/src/Pure/Thy/sessions.scala Wed Dec 21 12:30:48 2022 +0000
+++ b/src/Pure/Thy/sessions.scala Wed Dec 21 15:41:45 2022 +0100
@@ -112,6 +112,7 @@
infos: List[Info] = Nil
) {
def session_name: String = base.session_name
+ def info: Info = sessions_structure(session_name)
def check_errors: Background =
if (errors.isEmpty) this
--- a/src/Pure/Tools/build_job.scala Wed Dec 21 12:30:48 2022 +0000
+++ b/src/Pure/Tools/build_job.scala Wed Dec 21 15:41:45 2022 +0100
@@ -447,7 +447,7 @@
val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
val process =
- Isabelle_Process.start(session, options, session_background, store,
+ Isabelle_Process.start(store, options, session, session_background,
logic = parent, raw_ml_system = is_pure,
use_prelude = use_prelude, eval_main = eval_main,
cwd = info.dir.file, env = env)
--- a/src/Tools/VSCode/src/language_server.scala Wed Dec 21 12:30:48 2022 +0000
+++ b/src/Tools/VSCode/src/language_server.scala Wed Dec 21 15:41:45 2022 +0100
@@ -307,7 +307,7 @@
dynamic_output.init()
try {
- Isabelle_Process.start(session, options, session_background, store,
+ Isabelle_Process.start(store, options, session, session_background,
modes = modes, logic = session_background.session_name).await_startup()
reply_ok(
"Welcome to Isabelle/" + session_background.session_name +
--- a/src/Tools/jEdit/src/document_dockable.scala Wed Dec 21 12:30:48 2022 +0000
+++ b/src/Tools/jEdit/src/document_dockable.scala Wed Dec 21 15:41:45 2022 +0100
@@ -151,7 +151,7 @@
private def load_document(session: String): Boolean = {
val options = PIDE.options.value
- run_process { progress =>
+ run_process { _ =>
try {
val session_background =
Document_Build.session_background(
@@ -160,8 +160,7 @@
finish_process(Nil)
GUI_Thread.later {
- val domain = PIDE.editor.document_theories().toSet
- theories.update(domain = Some(domain), trim = true, force = true)
+ refresh_theories()
show_state()
show_page(theories_page)
}
@@ -177,32 +176,57 @@
}
}
- private def build_document(): Unit = {
- run_process { progress =>
- show_page(theories_page)
- Time.seconds(2.0).sleep()
+ private def document_build(
+ session_background: Sessions.Background,
+ progress: Document_Editor.Log_Progress
+ ): Unit = {
+ val store = JEdit_Sessions.sessions_store(PIDE.options.value)
+ val document_selection = PIDE.editor.document_selection()
+
+ val snapshot = PIDE.session.await_stable_snapshot()
+ val session_context =
+ Export.open_session_context(store, session_background,
+ document_snapshot = Some(snapshot))
+ try {
+ val context =
+ Document_Build.context(session_context,
+ document_session = Some(session_background.base),
+ document_selection = document_selection,
+ progress = progress)
+ val variant = session_background.info.documents.head
+
+ Isabelle_System.make_directory(Document_Editor.document_output_dir())
+ val doc = context.build_document(variant, verbose = true)
+
+ // log
+ File.write(Document_Editor.document_output().log, doc.log)
+ GUI_Thread.later { progress.finish(doc.log) }
- show_page(log_page)
- val res =
- Exn.capture {
- progress.echo("Start " + Date.now())
- for (i <- 1 to 200) {
- progress.echo("message " + i)
- Time.seconds(0.1).sleep()
- }
- progress.echo("Stop " + Date.now())
+ // pdf
+ Bytes.write(Document_Editor.document_output().pdf, doc.pdf)
+ Document_Editor.view_document()
+ }
+ finally { session_context.close() }
+ }
+
+ private def build_document(): Unit = {
+ PIDE.editor.document_session() match {
+ case Some(session_background) if session_background.info.documents.nonEmpty =>
+ run_process { progress =>
+ show_page(log_page)
+ val res = Exn.capture { document_build(session_background, progress) }
+ val msg =
+ res match {
+ case Exn.Res(_) => Protocol.writeln_message("OK")
+ case Exn.Exn(exn) => Protocol.error_message(Exn.print(exn))
+ }
+
+ finish_process(List(msg))
+
+ show_state()
+ show_page(if (Exn.is_interrupt_exn(res)) theories_page else output_page)
}
- val msg =
- res match {
- case Exn.Res(_) => Protocol.writeln_message("OK")
- case Exn.Exn(exn) => Protocol.error_message(Exn.print(exn))
- }
- finish_process(List(msg))
-
- show_state()
-
- show_page(if (Exn.is_interrupt_exn(res)) theories_page else output_page)
- GUI_Thread.later { progress.load() }
+ case _ =>
}
}
@@ -221,6 +245,12 @@
document_session.reactions += { case SelectionChanged(_) => delay_load.invoke() }
+ private val load_button =
+ new GUI.Button("Load") {
+ tooltip = "Load document theories"
+ override def clicked(): Unit = PIDE.editor.document_select_all(set = true)
+ }
+
private val build_button =
new GUI.Button("<html><b>Build</b></html>") {
tooltip = "Build document"
@@ -240,8 +270,8 @@
}
private val controls =
- Wrap_Panel(List(document_session, process_indicator.component, build_button,
- view_button, cancel_button))
+ Wrap_Panel(List(document_session, process_indicator.component, load_button,
+ build_button, view_button, cancel_button))
add(controls.peer, BorderLayout.NORTH)
@@ -250,23 +280,28 @@
/* message pane with pages */
- private val select_all_button =
- new GUI.Button("All") {
- tooltip = "Select all document theories"
- override def clicked(): Unit = PIDE.editor.document_select_all(set = true)
- }
-
- private val select_none_button =
- new GUI.Button("None") {
- tooltip = "Deselect all document theories"
+ private val reset_button =
+ new GUI.Button("Reset") {
+ tooltip = "Deselect document theories"
override def clicked(): Unit = PIDE.editor.document_select_all(set = false)
}
+ private val purge_button = new GUI.Button("Purge") {
+ tooltip = "Remove theories that are no longer required"
+ override def clicked(): Unit = PIDE.editor.purge()
+ }
+
private val theories_controls =
- Wrap_Panel(List(select_all_button, select_none_button))
+ Wrap_Panel(List(reset_button, purge_button))
private val theories = new Theories_Status(view, document = true)
+ private def refresh_theories(): Unit = {
+ val domain = PIDE.editor.document_theories().toSet
+ theories.update(domain = Some(domain), trim = true, force = true)
+ theories.refresh()
+ }
+
private val theories_page =
new TabbedPane.Page("Theories", new BorderPanel {
layout(theories_controls) = BorderPanel.Position.North
@@ -300,7 +335,7 @@
GUI_Thread.later {
document_session.load()
handle_resize()
- theories.refresh()
+ refresh_theories()
}
case changed: Session.Commands_Changed =>
GUI_Thread.later {
--- a/src/Tools/jEdit/src/jedit_sessions.scala Wed Dec 21 12:30:48 2022 +0000
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Wed Dec 21 15:41:45 2022 +0100
@@ -43,6 +43,9 @@
Sessions.load_structure(session_options(options), dirs = dirs)
}
+ def sessions_store(options: Options): Sessions.Store =
+ Sessions.store(session_options(options))
+
/* raw logic info */
@@ -141,18 +144,17 @@
infos = PIDE.resources.session_background.infos).rc
}
- def session_start(options0: Options): Unit = {
+ def session_start(options: Options): Unit = {
val session = PIDE.session
- val options = session_options(options0)
val session_background = PIDE.resources.session_background
- val store = Sessions.store(options)
+ val store = sessions_store(options)
session.phase_changed += PIDE.plugin.session_phase_changed
- Isabelle_Process.start(session, options, session_background, store,
- logic = PIDE.resources.session_base.session_name,
+ Isabelle_Process.start(store, store.options, session, session_background,
+ logic = session_background.session_name,
modes =
- (space_explode(',', options.string("jedit_print_mode")) :::
+ (space_explode(',', store.options.string("jedit_print_mode")) :::
space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE"))).reverse)
}
}
--- a/src/Tools/jEdit/src/theories_dockable.scala Wed Dec 21 12:30:48 2022 +0000
+++ b/src/Tools/jEdit/src/theories_dockable.scala Wed Dec 21 15:41:45 2022 +0100
@@ -31,7 +31,7 @@
}
private val purge = new GUI.Button("Purge") {
- tooltip = "Restrict document model to theories required for open editor buffers"
+ tooltip = "Remove theories that are no longer required"
override def clicked(): Unit = PIDE.editor.purge()
}