src/Pure/Tools/simplifier_trace.scala

       val continue = Answer("continue", "Continue")
       val continue_trace = Answer("continue_trace", "Continue (with full trace)")
       val continue_passive = Answer("continue_passive", "Continue (without asking)")
       val continue_disable = Answer("continue_disable", "Continue (without any trace)")
 
-      val default = skip
       val all = List(continue, continue_trace, continue_passive, continue_disable, skip)
     }
 
     object hint_fail
     {
       val exit = Answer("exit", "Exit")
       val redo = Answer("redo", "Redo")
 
-      val default = exit
       val all = List(redo, exit)
     }
   }
 
   val all_answers: List[Answer] = Answer.step.all ::: Answer.hint_fail.all
-
-  object Active
-  {
-    def unapply(tree: XML.Tree): Option[(Long, Answer)] =
-      tree match {
-        case XML.Elem(Markup(Markup.SIMP_TRACE, props), _) =>
-          (props, props) match {
-            case (Markup.Serial(serial), Markup.Name(name)) =>
-              all_answers.find(_.name == name).map((serial, _))
-            case _ => None
-          }
-        case _ => None
-      }
-  }
 
 
   /* GUI interaction */
 
   case object Event

   private case class Generate_Trace(results: Command.Results, slot: Promise[Trace])
   private case class Cancel(serial: Long)
   private object Clear_Memory
   case class Reply(session: Session, serial: Long, answer: Answer)
 
-  case class Question(data: Item.Data, answers: List[Answer], default_answer: Answer)
+  case class Question(data: Item.Data, answers: List[Answer])
 
   case class Context(
     last_serial: Long = 0L,
     questions: SortedMap[Long, Question] = SortedMap.empty)
   {

                       val index = Index.of_data(data)
                       memory.get(index) match {
                         case Some(answer) if data.memory =>
                           do_reply(session, serial, answer)
                         case _ =>
-                          new_context += Question(data, Answer.step.all, Answer.step.default)
+                          new_context += Question(data, Answer.step.all)
                       }
 
                     case Markup.SIMP_TRACE_HINT =>
                       data.props match {
                         case Success(false) =>
                           results.get(data.parent) match {
                             case Some(Item(Markup.SIMP_TRACE_STEP, _)) =>
-                              new_context +=
-                                Question(data, Answer.hint_fail.all, Answer.hint_fail.default)
+                              new_context += Question(data, Answer.hint_fail.all)
                             case _ =>
                               // unknown, better send a default reply
-                              do_reply(session, data.serial, Answer.hint_fail.default)
+                              do_reply(session, data.serial, Answer.hint_fail.exit)
                           }
                         case _ =>
                       }
 
                     case Markup.SIMP_TRACE_IGNORE =>

             // Since there are potentially lots of trace messages, we do not cache them here again.
             // Instead, everytime the trace is being requested, we re-assemble it based on the
             // current results.
 
             val items =
-              (for { (_, Item(_, data)) <- results.iterator }
-                yield data).toList
+              results.iterator.collect { case (_, Item(_, data)) => data }.toList
 
             slot.fulfill(Trace(items))
 
           case Cancel(serial) =>
             find_question(serial) match {

             memory_children = Map.empty
             memory = Map.empty
 
           case Reply(session, serial, answer) =>
             find_question(serial) match {
-              case Some((id, Question(data, _, _))) =>
+              case Some((id, Question(data, _))) =>
                 if (data.markup == Markup.SIMP_TRACE_STEP && data.memory)
                 {
                   val index = Index.of_data(data)
                   memory += (index -> answer)
                 }