# HG changeset patch
# User wenzelm
# Date 1667996478 -3600
# Node ID 8c9830109ab2dfcb2d9d2fe493d79405aebfc44a
# Parent  1eed7e1300ed8ba706e7c7d4afe12c50af920f36
clarified Log_Progress vs. GUI: more like Syslog_Dockable;

diff -r 1eed7e1300ed -r 8c9830109ab2 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Wed Nov 09 12:32:20 2022 +0100
+++ b/src/Tools/jEdit/src/document_dockable.scala	Wed Nov 09 13:21:18 2022 +0100
@@ -94,27 +94,32 @@
 
   /* progress log */
 
-  private val log_area = new TextArea {
-    editable = false
-    columns = 60
-    rows = 24
-  }
-  log_area.font = GUI.copy_font((new Label).font)
-
+  private val log_area =
+    new TextArea {
+      editable = false
+      font = GUI.copy_font((new Label).font)
+    }
   private val scroll_log_area = new ScrollPane(log_area)
 
-  private def init_progress() = {
-    GUI_Thread.later { log_area.text = "" }
-    new Progress {
-      override def echo(txt: String): Unit =
-        GUI_Thread.later {
-          log_area.append(txt + "\n")
-          val vertical = scroll_log_area.peer.getVerticalScrollBar
-          vertical.setValue(vertical.getMaximum)
-        }
+  private class Log_Progress extends Progress {
+    private val syslog = PIDE.session.make_syslog()
 
-      override def theory(theory: Progress.Theory): Unit = echo(theory.message)
+    private def update(): Unit = {
+      val text = syslog.content()
+      if (text != log_area.text) {
+        log_area.text = text
+        val vertical = scroll_log_area.peer.getVerticalScrollBar
+        vertical.setValue(vertical.getMaximum)
+      }
     }
+    update()
+
+    private val delay =
+      Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { update() }
+
+    override def echo(msg: String): Unit = { syslog += msg; delay.invoke() }
+
+    override def theory(theory: Progress.Theory): Unit = echo(theory.message)
   }
 
 
@@ -126,14 +131,17 @@
   private def build_document(): Unit = {
     current_state.change { st =>
       if (st.process.is_finished) {
-        val progress = init_progress()
+        val progress = new Log_Progress()
         val process =
           Future.thread[Unit](name = "document_build") {
             show_page(log_page)
             val res =
               Exn.capture {
                 progress.echo("Start " + Date.now())
-                Time.seconds(2.0).sleep()
+                for (i <- 1 to 200) {
+                  progress.echo("message " + i)
+                  Time.seconds(0.1).sleep()
+                }
                 progress.echo("Stop " + Date.now())
               }
             val msg =
@@ -206,7 +214,7 @@
 
   private val log_page =
     new TabbedPane.Page("Log", new BorderPanel {
-      layout(log_area) = BorderPanel.Position.Center
+      layout(scroll_log_area) = BorderPanel.Position.Center
     }, "Raw log of build process")
 
   message_pane.pages ++= List(log_page, output_page)