src/Pure/PIDE/markup.scala
changeset 50503 50f141b34bb7
parent 50501 6f41f1646617
child 50543 42bbe637be54
     1.1 --- a/src/Pure/PIDE/markup.scala	Thu Dec 13 17:46:33 2012 +0100
     1.2 +++ b/src/Pure/PIDE/markup.scala	Thu Dec 13 18:00:24 2012 +0100
     1.3 @@ -286,7 +286,7 @@
     1.4    val PADDING_LINE = (PADDING, LINE)
     1.5  
     1.6    val DIALOG = "dialog"
     1.7 -  val Result = new Properties.String("result")
     1.8 +  val Result = new Properties.String(RESULT)
     1.9  
    1.10  
    1.11    /* protocol message functions */