src/Pure/PIDE/protocol.scala

 */
 
 package isabelle
 
 
-object Protocol
-{
+object Protocol {
   /* markers for inlined messages */
 
   val Loading_Theory_Marker = Protocol_Message.Marker("loading_theory")
   val Meta_Info_Marker = Protocol_Message.Marker("meta_info")
   val Command_Timing_Marker = Protocol_Message.Marker("command_timing")

   val Error_Message_Marker = Protocol_Message.Marker("error_message")
 
 
   /* batch build */
 
-  object Loading_Theory
-  {
+  object Loading_Theory {
     def unapply(props: Properties.T): Option[(Document.Node.Name, Document_ID.Exec)] =
       (props, props, props) match {
         case (Markup.Name(name), Position.File(file), Position.Id(id))
         if Path.is_wellformed(file) =>
           val master_dir = Path.explode(file).dir.implode

   }
 
 
   /* document editing */
 
-  object Commands_Accepted
-  {
+  object Commands_Accepted {
     def unapply(text: String): Option[List[Document_ID.Command]] =
       try { Some(space_explode(',', text).map(Value.Long.parse)) }
       catch { case ERROR(_) => None }
 
     val message: XML.Elem = XML.elem(Markup.STATUS, List(XML.elem(Markup.ACCEPTED)))
   }
 
-  object Assign_Update
-  {
-    def unapply(text: String)
-      : Option[(Document_ID.Version, List[String], Document.Assign_Update)] =
-    {
+  object Assign_Update {
+    def unapply(
+      text: String
+    ) : Option[(Document_ID.Version, List[String], Document.Assign_Update)] = {
       try {
         import XML.Decode._
         def decode_upd(body: XML.Body): (Long, List[Long]) =
           space_explode(',', string(body)).map(Value.Long.parse) match {
             case a :: bs => (a, bs)

         case _: XML.Error => None
       }
     }
   }
 
-  object Removed
-  {
+  object Removed {
     def unapply(text: String): Option[List[Document_ID.Version]] =
       try {
         import XML.Decode._
         Some(list(long)(Symbol.decode_yxml(text)))
       }

   }
 
 
   /* command timing */
 
-  object Command_Timing
-  {
+  object Command_Timing {
     def unapply(props: Properties.T): Option[(Properties.T, Document_ID.Generic, isabelle.Timing)] =
       props match {
         case Markup.Command_Timing(args) =>
           (args, args) match {
             case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((args, id, timing))

   }
 
 
   /* theory timing */
 
-  object Theory_Timing
-  {
+  object Theory_Timing {
     def unapply(props: Properties.T): Option[(String, isabelle.Timing)] =
       props match {
         case Markup.Theory_Timing(args) =>
           (args, args) match {
             case (Markup.Name(name), Markup.Timing_Properties(timing)) => Some((name, timing))

   def message_text(elem: XML.Elem,
     heading: Boolean = false,
     pos: Position.T = Position.none,
     margin: Double = Pretty.default_margin,
     breakgain: Double = Pretty.default_breakgain,
-    metric: Pretty.Metric = Pretty.Default_Metric): String =
-  {
+    metric: Pretty.Metric = Pretty.Default_Metric
+  ): String = {
     val text1 =
       if (heading) {
         val h =
           if (is_warning(elem) || is_legacy(elem)) "Warning"
           else if (is_error(elem)) "Error"

   }
 
 
   /* ML profiling */
 
-  object ML_Profiling
-  {
+  object ML_Profiling {
     def unapply(msg: XML.Tree): Option[isabelle.ML_Profiling.Report] =
       msg match {
         case XML.Elem(_, List(tree)) if is_tracing(msg) =>
           Markup.ML_Profiling.unapply_report(tree)
         case _ => None

   }
 
 
   /* export */
 
-  object Export
-  {
+  object Export {
     sealed case class Args(
       id: Option[String] = None,
       serial: Long = 0L,
       theory_name: String,
       name: String,
       executable: Boolean = false,
       compress: Boolean = true,
-      strict: Boolean = true)
-    {
+      strict: Boolean = true
+    ) {
       def compound_name: String = isabelle.Export.compound_name(theory_name, name)
     }
 
     def unapply(props: Properties.T): Option[Args] =
       props match {

   }
 
 
   /* breakpoints */
 
-  object ML_Breakpoint
-  {
+  object ML_Breakpoint {
     def unapply(tree: XML.Tree): Option[Long] =
     tree match {
       case XML.Elem(Markup(Markup.ML_BREAKPOINT, Markup.Serial(breakpoint)), _) => Some(breakpoint)
       case _ => None
     }
   }
 
 
   /* dialogs */
 
-  object Dialog_Args
-  {
+  object Dialog_Args {
     def unapply(props: Properties.T): Option[(Document_ID.Generic, Long, String)] =
       (props, props, props) match {
         case (Position.Id(id), Markup.Serial(serial), Markup.Result(result)) =>
           Some((id, serial, result))
         case _ => None
       }
   }
 
-  object Dialog
-  {
+  object Dialog {
     def unapply(tree: XML.Tree): Option[(Document_ID.Generic, Long, String)] =
       tree match {
         case XML.Elem(Markup(Markup.DIALOG, Dialog_Args(id, serial, result)), _) =>
           Some((id, serial, result))
         case _ => None
       }
   }
 
-  object Dialog_Result
-  {
-    def apply(id: Document_ID.Generic, serial: Long, result: String): XML.Elem =
-    {
+  object Dialog_Result {
+    def apply(id: Document_ID.Generic, serial: Long, result: String): XML.Elem = {
       val props = Position.Id(id) ::: Markup.Serial(serial)
       XML.Elem(Markup(Markup.RESULT, props), List(XML.Text(result)))
     }
 
     def unapply(tree: XML.Tree): Option[String] =

       }
   }
 }
 
 
-trait Protocol
-{
+trait Protocol {
   /* protocol commands */
 
   def protocol_command_raw(name: String, args: List[Bytes]): Unit
   def protocol_command_args(name: String, args: List[String]): Unit
   def protocol_command(name: String, args: String*): Unit

   /* interned items */
 
   def define_blob(digest: SHA1.Digest, bytes: Bytes): Unit =
     protocol_command_raw("Document.define_blob", List(Bytes(digest.toString), bytes))
 
-  private def encode_command(resources: Resources, command: Command)
-    : (String, String, String, String, String, List[String]) =
-  {
+  private def encode_command(
+    resources: Resources,
+    command: Command
+  ) : (String, String, String, String, String, List[String]) = {
     import XML.Encode._
 
     val parents = command.theory_parents(resources).map(name => File.standard_url(name.node))
     val parents_yxml = Symbol.encode_yxml(list(string)(parents))
 
-    val blobs_yxml =
-    {
+    val blobs_yxml = {
       val encode_blob: T[Exn.Result[Command.Blob]] =
         variant(List(
           { case Exn.Res(Command.Blob(a, b, c)) =>
               (Nil, triple(string, string, option(string))(
                 (a.node, b.implode, c.map(p => p._1.toString)))) },
           { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
 
       Symbol.encode_yxml(pair(list(encode_blob), int)(command.blobs, command.blobs_index))
     }
 
-    val toks_yxml =
-    {
+    val toks_yxml = {
       val encode_tok: T[Token] = (tok => pair(int, int)((tok.kind.id, Symbol.length(tok.source))))
       Symbol.encode_yxml(list(encode_tok)(command.span.content))
     }
     val toks_sources = command.span.content.map(tok => Symbol.encode(tok.source))
 
     (Document_ID(command.id), Symbol.encode(command.span.name), parents_yxml,
       blobs_yxml, toks_yxml, toks_sources)
   }
 
-  def define_command(resources: Resources, command: Command): Unit =
-  {
+  def define_command(resources: Resources, command: Command): Unit = {
     val (command_id, name, parents_yxml, blobs_yxml, toks_yxml, toks_sources) =
       encode_command(resources, command)
     protocol_command_args(
       "Document.define_command", command_id :: name :: parents_yxml :: blobs_yxml ::
         toks_yxml :: toks_sources)
   }
 
-  def define_commands(resources: Resources, commands: List[Command]): Unit =
-  {
+  def define_commands(resources: Resources, commands: List[Command]): Unit = {
     protocol_command_args("Document.define_commands",
-      commands.map(command =>
-      {
+      commands.map(command => {
         import XML.Encode._
         val (command_id, name, parents_yxml, blobs_yxml, toks_yxml, toks_sources) =
           encode_command(resources, command)
         val body =
           pair(string, pair(string, pair(string, pair(string, pair(string, list(string))))))(
             command_id, (name, (parents_yxml, (blobs_yxml, (toks_yxml, toks_sources)))))
         YXML.string_of_body(body)
       }))
   }
 
-  def define_commands_bulk(resources: Resources, commands: List[Command]): Unit =
-  {
+  def define_commands_bulk(resources: Resources, commands: List[Command]): Unit = {
     val (irregular, regular) = commands.partition(command => YXML.detect(command.source))
     irregular.foreach(define_command(resources, _))
     regular match {
       case Nil =>
       case List(command) => define_command(resources, command)

     protocol_command("Document.cancel_exec", Document_ID(id))
 
 
   /* document versions */
 
-  def update(old_id: Document_ID.Version, new_id: Document_ID.Version,
-    edits: List[Document.Edit_Command], consolidate: List[Document.Node.Name]): Unit =
-  {
-    val consolidate_yxml =
-    {
+  def update(
+    old_id: Document_ID.Version,
+    new_id: Document_ID.Version,
+    edits: List[Document.Edit_Command],
+    consolidate: List[Document.Node.Name]
+  ): Unit = {
+    val consolidate_yxml = {
       import XML.Encode._
       Symbol.encode_yxml(list(string)(consolidate.map(_.node)))
     }
-    val edits_yxml =
-    {
+    val edits_yxml = {
       import XML.Encode._
       def id: T[Command] = (cmd => long(cmd.id))
       def encode_edit(name: Document.Node.Name)
           : T[Document.Node.Edit[Command.Edit, Command.Perspective]] =
         variant(List(

     }
     protocol_command_args("Document.update",
       Document_ID(old_id) :: Document_ID(new_id) :: consolidate_yxml :: edits_yxml)
   }
 
-  def remove_versions(versions: List[Document.Version]): Unit =
-  {
+  def remove_versions(versions: List[Document.Version]): Unit = {
     val versions_yxml =
     { import XML.Encode._
       Symbol.encode_yxml(list(long)(versions.map(_.id))) }
     protocol_command("Document.remove_versions", versions_yxml)
   }