| changeset 72002 | 5c4800f6b25a |
| parent 71673 | 88dfbc382a3d |
| child 72008 | 7a53fc156c2b |
--- a/src/Pure/PIDE/markup.scala Mon Jul 06 16:52:48 2020 +0200 +++ b/src/Pure/PIDE/markup.scala Wed Jul 08 14:43:02 2020 +0200 @@ -575,6 +575,7 @@ object Command_Timing extends Properties_Function("command_timing") object Theory_Timing extends Properties_Function("theory_timing") + object Session_Timing extends Properties_Function("session_timing") object ML_Statistics extends Properties_Function("ML_statistics") object Task_Statistics extends Properties_Function("task_statistics")