tuned whitespace;
authorwenzelm
Fri Apr 25 12:59:33 2014 +0200 (2014-04-25)
changeset 56717d96b10ec397c
parent 56716 6d5733303a50
child 56718 096139bcfadd
tuned whitespace;
src/Pure/Tools/simplifier_trace.scala
     1.1 --- a/src/Pure/Tools/simplifier_trace.scala	Fri Apr 25 12:56:24 2014 +0200
     1.2 +++ b/src/Pure/Tools/simplifier_trace.scala	Fri Apr 25 12:59:33 2014 +0200
     1.3 @@ -104,7 +104,8 @@
     1.4  
     1.5    /* manager actor */
     1.6  
     1.7 -  private case class Handle_Results(session: Session, id: Document_ID.Command, results: Command.Results)
     1.8 +  private case class Handle_Results(
     1.9 +    session: Session, id: Document_ID.Command, results: Command.Results)
    1.10    private case class Generate_Trace(results: Command.Results)
    1.11    private case class Cancel(serial: Long)
    1.12    private object Clear_Memory
    1.13 @@ -115,10 +116,8 @@
    1.14  
    1.15    case class Context(
    1.16      last_serial: Long = 0L,
    1.17 -    questions: SortedMap[Long, Question] = SortedMap.empty
    1.18 -  )
    1.19 +    questions: SortedMap[Long, Question] = SortedMap.empty)
    1.20    {
    1.21 -
    1.22      def +(q: Question): Context =
    1.23        copy(questions = questions + ((q.data.serial, q)))
    1.24  
    1.25 @@ -127,7 +126,6 @@
    1.26  
    1.27      def with_serial(s: Long): Context =
    1.28        copy(last_serial = Math.max(last_serial, s))
    1.29 -
    1.30    }
    1.31  
    1.32    case class Trace(entries: List[Item.Data])
    1.33 @@ -175,7 +173,8 @@
    1.34  
    1.35      def do_reply(session: Session, serial: Long, answer: Answer)
    1.36      {
    1.37 -      session.protocol_command("Simplifier_Trace.reply", Properties.Value.Long(serial), answer.name)
    1.38 +      session.protocol_command(
    1.39 +        "Simplifier_Trace.reply", Properties.Value.Long(serial), answer.name)
    1.40      }
    1.41  
    1.42      loop {
    1.43 @@ -188,7 +187,8 @@
    1.44            {
    1.45              result match {
    1.46                case Item(markup, data) =>
    1.47 -                memory_children += (data.parent -> (memory_children.getOrElse(data.parent, Set.empty) + serial))
    1.48 +                memory_children +=
    1.49 +                  (data.parent -> (memory_children.getOrElse(data.parent, Set.empty) + serial))
    1.50  
    1.51                  markup match {
    1.52  
    1.53 @@ -206,7 +206,8 @@
    1.54                        case Success(false) =>
    1.55                          results.get(data.parent) match {
    1.56                            case Some(Item(Markup.SIMP_TRACE_STEP, _)) =>
    1.57 -                            new_context += Question(data, Answer.hint_fail.all, Answer.hint_fail.default)
    1.58 +                            new_context +=
    1.59 +                              Question(data, Answer.hint_fail.all, Answer.hint_fail.default)
    1.60                            case _ =>
    1.61                              // unknown, better send a default reply
    1.62                              do_reply(session, data.serial, Answer.hint_fail.default)