| changeset 55917 | 5438ed05e1c9 |
| parent 55915 | 607948c90bf0 |
| child 55977 | ec4830499634 |
| 55916:0ac57f18a4b9 | 55917:5438ed05e1c9 |
|---|---|
49 |
49 |
50 |
50 |
51 (* suppress short abbreviations *) |
51 (* suppress short abbreviations *) |
52 |
52 |
53 fun suppress_abbrevs s = |
53 fun suppress_abbrevs s = |
54 if not (Symbol.is_ascii_identifier s) andalso (length (Symbol.explode s) = 1 orelse s = "::") |
54 if not (Symbol.is_ascii_identifier s) andalso (length (Symbol.explode s) <= 1 orelse s = "::") |
55 then [Markup.no_completion] |
55 then [Markup.no_completion] |
56 else []; |
56 else []; |
57 |
57 |
58 end; |
58 end; |