src/Pure/PIDE/markup.scala
changeset 50503 50f141b34bb7
parent 50501 6f41f1646617
child 50543 42bbe637be54
equal deleted inserted replaced
50502:51408dde956f 50503:50f141b34bb7
   284   val SENDBACK = "sendback"
   284   val SENDBACK = "sendback"
   285   val PADDING = "padding"
   285   val PADDING = "padding"
   286   val PADDING_LINE = (PADDING, LINE)
   286   val PADDING_LINE = (PADDING, LINE)
   287 
   287 
   288   val DIALOG = "dialog"
   288   val DIALOG = "dialog"
   289   val Result = new Properties.String("result")
   289   val Result = new Properties.String(RESULT)
   290 
   290 
   291 
   291 
   292   /* protocol message functions */
   292   /* protocol message functions */
   293 
   293 
   294   val FUNCTION = "function"
   294   val FUNCTION = "function"