# 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) } }