# HG changeset patch
# User wenzelm
# Date 1607366752 -3600
# Node ID a23e0964f3c3989d0b37f235f7cde361f6332133
# Parent  60f56f623be256e5fe9e3613b9af88eaa653b937
tuned signature;

diff -r 60f56f623be2 -r a23e0964f3c3 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Mon Dec 07 19:22:37 2020 +0100
+++ b/src/Pure/PIDE/command.scala	Mon Dec 07 19:45:52 2020 +0100
@@ -38,13 +38,13 @@
 
   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)
+      Blobs_Info(msgs.map(msg => Exn.Exn[Blob](ERROR(msg))))
   }
 
-  sealed case class Blobs_Info(blobs: List[Exn.Result[Blob]], index: Int)
+  sealed case class Blobs_Info(blobs: List[Exn.Result[Blob]], index: Int = -1)
 
 
 
@@ -475,7 +475,7 @@
               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)
     }
   }
 
@@ -496,7 +496,7 @@
           Blob.read_file(name, src_path)
         }).user_error
       }
-    Blobs_Info(blobs, -1)
+    Blobs_Info(blobs)
   }
 }