src/Pure/Tools/simplifier_trace.scala

 
 import scala.annotation.tailrec
 import scala.collection.immutable.SortedMap
 
 
-object Simplifier_Trace
-{
+object Simplifier_Trace {
   /* trace items from the prover */
 
   val TEXT = "text"
   val Text = new Properties.String(TEXT)
 

   val Success = new Properties.Boolean(SUCCESS)
 
   val MEMORY = "memory"
   val Memory = new Properties.Boolean(MEMORY)
 
-  object Item
-  {
+  object Item {
     case class Data(
       serial: Long, markup: String, text: String,
-      parent: Long, props: Properties.T, content: XML.Body)
-    {
+      parent: Long, props: Properties.T, content: XML.Body
+    ) {
       def memory: Boolean = Memory.unapply(props) getOrElse true
     }
 
     def unapply(tree: XML.Tree): Option[(String, Data)] =
       tree match {

 
   /* replies to the prover */
 
   case class Answer private[Simplifier_Trace](val name: String, val string: String)
 
-  object Answer
-  {
-    object step
-    {
+  object Answer {
+    object step {
       val skip = Answer("skip", "Skip")
       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 all = List(continue, continue_trace, continue_passive, continue_disable, skip)
     }
 
-    object hint_fail
-    {
+    object hint_fail {
       val exit = Answer("exit", "Exit")
       val redo = Answer("redo", "Redo")
 
       val all = List(redo, exit)
     }

 
   case class Question(data: Item.Data, answers: List[Answer])
 
   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)))
 
     def -(s: Long): Context =
       copy(questions = questions - s)

 
   case class Trace(entries: List[Item.Data])
 
   case class Index(text: String, content: XML.Body)
 
-  object Index
-  {
+  object Index {
     def of_data(data: Item.Data): Index =
       Index(data.text, data.content)
   }
 
-  def handle_results(session: Session, id: Document_ID.Command, results: Command.Results): Context =
-  {
+  def handle_results(
+    session: Session,
+    id: Document_ID.Command,
+    results: Command.Results
+  ): Context = {
     val slot = Future.promise[Context]
     the_manager(session).send(Handle_Results(session, id, results, slot))
     slot.join
   }
 
-  def generate_trace(session: Session, results: Command.Results): Trace =
-  {
+  def generate_trace(session: Session, results: Command.Results): Trace = {
     val slot = Future.promise[Trace]
     the_manager(session).send(Generate_Trace(results, slot))
     slot.join
   }
 

     the_manager(session).send(Clear_Memory)
 
   def send_reply(session: Session, serial: Long, answer: Answer): Unit =
     the_manager(session).send(Reply(session, serial, answer))
 
-  def make_manager: Consumer_Thread[Any] =
-  {
+  def make_manager: Consumer_Thread[Any] = {
     var contexts = Map.empty[Document_ID.Command, Context]
 
     var memory_children = Map.empty[Long, Set[Long]]
     var memory = Map.empty[Index, Answer]
 

       contexts collectFirst {
         case (id, context) if context.questions contains serial =>
           (id, context.questions(serial))
       }
 
-    def do_cancel(serial: Long, id: Document_ID.Command): Unit =
-    {
+    def do_cancel(serial: Long, id: Document_ID.Command): Unit = {
       // To save memory, we could try to remove empty contexts at this point.
       // However, if a new serial gets attached to the same command_id after we deleted
       // its context, its last_serial counter will start at 0 again, and we'll think the
       // old serials are actually new
       contexts += (id -> (contexts(id) - serial))
     }
 
-    def do_reply(session: Session, serial: Long, answer: Answer): Unit =
-    {
+    def do_reply(session: Session, serial: Long, answer: Answer): Unit = {
       session.protocol_command(
         "Simplifier_Trace.reply", Value.Long(serial), answer.name)
     }
 
     Consumer_Thread.fork[Any]("Simplifier_Trace.manager", daemon = true)(
-      consume = (arg: Any) =>
-      {
+      consume = (arg: Any) => {
         arg match {
           case Handle_Results(session, id, results, slot) =>
             var new_context = contexts.getOrElse(id, Context())
             var new_serial = new_context.last_serial
 
-            for ((serial, result) <- results.iterator if serial > new_context.last_serial)
-            {
+            for ((serial, result) <- results.iterator if serial > new_context.last_serial) {
               result match {
                 case Item(markup, data) =>
                   memory_children +=
                     (data.parent -> (memory_children.getOrElse(data.parent, Set.empty) + serial))
 

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

     }
 
 
   /* protocol handler */
 
-  class Handler extends Session.Protocol_Handler
-  {
+  class Handler extends Session.Protocol_Handler {
     private var the_session: Session = null
 
-    override def init(session: Session): Unit =
-    {
+    override def init(session: Session): Unit = {
       try { the_manager(session) }
       catch { case ERROR(_) => managers.change(map => map + (session -> make_manager)) }
       the_session = session
     }
 
-    override def exit(): Unit =
-    {
+    override def exit(): Unit = {
       val session = the_session
       if (session != null) {
         val manager = the_manager(session)
         manager.send(Clear_Memory)
         manager.shutdown()