# HG changeset patch
# User wenzelm
# Date 1587488869 -7200
# Node ID 291c46bf30000daaf511094d31ee13327c6c8933
# Parent  491f185fd705e4424a19700f4f6de61e1e92ec6e
tuned;

diff -r 491f185fd705 -r 291c46bf3000 src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala	Tue Apr 21 19:07:11 2020 +0200
+++ b/src/Pure/General/sha1.scala	Tue Apr 21 19:07:49 2020 +0200
@@ -45,12 +45,10 @@
     {
       val buf = new Array[Byte](65536)
       var m = 0
-      try {
-        do {
-          m = stream.read(buf, 0, buf.length)
-          if (m != -1) digest.update(buf, 0, m)
-        } while (m != -1)
-      }
+      do {
+        m = stream.read(buf, 0, buf.length)
+        if (m != -1) digest.update(buf, 0, m)
+      } while (m != -1)
     })
 
     make_result(digest)
diff -r 491f185fd705 -r 291c46bf3000 src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Tue Apr 21 19:07:11 2020 +0200
+++ b/src/Tools/jEdit/src/active.scala	Tue Apr 21 19:07:49 2020 +0200
@@ -30,7 +30,7 @@
 
     Document_View.get(view.getTextArea) match {
       case Some(doc_view) =>
-        doc_view.rich_text_area.robust_body() {
+        doc_view.rich_text_area.robust_body(()) {
           val snapshot = doc_view.model.snapshot()
           if (!snapshot.is_outdated) {
             handlers.find(_.handle(view, text, elem, doc_view, snapshot))