diff -r 51408dde956f -r 50f141b34bb7 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Thu Dec 13 17:46:33 2012 +0100 +++ b/src/Pure/PIDE/markup.scala Thu Dec 13 18:00:24 2012 +0100 @@ -286,7 +286,7 @@ val PADDING_LINE = (PADDING, LINE) val DIALOG = "dialog" - val Result = new Properties.String("result") + val Result = new Properties.String(RESULT) /* protocol message functions */