src/Pure/PIDE/session.scala

 
   class Outlet[A](dispatcher: Consumer_Thread[() => Unit])
   {
     private val consumers = Synchronized[List[Consumer[A]]](Nil)
 
-    def += (c: Consumer[A]) { consumers.change(Library.update(c)) }
-    def -= (c: Consumer[A]) { consumers.change(Library.remove(c)) }
-
-    def post(a: A)
+    def += (c: Consumer[A]): Unit = consumers.change(Library.update(c))
+    def -= (c: Consumer[A]): Unit = consumers.change(Library.remove(c))
+
+    def post(a: A): Unit =
     {
       for (c <- consumers.value.iterator) {
         dispatcher.send(() =>
           try { c.consume(a) }
           catch {

           commands += command
         }
         delay_flush.invoke()
       }
 
-    def shutdown()
+    def shutdown(): Unit =
     {
       delay_flush.revoke()
       flush()
     }
   }

       Delay.first(consolidate_delay) { manager.send(Consolidate_Execution) }
 
     private val init_state: Option[Set[Document.Node.Name]] = Some(Set.empty)
     private val state = Synchronized(init_state)
 
-    def exit()
+    def exit(): Unit =
     {
       delay.revoke()
       state.change(_ => None)
     }
 
-    def update(new_nodes: Set[Document.Node.Name] = Set.empty)
+    def update(new_nodes: Set[Document.Node.Name] = Set.empty): Unit =
     {
       val active =
         state.change_result(st =>
           (st.isDefined, st.map(nodes => if (nodes.isEmpty) new_nodes else nodes ++ new_nodes)))
       if (active) delay.invoke()

   {
     private val variable = Synchronized[Option[Prover]](None)
 
     def defined: Boolean = variable.value.isDefined
     def get: Prover = variable.value.get
-    def set(p: Prover) { variable.change(_ => Some(p)) }
-    def reset { variable.change(_ => None) }
-    def await_reset() { variable.guarded_access({ case None => Some((), None) case _ => None }) }
+    def set(p: Prover): Unit = variable.change(_ => Some(p))
+    def reset: Unit = variable.change(_ => None)
+    def await_reset(): Unit = variable.guarded_access({ case None => Some((), None) case _ => None })
   }
 
 
   /* file formats and protocol handlers */
 

     /* raw edits */
 
     def handle_raw_edits(
       doc_blobs: Document.Blobs = Document.Blobs.empty,
       edits: List[Document.Edit_Text] = Nil,
-      consolidate: List[Document.Node.Name] = Nil)
+      consolidate: List[Document.Node.Name] = Nil): Unit =
     //{{{
     {
       require(prover.defined, "prover process not defined (handle_raw_edits)")
 
       if (edits.nonEmpty) prover.get.discontinue_execution()

     //}}}
 
 
     /* resulting changes */
 
-    def handle_change(change: Session.Change)
+    def handle_change(change: Session.Change): Unit =
     //{{{
     {
       require(prover.defined, "prover process not defined (handle_change)")
 
       // define commands
       {
         val id_commands = new mutable.ListBuffer[Command]
-        def id_command(command: Command)
+        def id_command(command: Command): Unit =
         {
           for {
             (name, digest) <- command.blobs_defined
             if !global_state.value.defined_blob(digest)
           } {

     //}}}
 
 
     /* prover output */
 
-    def handle_output(output: Prover.Output)
+    def handle_output(output: Prover.Output): Unit =
     //{{{
     {
-      def bad_output()
+      def bad_output(): Unit =
       {
         if (verbose)
           Output.warning("Ignoring bad prover output: " + output.message.toString)
       }
 
-      def change_command(f: Document.State => (Command.State, Document.State))
+      def change_command(f: Document.State => (Command.State, Document.State)): Unit =
       {
         try {
           val st = global_state.change_result(f)
           if (!st.command.span.is_theory) {
             change_buffer.invoke(false, Nil, List(st.command))

       await_stable_snapshot()
     }
     else snapshot
   }
 
-  def start(start_prover: Prover.Receiver => Prover)
+  def start(start_prover: Prover.Receiver => Prover): Unit =
   {
     file_formats
     _phase.change(
       {
         case Session.Inactive =>

       case Session.Terminated(result) => result
       case phase => error("Bad session phase after shutdown: " + quote(phase.print))
     }
   }
 
-  def protocol_command(name: String, args: String*)
-  { manager.send(Protocol_Command(name, args.toList)) }
-
-  def cancel_exec(exec_id: Document_ID.Exec)
-  { manager.send(Cancel_Exec(exec_id)) }
-
-  def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
-  {
+  def protocol_command(name: String, args: String*): Unit =
+    manager.send(Protocol_Command(name, args.toList))
+
+  def cancel_exec(exec_id: Document_ID.Exec): Unit =
+    manager.send(Cancel_Exec(exec_id))
+
+  def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]): Unit =
     if (edits.nonEmpty) manager.send_wait(Session.Raw_Edits(doc_blobs, edits))
-  }
-
-  def update_options(options: Options)
-  { manager.send_wait(Update_Options(options)) }
-
-  def dialog_result(id: Document_ID.Generic, serial: Long, result: String)
-  { manager.send(Session.Dialog_Result(id, serial, result)) }
+
+  def update_options(options: Options): Unit =
+    manager.send_wait(Update_Options(options))
+
+  def dialog_result(id: Document_ID.Generic, serial: Long, result: String): Unit =
+    manager.send(Session.Dialog_Result(id, serial, result))
 }