src/Pure/PIDE/markup.ML
changeset 55694 a1184dfb8e00
parent 55687 78c83cd477c1
child 55744 4a4e5686e091
     1.1 --- a/src/Pure/PIDE/markup.ML	Sun Feb 23 20:24:33 2014 +0100
     1.2 +++ b/src/Pure/PIDE/markup.ML	Sun Feb 23 21:11:59 2014 +0100
     1.3 @@ -37,8 +37,7 @@
     1.4    val get_entity_kind: T -> string option
     1.5    val defN: string
     1.6    val refN: string
     1.7 -  val totalN: string
     1.8 -  val completionN: string
     1.9 +  val completionN: string val completion: T
    1.10    val lineN: string
    1.11    val offsetN: string
    1.12    val end_offsetN: string
    1.13 @@ -287,8 +286,7 @@
    1.14  
    1.15  (* completion *)
    1.16  
    1.17 -val totalN = "total";
    1.18 -val completionN = "completion";
    1.19 +val (completionN, completion) = markup_elem "completion";
    1.20  
    1.21  
    1.22  (* position *)