src/Pure/General/completion.ML
changeset 55977 ec4830499634
parent 55917 5438ed05e1c9
child 56293 9bc33476f6ac
equal deleted inserted replaced
55976:43815ee659bc 55977:ec4830499634
     5 *)
     5 *)
     6 
     6 
     7 signature COMPLETION =
     7 signature COMPLETION =
     8 sig
     8 sig
     9   type T
     9   type T
    10   val names: Position.T -> (string * string) list -> T
    10   val names: Position.T -> (string * (string * string)) list -> T
    11   val none: T
    11   val none: T
    12   val reported_text: T -> string
    12   val reported_text: T -> string
    13   val report: T -> unit
    13   val report: T -> unit
    14   val suppress_abbrevs: string -> Markup.T list
    14   val suppress_abbrevs: string -> Markup.T list
    15 end;
    15 end;
    16 
    16 
    17 structure Completion: COMPLETION =
    17 structure Completion: COMPLETION =
    18 struct
    18 struct
    19 
    19 
    20 abstype T = Completion of {pos: Position.T, total: int, names: (string * string) list}
    20 abstype T =
       
    21   Completion of {pos: Position.T, total: int, names: (string * (string * string)) list}
    21 with
    22 with
    22 
    23 
    23 (* completion of names *)
    24 (* completion of names *)
    24 
    25 
    25 fun dest (Completion args) = args;
    26 fun dest (Completion args) = args;
    38   let val {pos, total, names} = dest completion in
    39   let val {pos, total, names} = dest completion in
    39     if Position.is_reported pos andalso not (null names) then
    40     if Position.is_reported pos andalso not (null names) then
    40       let
    41       let
    41         val markup = Position.markup pos Markup.completion;
    42         val markup = Position.markup pos Markup.completion;
    42         val body = (total, names) |>
    43         val body = (total, names) |>
    43           let open XML.Encode in pair int (list (pair string string)) end;
    44           let open XML.Encode in pair int (list (pair string (pair string string))) end;
    44       in YXML.string_of (XML.Elem (markup, body)) end
    45       in YXML.string_of (XML.Elem (markup, body)) end
    45     else ""
    46     else ""
    46   end;
    47   end;
    47 
    48 
    48 val report = Output.report o reported_text;
    49 val report = Output.report o reported_text;