src/Pure/PIDE/command.scala

       Symbol.Text_Chunk.File(name.node)
   }
 
   object Blobs_Info
   {
-    val none: Blobs_Info = Blobs_Info(Nil, -1)
+    val none: Blobs_Info = Blobs_Info(Nil)
 
     def errors(msgs: List[String]): Blobs_Info =
-      Blobs_Info(msgs.map(msg => Exn.Exn[Blob](ERROR(msg))), -1)
-  }
-
-  sealed case class Blobs_Info(blobs: List[Exn.Result[Blob]], index: Int)
+      Blobs_Info(msgs.map(msg => Exn.Exn[Blob](ERROR(msg))))
+  }
+
+  sealed case class Blobs_Info(blobs: List[Exn.Result[Blob]], index: Int = -1)
 
 
 
   /** accumulated results from prover **/
 

               val src_path = Path.explode(file)
               val name = Document.Node.Name(resources.append(node_name, src_path))
               val content = get_blob(name).map(blob => (blob.bytes.sha1_digest, blob.chunk))
               Blob(name, src_path, content)
             }).user_error)
-        Blobs_Info(blobs, loaded_files.index)
+        Blobs_Info(blobs, index = loaded_files.index)
     }
   }
 
   def build_blobs_info(
     syntax: Outer_Syntax,

           val src_path = Path.explode(file)
           val name = Document.Node.Name((dir + src_path).expand.implode_symbolic)
           Blob.read_file(name, src_path)
         }).user_error
       }
-    Blobs_Info(blobs, -1)
+    Blobs_Info(blobs)
   }
 }
 
 
 final class Command private(