| changeset 83226 | 37b61794a93a |
| parent 83224 | 14d83daeaafc |
| child 83242 | a4e47c1617c9 |
--- a/src/Pure/PIDE/markup.scala Wed Sep 24 16:53:36 2025 +0200 +++ b/src/Pure/PIDE/markup.scala Wed Sep 24 17:41:36 2025 +0200 @@ -721,6 +721,7 @@ } object Task_Statistics extends Properties_Function("task_statistics") + val Commands = new Properties.Int("commands") object Loading_Theory extends Properties_Function("loading_theory") object Build_Session_Finished extends Function("build_session_finished")