# HG changeset patch # User wenzelm # Date 1670516611 -3600 # Node ID 3558388330f891392598ccb6444f926c55ba7cd4 # Parent 77805bdabc8eb2a332c0566c4a1a137cf5fbaa82 clarified modules; diff -r 77805bdabc8e -r 3558388330f8 etc/build.props --- a/etc/build.props Thu Dec 08 17:04:13 2022 +0100 +++ b/etc/build.props Thu Dec 08 17:23:31 2022 +0100 @@ -124,6 +124,7 @@ src/Pure/PIDE/command.scala \ src/Pure/PIDE/command_span.scala \ src/Pure/PIDE/document.scala \ + src/Pure/PIDE/document_editor.scala \ src/Pure/PIDE/document_id.scala \ src/Pure/PIDE/document_info.scala \ src/Pure/PIDE/document_status.scala \ diff -r 77805bdabc8e -r 3558388330f8 src/Pure/PIDE/document_editor.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/PIDE/document_editor.scala Thu Dec 08 17:23:31 2022 +0100 @@ -0,0 +1,44 @@ +/* Title: Pure/PIDE/document_editor.scala + Author: Makarius + +Central resources for interactive document preparation. +*/ + +package isabelle + + +object Document_Editor { + /* document output */ + + def document_name: String = "document" + def document_output_dir(): Path = Path.explode("$ISABELLE_HOME_USER/document_output") + def document_output(): Path = document_output_dir() + Path.basic(document_name) + + def view_document(): Unit = { + val path = document_output().pdf + if (path.is_file) Isabelle_System.pdf_viewer(path) + } + + + /* progress */ + + class Log_Progress(session: Session) extends Progress { + def show(text: String): Unit = {} + + private val syslog = session.make_syslog() + + private def update(text: String = syslog.content()): Unit = show(text) + private val delay = + Delay.first(session.session_options.seconds("editor_update_delay"), gui = true) { update() } + + 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) } + } + + GUI_Thread.later { update() } + } +} diff -r 77805bdabc8e -r 3558388330f8 src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala Thu Dec 08 17:04:13 2022 +0100 +++ b/src/Tools/jEdit/src/document_dockable.scala Thu Dec 08 17:23:31 2022 +0100 @@ -19,38 +19,6 @@ object Document_Dockable { - /* document output */ - - def document_name: String = "document" - def document_output_dir(): Path = Path.explode("$ISABELLE_HOME_USER/document_output") - def document_output(): Path = document_output_dir() + Path.basic(document_name) - - def view_document(): Unit = { - val path = Document_Dockable.document_output().pdf - if (path.is_file) Isabelle_System.pdf_viewer(path) - } - - class Log_Progress extends Progress { - def show(text: String): Unit = {} - - private val syslog = PIDE.session.make_syslog() - - private def update(text: String = syslog.content()): Unit = show(text) - private val delay = - Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { update() } - - 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) } - } - - GUI_Thread.later { update() } - } - - /* state */ object Status extends Enumeration { @@ -69,7 +37,7 @@ } sealed case class State( - progress: Log_Progress = new Log_Progress, + progress: Progress = new Progress, process: Future[Unit] = Future.value(()), output: List[XML.Tree] = Nil, status: Status.Value = Status.FINISHED) @@ -132,8 +100,8 @@ } private val scroll_log_area = new ScrollPane(log_area) - def init_progress(): Document_Dockable.Log_Progress = - new Document_Dockable.Log_Progress { + def log_progress(): Document_Editor.Log_Progress = + new Document_Editor.Log_Progress(PIDE.session) { override def show(text: String): Unit = if (text != log_area.text) { log_area.text = text @@ -149,12 +117,12 @@ current_state.change { st => st.process.cancel(); st } private def init_state(): Unit = - current_state.change { _ => Document_Dockable.State(progress = init_progress()) } + current_state.change { _ => Document_Dockable.State(progress = log_progress()) } private def build_document(): Unit = { current_state.change { st => if (st.process.is_finished) { - val progress = init_progress() + val progress = log_progress() val process = Future.thread[Unit](name = "document_build") { show_page(theories_page) @@ -218,7 +186,7 @@ private val view_button = new GUI.Button("View") { tooltip = "View document" - override def clicked(): Unit = Document_Dockable.view_document() + override def clicked(): Unit = Document_Editor.view_document() } private val controls =