src/Pure/PIDE/markup.scala
changeset 66873 9953ae603a23
parent 66872 69afe45a6062
child 66942 91a21a5631ae
     1.1 --- a/src/Pure/PIDE/markup.scala	Mon Oct 16 14:21:14 2017 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Mon Oct 16 14:32:09 2017 +0200
     1.3 @@ -392,9 +392,11 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* command timing */
     1.8 +  /* protocol functions */
     1.9  
    1.10 -  val COMMAND_TIMING = "command_timing"
    1.11 +  val COMMAND_TIMING: Properties.Entry = (FUNCTION, "command_timing")
    1.12 +
    1.13 +  val THEORY_TIMING: Properties.Entry = (FUNCTION, "theory_timing")
    1.14  
    1.15  
    1.16    /* command indentation */