equal
deleted
inserted
replaced
78 |
78 |
79 val no_shasum: Shasum = new Shasum(Nil) |
79 val no_shasum: Shasum = new Shasum(Nil) |
80 def flat_shasum(list: List[Shasum]): Shasum = new Shasum(list.flatMap(_.rep)) |
80 def flat_shasum(list: List[Shasum]): Shasum = new Shasum(list.flatMap(_.rep)) |
81 def fake_shasum(text: String): Shasum = new Shasum(Library.trim_split_lines(text)) |
81 def fake_shasum(text: String): Shasum = new Shasum(Library.trim_split_lines(text)) |
82 |
82 |
83 def shasum(digest: Digest, name: String): Shasum = new Shasum(List(digest.toString + " " + name)) |
83 def shasum(digest: Digest, name: String): Shasum = |
84 def shasum_meta_info(digest: Digest): Shasum = shasum(digest, isabelle.setup.Build.META_INFO) |
84 new Shasum(List(digest.toString + " " + name)) |
|
85 def shasum_meta_info(digest: Digest): Shasum = |
|
86 shasum(digest, isabelle.setup.Build.META_INFO) |
85 def shasum_sorted(args: List[(Digest, String)]): Shasum = |
87 def shasum_sorted(args: List[(Digest, String)]): Shasum = |
86 flat_shasum(args.sortBy(_._2).map(shasum)) |
88 flat_shasum(args.sortBy(_._2).map(shasum)) |
87 } |
89 } |