special treatment of method combinators like Args.$$$ keywords, although parsed via Parse.$$$;

--- 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 [];
 

--- a/src/Pure/Isar/method.ML	Wed Mar 05 15:24:06 2014 +0100
+++ b/src/Pure/Isar/method.ML	Wed Mar 05 15:25:52 2014 +0100
@@ -435,7 +435,8 @@
 
 fun reports_of ((text, (pos, _)): text_range) =
   (pos, Markup.language_method) ::
-    map (rpair Markup.keyword3) (keyword_positions text);
+    maps (fn p => map (pair p) (Markup.keyword3 :: Completion.suppress_abbrevs ""))
+      (keyword_positions text);
 
 val report = Position.reports o reports_of;