diff --git a/src/Tools/jEdit/src/output_dockable.scala b/src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala
+++ b/src/Tools/jEdit/src/output_dockable.scala
@@ -1,132 +1,132 @@
 /*  Title:      Tools/jEdit/src/output_dockable.scala
     Author:     Makarius
 
 Dockable window with result message output.
 */
 
 package isabelle.jedit
 
 
 import isabelle._
 
 import java.awt.BorderLayout
 import java.awt.event.{ComponentEvent, ComponentAdapter}
 
 import org.gjt.sp.jedit.View
 
 
 class Output_Dockable(view: View, position: String) extends Dockable(view, position) {
   /* component state -- owned by GUI thread */
 
   private var do_update = true
   private var current_output: List[XML.Tree] = Nil
 
 
   /* pretty text area */
 
   val pretty_text_area = new Pretty_Text_Area(view)
   set_content(pretty_text_area)
 
   override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
 
 
   private def handle_resize(): Unit =
     GUI_Thread.require { pretty_text_area.zoom(zoom) }
 
   private def handle_update(follow: Boolean, restriction: Option[Set[Command]]): Unit = {
     GUI_Thread.require {}
 
     for {
       snapshot <- PIDE.editor.current_node_snapshot(view)
       if follow && !snapshot.is_outdated
     } {
       val (command, results) =
         PIDE.editor.current_command(view, snapshot) match {
           case Some(command) => (command, snapshot.command_results(command))
           case None => (Command.empty, Command.Results.empty)
         }
 
       val new_output =
         if (restriction.isEmpty || restriction.get.contains(command))
-          Rendering.output_messages(results, JEdit_Options.output_state())
+          Rendering.output_messages(results, true)
         else current_output
 
       if (current_output != new_output) {
         pretty_text_area.update(snapshot, results, Pretty.separate(new_output))
         current_output = new_output
       }
     }
   }
 
 
   /* controls */
 
   private val output_state_button = new JEdit_Options.output_state.GUI
 
   private val auto_update_button = new GUI.Check("Auto update", init = do_update) {
     tooltip = "Indicate automatic update following cursor movement"
     override def clicked(state: Boolean): Unit = {
       do_update = state
       handle_update(do_update, None)
     }
   }
 
   private val update_button = new GUI.Button("Update") {
     tooltip = "Update display according to the command at cursor position"
     override def clicked(): Unit = handle_update(true, None)
   }
 
   private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() }
 
   private val controls =
     Wrap_Panel(
       List(output_state_button, auto_update_button,
         update_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom))
 
   add(controls.peer, BorderLayout.NORTH)
 
 
   /* main */
 
   private val main =
     Session.Consumer[Any](getClass.getName) {
       case _: Session.Global_Options =>
         GUI_Thread.later {
           handle_resize()
           output_state_button.load()
           handle_update(do_update, None)
         }
 
       case changed: Session.Commands_Changed =>
         val restriction = if (changed.assignment) None else Some(changed.commands)
         GUI_Thread.later { handle_update(do_update, restriction) }
 
       case Session.Caret_Focus =>
         GUI_Thread.later { handle_update(do_update, None) }
     }
 
   override def init(): Unit = {
     PIDE.session.global_options += main
     PIDE.session.commands_changed += main
     PIDE.session.caret_focus += main
     handle_update(true, None)
   }
 
   override def exit(): Unit = {
     PIDE.session.global_options -= main
     PIDE.session.commands_changed -= main
     PIDE.session.caret_focus -= main
     delay_resize.revoke()
   }
 
 
   /* resize */
 
   private val delay_resize =
     Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() }
 
   addComponentListener(new ComponentAdapter {
     override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
     override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
   })
 }