src/Pure/PIDE/markup.scala
changeset 63681 d2448471ffba
parent 63475 31016a88197b
child 64358 15c90b744481
     1.1 --- a/src/Pure/PIDE/markup.scala	Fri Aug 12 17:53:55 2016 +0200
     1.2 +++ b/src/Pure/PIDE/markup.scala	Fri Aug 12 20:58:05 2016 +0200
     1.3 @@ -472,6 +472,8 @@
     1.4    val DIALOG = "dialog"
     1.5    val Result = new Properties.String(RESULT)
     1.6  
     1.7 +  val JEDIT_ACTION = "jedit_action"
     1.8 +
     1.9  
    1.10    /* protocol message functions */
    1.11