equal
deleted
inserted
replaced
8 sig |
8 sig |
9 type T |
9 type T |
10 val names: Position.T -> (string * (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 |
|
14 val suppress_abbrevs: string -> Markup.T list |
13 val suppress_abbrevs: string -> Markup.T list |
15 end; |
14 end; |
16 |
15 |
17 structure Completion: COMPLETION = |
16 structure Completion: COMPLETION = |
18 struct |
17 struct |
44 let open XML.Encode in pair int (list (pair string (pair string string))) end; |
43 let open XML.Encode in pair int (list (pair string (pair string string))) end; |
45 in YXML.string_of (XML.Elem (markup, body)) end |
44 in YXML.string_of (XML.Elem (markup, body)) end |
46 else "" |
45 else "" |
47 end; |
46 end; |
48 |
47 |
49 val report = Output.report o reported_text; |
|
50 |
|
51 |
48 |
52 (* suppress short abbreviations *) |
49 (* suppress short abbreviations *) |
53 |
50 |
54 fun suppress_abbrevs s = |
51 fun suppress_abbrevs s = |
55 if not (Symbol.is_ascii_identifier s) andalso (length (Symbol.explode s) <= 1 orelse s = "::") |
52 if not (Symbol.is_ascii_identifier s) andalso (length (Symbol.explode s) <= 1 orelse s = "::") |