src/Pure/PIDE/markup.scala
changeset 67839 0c2ed45ece20
parent 67336 3ee6da378183
child 67870 586be47e00b3
     1.1 --- a/src/Pure/PIDE/markup.scala	Mon Mar 12 11:37:30 2018 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Mon Mar 12 16:32:33 2018 +0100
     1.3 @@ -457,6 +457,7 @@
     1.4    val STDOUT = "stdout"
     1.5    val STDERR = "stderr"
     1.6    val EXIT = "exit"
     1.7 +  val LOGGER = "logger"
     1.8  
     1.9    val WRITELN_MESSAGE = "writeln_message"
    1.10    val STATE_MESSAGE = "state_message"