# HG changeset patch
# User wenzelm
# Date 1398423573 -7200
# Node ID d96b10ec397caa0f84d749b8b843ab718940e1fa
# Parent  6d5733303a50a21ea7c5a905d74046c12305949b
tuned whitespace;

diff -r 6d5733303a50 -r d96b10ec397c src/Pure/Tools/simplifier_trace.scala
--- a/src/Pure/Tools/simplifier_trace.scala	Fri Apr 25 12:56:24 2014 +0200
+++ b/src/Pure/Tools/simplifier_trace.scala	Fri Apr 25 12:59:33 2014 +0200
@@ -104,7 +104,8 @@
 
   /* manager actor */
 
-  private case class Handle_Results(session: Session, id: Document_ID.Command, results: Command.Results)
+  private case class Handle_Results(
+    session: Session, id: Document_ID.Command, results: Command.Results)
   private case class Generate_Trace(results: Command.Results)
   private case class Cancel(serial: Long)
   private object Clear_Memory
@@ -115,10 +116,8 @@
 
   case class Context(
     last_serial: Long = 0L,
-    questions: SortedMap[Long, Question] = SortedMap.empty
-  )
+    questions: SortedMap[Long, Question] = SortedMap.empty)
   {
-
     def +(q: Question): Context =
       copy(questions = questions + ((q.data.serial, q)))
 
@@ -127,7 +126,6 @@
 
     def with_serial(s: Long): Context =
       copy(last_serial = Math.max(last_serial, s))
-
   }
 
   case class Trace(entries: List[Item.Data])
@@ -175,7 +173,8 @@
 
     def do_reply(session: Session, serial: Long, answer: Answer)
     {
-      session.protocol_command("Simplifier_Trace.reply", Properties.Value.Long(serial), answer.name)
+      session.protocol_command(
+        "Simplifier_Trace.reply", Properties.Value.Long(serial), answer.name)
     }
 
     loop {
@@ -188,7 +187,8 @@
           {
             result match {
               case Item(markup, data) =>
-                memory_children += (data.parent -> (memory_children.getOrElse(data.parent, Set.empty) + serial))
+                memory_children +=
+                  (data.parent -> (memory_children.getOrElse(data.parent, Set.empty) + serial))
 
                 markup match {
 
@@ -206,7 +206,8 @@
                       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, Answer.hint_fail.default)
                           case _ =>
                             // unknown, better send a default reply
                             do_reply(session, data.serial, Answer.hint_fail.default)