src/Pure/PIDE/markup.scala
changeset 55694 a1184dfb8e00
parent 55687 78c83cd477c1
child 55744 4a4e5686e091
equal deleted inserted replaced
55693:93ba0085e888 55694:a1184dfb8e00
    67   }
    67   }
    68 
    68 
    69 
    69 
    70   /* completion */
    70   /* completion */
    71 
    71 
    72   val TOTAL = "total"
       
    73   val COMPLETION = "completion"
    72   val COMPLETION = "completion"
    74 
    73 
    75 
    74 
    76   /* position */
    75   /* position */
    77 
    76