| changeset 82092 | 93195437fdee |
| parent 81565 | bf19ea589f99 |
| child 82316 | 83584916b6d7 |
--- a/src/Pure/PIDE/markup.ML Thu Feb 06 12:18:56 2025 +0100 +++ b/src/Pure/PIDE/markup.ML Thu Feb 06 12:46:13 2025 +0100 @@ -703,9 +703,9 @@ val gcN = "gc"; fun timing_properties {elapsed, cpu, gc} = - [(elapsedN, Value.print_time elapsed), - (cpuN, Value.print_time cpu), - (gcN, Value.print_time gc)]; + [(elapsedN, Time.print elapsed), + (cpuN, Time.print cpu), + (gcN, Time.print gc)]; val timingN = "timing"; fun timing t = (timingN, timing_properties t);