# HG changeset patch
# User wenzelm
# Date 1394029552 -3600
# Node ID 5438ed05e1c9ae71de93b10be7666fcd365a2480
# Parent  0ac57f18a4b93a45ab33dc6b7d2f0e324fda0ad4
special treatment of method combinators like Args.$$$ keywords, although parsed via Parse.$$$;

diff -r 0ac57f18a4b9 -r 5438ed05e1c9 src/Pure/General/completion.ML
--- 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 [];
 
diff -r 0ac57f18a4b9 -r 5438ed05e1c9 src/Pure/Isar/method.ML
--- 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;