src/Pure/PIDE/markup.scala
changeset 69557 e72360fef69a
parent 69320 fc221fa79741
child 69648 97ddaec3e2ae
equal deleted inserted replaced
69556:0a38f23ca4c5 69557:e72360fef69a
   112 
   112 
   113   /* completion */
   113   /* completion */
   114 
   114 
   115   val COMPLETION = "completion"
   115   val COMPLETION = "completion"
   116   val NO_COMPLETION = "no_completion"
   116   val NO_COMPLETION = "no_completion"
       
   117 
       
   118   val UPDATE = "update"
   117 
   119 
   118 
   120 
   119   /* position */
   121   /* position */
   120 
   122 
   121   val LINE = "line"
   123   val LINE = "line"