src/Pure/Isar/document_structure.scala

     def buffer(): mutable.ListBuffer[Document] = new mutable.ListBuffer[Document]
 
     var stack: List[(Command, mutable.ListBuffer[Document])] =
       List((Command.empty, buffer()))
 
-    def open(command: Command) { stack = (command, buffer()) :: stack }
+    def open(command: Command): Unit = { stack = (command, buffer()) :: stack }
 
     def close(): Boolean =
       stack match {
         case (command, body) :: (_, body2) :: _ =>
           body2 += Block(command.span.name, command.source, body.toList)

           true
         case _ =>
           false
       }
 
-    def flush() { if (is_plain_theory(stack.head._1)) close() }
+    def flush(): Unit = if (is_plain_theory(stack.head._1)) close()
 
     def result(): List[Document] =
     {
       while (close()) { }
       stack.head._2.toList
     }
 
-    def add(command: Command)
+    def add(command: Command): Unit =
     {
       if (command.span.is_begin || is_plain_theory(command)) { flush(); open(command) }
       else if (command.span.is_end) { flush(); close() }
 
       stack.head._2 += Atom(command.source.length)

     private def buffer(): mutable.ListBuffer[Document] = new mutable.ListBuffer[Document]
 
     private var stack: List[(Int, Item, mutable.ListBuffer[Document])] =
       List((0, No_Item, buffer()))
 
-    @tailrec private def close(level: Int => Boolean)
+    @tailrec private def close(level: Int => Boolean): Unit =
     {
       stack match {
         case (lev, item, body) :: (_, _, body2) :: _ if level(lev) =>
           body2 += Block(item.name, item.source, body.toList)
           stack = stack.tail

     {
       close(_ => true)
       stack.head._3.toList
     }
 
-    def add(item: Item)
+    def add(item: Item): Unit =
     {
       item.heading_level match {
         case Some(i) =>
           close(_ > i)
           stack = (i + 1, item, buffer()) :: stack