| changeset 83297 | 00bb83e60336 |
| parent 83294 | 8d30612cff2d |
| child 83299 | 7d8713e1890b |
--- a/src/Pure/PIDE/markup.scala Fri Oct 17 11:03:16 2025 +0200 +++ b/src/Pure/PIDE/markup.scala Fri Oct 17 15:13:45 2025 +0200 @@ -560,6 +560,8 @@ val CONSOLIDATING = "consolidating" val CONSOLIDATED = "consolidated" + val command_running: Properties.Entry = (COMMAND, RUNNING) + /* interactive documents */