# HG changeset patch
# User wenzelm
# Date 1596748404 -7200
# Node ID 36743e0e2c4cd5a7e9cf4eeb79b48dcca93c38ff
# Parent  a1fb4d28e6090eb26b54bce0391e9152942503d7
unused;

diff -r a1fb4d28e609 -r 36743e0e2c4c src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Thu Aug 06 22:58:18 2020 +0200
+++ b/src/Pure/PIDE/markup.ML	Thu Aug 06 23:13:24 2020 +0200
@@ -165,7 +165,6 @@
   val cpuN: string
   val gcN: string
   val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T
-  val command_timingN: string
   val parse_command_timing_properties:
     Properties.T -> ({file: string, offset: int, name: string} * Time.time) option
   val timingN: string val timing: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> T
@@ -591,8 +590,6 @@
 
 (* command timing *)
 
-val command_timingN = "command_timing";
-
 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) =>