| changeset 55917 | 5438ed05e1c9 |
| parent 55915 | 607948c90bf0 |
| child 55977 | ec4830499634 |
--- a/src/Pure/General/completion.ML Wed Mar 05 15:24:06 2014 +0100 +++ b/src/Pure/General/completion.ML Wed Mar 05 15:25:52 2014 +0100 @@ -51,7 +51,7 @@ (* suppress short abbreviations *) fun suppress_abbrevs s = - if not (Symbol.is_ascii_identifier s) andalso (length (Symbol.explode s) = 1 orelse s = "::") + if not (Symbol.is_ascii_identifier s) andalso (length (Symbol.explode s) <= 1 orelse s = "::") then [Markup.no_completion] else [];