diff --git a/src/Pure/General/sha1.scala b/src/Pure/General/sha1.scala
--- a/src/Pure/General/sha1.scala
+++ b/src/Pure/General/sha1.scala
@@ -1,73 +1,71 @@
 /*  Title:      Pure/General/sha1.scala
     Author:     Makarius
 
 Digest strings according to SHA-1 (see RFC 3174).
 */
 
 package isabelle
 
 
 import java.io.{File => JFile, FileInputStream}
 import java.security.MessageDigest
 
 
 object SHA1
 {
   final class Digest private[SHA1](val rep: String)
   {
     override def hashCode: Int = rep.hashCode
     override def equals(that: Any): Boolean =
       that match {
         case other: Digest => rep == other.rep
         case _ => false
       }
     override def toString: String = rep
   }
 
   private def make_result(digest: MessageDigest): Digest =
   {
     val result = new StringBuilder
     for (b <- digest.digest()) {
       val i = b.asInstanceOf[Int] & 0xFF
       if (i < 16) result += '0'
       result ++= Integer.toHexString(i)
     }
     new Digest(result.toString)
   }
 
   def fake(rep: String): Digest = new Digest(rep)
 
   def digest(file: JFile): Digest =
   {
     val digest = MessageDigest.getInstance("SHA")
 
     using(new FileInputStream(file))(stream =>
     {
       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)
   }
 
   def digest(path: Path): Digest = digest(path.file)
 
   def digest(bytes: Array[Byte]): Digest =
   {
     val digest = MessageDigest.getInstance("SHA")
     digest.update(bytes)
 
     make_result(digest)
   }
 
   def digest(bytes: Bytes): Digest = bytes.sha1_digest
   def digest(string: String): Digest = digest(Bytes(string))
 
   val digest_length: Int = digest("").rep.length
 }
diff --git a/src/Tools/jEdit/src/active.scala b/src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala
+++ b/src/Tools/jEdit/src/active.scala
@@ -1,110 +1,110 @@
 /*  Title:      Tools/jEdit/src/active.scala
     Author:     Makarius
 
 Active areas within the document.
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 import org.gjt.sp.jedit.{ServiceManager, View}
 
 
 object Active
 {
   abstract class Handler
   {
     def handle(
       view: View, text: String, elem: XML.Elem,
       doc_view: Document_View, snapshot: Document.Snapshot): Boolean
   }
 
   def handlers: List[Handler] =
     ServiceManager.getServiceNames(classOf[Handler]).toList
       .map(ServiceManager.getService(classOf[Handler], _))
 
   def action(view: View, text: String, elem: XML.Elem)
   {
     GUI_Thread.require {}
 
     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))
           }
         }
       case None =>
     }
   }
 
   class Misc_Handler extends Active.Handler
   {
     override def handle(
       view: View, text: String, elem: XML.Elem,
       doc_view: Document_View, snapshot: Document.Snapshot): Boolean =
     {
       val text_area = doc_view.text_area
       val model = doc_view.model
       val buffer = model.buffer
 
       elem match {
         case XML.Elem(Markup(Markup.BROWSER, _), body) =>
           Isabelle_Thread.fork(name = "browser") {
             val graph_file = Isabelle_System.tmp_file("graph")
             File.write(graph_file, XML.content(body))
             Isabelle_System.bash("isabelle browser -c " + File.bash_path(graph_file) + " &")
           }
           true
 
         case XML.Elem(Markup(Markup.THEORY_EXPORTS, props), _) =>
           GUI_Thread.later {
             val name = Markup.Name.unapply(props) getOrElse ""
             PIDE.editor.hyperlink_file(true, Isabelle_Export.vfs_prefix + name).follow(view)
           }
           true
 
         case XML.Elem(Markup(Markup.JEDIT_ACTION, _), body) =>
           GUI_Thread.later {
             view.getInputHandler.invokeAction(XML.content(body))
           }
           true
 
         case XML.Elem(Markup(Markup.SIMP_TRACE_PANEL, props), _) =>
           val link =
             props match {
               case Position.Id(id) => PIDE.editor.hyperlink_command(true, snapshot, id)
               case _ => None
             }
           GUI_Thread.later {
             link.foreach(_.follow(view))
             view.getDockableWindowManager.showDockableWindow("isabelle-simplifier-trace")
           }
           true
 
         case XML.Elem(Markup(Markup.SENDBACK, props), _) =>
           if (buffer.isEditable) {
             props match {
               case Position.Id(id) =>
                 Isabelle.edit_command(snapshot, text_area,
                   props.contains(Markup.PADDING_COMMAND), id, text)
               case _ =>
                 if (props.contains(Markup.PADDING_LINE))
                   Isabelle.insert_line_padding(text_area, text)
                 else text_area.setSelectedText(text)
             }
             text_area.requestFocus
           }
           true
 
         case Protocol.Dialog(id, serial, result) =>
           model.session.dialog_result(id, serial, result)
           true
 
         case _ => false
       }
     }
   }
 }