--- a/src/Pure/PIDE/markup.ML Mon Sep 22 14:01:37 2025 +0200
+++ b/src/Pure/PIDE/markup.ML Mon Sep 22 15:55:47 2025 +0200
@@ -206,6 +206,7 @@
val cpuN: string
val gcN: string
val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T
+ val command_offsetN: string val command_offset: int option -> T -> T
val parse_command_timing_properties:
Properties.T -> ({file: string, offset: int, name: string} * Time.time) option
val command_indentN: string val command_indent: int -> T
@@ -716,6 +717,11 @@
(* command timing *)
+val command_offsetN = "command_offset";
+fun command_offset offset =
+ let val i = the_default 0 offset
+ in if i = 0 then I else properties [(command_offsetN, Value.print_int i)] end;
+
fun parse_command_timing_properties props =
(case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of
(SOME file, SOME offset, SOME name) =>