1.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Thu Dec 06 21:54:43 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Thu Dec 06 22:12:25 2012 +0100
     1.3 @@ -29,12 +29,10 @@
     1.4    /* component state -- owned by Swing thread */
     1.5  
     1.6    private var zoom_factor = 100
     1.7 -  private var show_tracing = false
     1.8    private var do_update = true
     1.9    private var current_snapshot = Document.State.init.snapshot()
    1.10    private var current_state = Command.empty.init_state
    1.11    private var current_output: List[XML.Tree] = Nil
    1.12 -  private var current_tracing = 0
    1.13  
    1.14  
    1.15    /* pretty text area */
    1.16 @@ -71,28 +69,17 @@
    1.17          case None => (current_snapshot, current_state)
    1.18        }
    1.19  
    1.20 -    val (new_output, new_tracing) =
    1.21 +    val new_output =
    1.22        if (!restriction.isDefined || restriction.get.contains(new_state.command))
    1.23 -      {
    1.24 -        val new_output =
    1.25 -          new_state.results.iterator.map(_._2)
    1.26 -            .filter(msg => !Protocol.is_tracing(msg) || show_tracing).toList
    1.27 -        val new_tracing =
    1.28 -          new_state.results.iterator.map(_._2).filter(Protocol.is_tracing(_)).length
    1.29 -        (new_output, new_tracing)
    1.30 -      }
    1.31 -      else (current_output, current_tracing)
    1.32 +        new_state.results.iterator.map(_._2).toList
    1.33 +      else current_output
    1.34  
    1.35      if (new_output != current_output)
    1.36        pretty_text_area.update(new_snapshot, Pretty.separate(new_output))
    1.37  
    1.38 -    if (new_tracing != current_tracing)
    1.39 -      tracing.text = tracing_text(new_tracing)
    1.40 -
    1.41      current_snapshot = new_snapshot
    1.42      current_state = new_state
    1.43      current_output = new_output
    1.44 -    current_tracing = new_tracing
    1.45    }
    1.46  
    1.47  
    1.48 @@ -148,14 +135,6 @@
    1.49    private val zoom = new Library.Zoom_Box(factor => { zoom_factor = factor; handle_resize() })
    1.50    zoom.tooltip = "Zoom factor for basic font size"
    1.51  
    1.52 -  private def tracing_text(n: Int): String = "Tracing (" + n.toString + ")"
    1.53 -  private val tracing = new CheckBox(tracing_text(current_tracing)) {
    1.54 -    reactions += {
    1.55 -      case ButtonClicked(_) => show_tracing = this.selected; handle_update(do_update, None) }
    1.56 -  }
    1.57 -  tracing.selected = show_tracing
    1.58 -  tracing.tooltip = "Indicate output of tracing messages"
    1.59 -
    1.60    private val auto_update = new CheckBox("Auto update") {
    1.61      reactions += {
    1.62        case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None) }
    1.63 @@ -176,7 +155,6 @@
    1.64    }
    1.65    detach.tooltip = "Detach window with static copy of current output"
    1.66  
    1.67 -  private val controls =
    1.68 -    new FlowPanel(FlowPanel.Alignment.Right)(zoom, tracing, auto_update, update, detach)
    1.69 +  private val controls = new FlowPanel(FlowPanel.Alignment.Right)(zoom, auto_update, update, detach)
    1.70    add(controls.peer, BorderLayout.NORTH)
    1.71  }