src/Pure/General/completion.ML
changeset 55672 5e25cc741ab9
child 55674 8a213ab0e78a
equal deleted inserted replaced
55671:aeca05e62fef 55672:5e25cc741ab9
       
     1 (*  Title:      Pure/Isar/completion.ML
       
     2     Author:     Makarius
       
     3 
       
     4 Completion within the formal context.
       
     5 *)
       
     6 
       
     7 signature COMPLETION =
       
     8 sig
       
     9   val limit: unit -> int
       
    10   type T = {original: string, replacements: string list}
       
    11   val none: T
       
    12   val reported_text: Position.T -> T -> string
       
    13   val report: Position.T -> T -> unit
       
    14 end;
       
    15 
       
    16 structure Completion: COMPLETION =
       
    17 struct
       
    18 
       
    19 fun limit () = Options.default_int "completion_limit";
       
    20 
       
    21 
       
    22 type T = {original: string, replacements: string list};
       
    23 
       
    24 val none: T = {original = "", replacements = []};
       
    25 
       
    26 fun encode ({original, replacements}: T) =
       
    27   (original, replacements)
       
    28   |> let open XML.Encode in pair string (list string) end;
       
    29 
       
    30 fun reported_text pos (completion: T) =
       
    31   if null (#replacements completion) then ""
       
    32   else Position.reported_text pos Markup.completion (YXML.string_of_body (encode completion));
       
    33 
       
    34 fun report pos completion =
       
    35   Output.report (reported_text pos completion);
       
    36 
       
    37 end;