# HG changeset patch
# User wenzelm
# Date 1661971615 -7200
# Node ID 2ba535c2d2d8e38af0fb68f58330e5ce8aa97fe3
# Parent  dc1a950183a4d8a033acbb2c1abce293298e9834
clarified signature;

diff -r dc1a950183a4 -r 2ba535c2d2d8 src/Tools/jEdit/src/document_dockable.scala
--- a/src/Tools/jEdit/src/document_dockable.scala	Wed Aug 31 20:41:30 2022 +0200
+++ b/src/Tools/jEdit/src/document_dockable.scala	Wed Aug 31 20:46:55 2022 +0200
@@ -27,17 +27,17 @@
     val FINISHED = Value("finished")
   }
 
-  sealed case class Result(output: List[XML.Tree] = Nil, ok: Boolean = true)
+  sealed case class Result(failed: Boolean = false, output: List[XML.Tree] = Nil)
 
   object State {
     val empty: State = State()
-    def finish(result: Result): State = State(ok = result.ok, output = result.output)
+    def finish(result: Result): State = State(failed = result.failed, output = result.output)
   }
 
   sealed case class State(
     progress: Progress = new Progress,
     process: Future[Unit] = Future.value(()),
-    ok: Boolean = true,
+    failed: Boolean = false,
     output: List[XML.Tree] = Nil,
     status: Status.Value = Status.FINISHED
   )
@@ -69,7 +69,7 @@
         process_indicator.update(null, 0)
     }
 
-    if (!st.ok && output_page != null) message_pane.selection.page = output_page
+    if (st.failed && output_page != null) message_pane.selection.page = output_page
   }
 
 
@@ -137,12 +137,12 @@
                 Time.seconds(2.0).sleep()
                 progress.echo("Stop " + Date.now())
               }
-            val (ok, msg) =
+            val (failed, msg) =
               res match {
-                case Exn.Res(_) => (true, Protocol.make_message(XML.string("OK")))
-                case Exn.Exn(exn) => (false, Protocol.error_message(XML.string(Exn.message(exn))))
+                case Exn.Res(_) => (false, Protocol.make_message(XML.string("OK")))
+                case Exn.Exn(exn) => (true, Protocol.error_message(XML.string(Exn.message(exn))))
               }
-            val result = Document_Dockable.Result(ok = ok, output = List(msg))
+            val result = Document_Dockable.Result(failed = failed, output = List(msg))
             finish(result)
           }
         st.copy(progress = progress, process = process, status = Document_Dockable.Status.RUNNING)