diff -r 679c2617f312 -r 7b1b7ac616c0 src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Tue Nov 04 17:20:20 2025 +0100 +++ b/src/Pure/PIDE/command.scala Tue Nov 04 20:11:15 2025 +0100 @@ -217,7 +217,7 @@ markups: Markups = Markups.empty, ): State = { new State(command, results, exports, markups, - Document_Status.Command_Status.make(Time.now(), + Document_Status.Command_Status.make(Date.now(), warned = results.warned, failed = results.failed)) } @@ -252,11 +252,11 @@ new Command(id, command.node_name, command.blobs_info, command.span, command.source, results, exports, markups, document_status) - private def add_status(now: Time, st: Markup): State = + private def add_status(now: Date, st: Markup): State = new State(command, results, exports, markups, document_status.update(now, markups = List(st))) - private def add_result(now: Time, entry: Results.Entry): State = + private def add_result(now: Date, entry: Results.Entry): State = new State(command, results + entry, exports, markups, document_status.update(now, warned = Results.warned(entry), @@ -282,7 +282,7 @@ } def accumulate( - now: Time, + now: Date, self_id: Document_ID.Generic => Boolean, other_id: (Document.Node.Name, Document_ID.Generic) => Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)], @@ -623,7 +623,7 @@ lazy val init_state: Command.State = new Command.State(this, init_results, init_exports, init_markups, - init_document_status.update(Time.now(), + init_document_status.update(Date.now(), warned = init_results.warned, failed = init_results.failed))