# HG changeset patch
# User wenzelm
# Date 1394025594 -3600
# Node ID 607948c90bf0d92f7696a39e8695cc618b8f70e4
# Parent  c5b752d549e312eb9fe084914d8f45acb48b3adb
suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
tuned signature;

diff -r c5b752d549e3 -r 607948c90bf0 src/Pure/General/completion.ML
--- a/src/Pure/General/completion.ML	Wed Mar 05 13:11:08 2014 +0100
+++ b/src/Pure/General/completion.ML	Wed Mar 05 14:19:54 2014 +0100
@@ -11,6 +11,7 @@
   val none: T
   val reported_text: T -> string
   val report: T -> unit
+  val suppress_abbrevs: string -> Markup.T list
 end;
 
 structure Completion: COMPLETION =
@@ -19,6 +20,8 @@
 abstype T = Completion of {pos: Position.T, total: int, names: (string * string) list}
 with
 
+(* completion of names *)
+
 fun dest (Completion args) = args;
 
 fun names pos names =
@@ -44,4 +47,12 @@
 
 val report = Output.report o reported_text;
 
+
+(* suppress short abbreviations *)
+
+fun suppress_abbrevs s =
+  if not (Symbol.is_ascii_identifier s) andalso (length (Symbol.explode s) = 1 orelse s = "::")
+  then [Markup.no_completion]
+  else [];
+
 end;
diff -r c5b752d549e3 -r 607948c90bf0 src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Wed Mar 05 13:11:08 2014 +0100
+++ b/src/Pure/Isar/args.ML	Wed Mar 05 14:19:54 2014 +0100
@@ -85,12 +85,12 @@
     val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
     fun prt arg =
       (case Token.get_value arg of
-        SOME (v as Token.Literal s) => Pretty.marks_str (Token.value_markup false v, s)
+        SOME (v as Token.Literal s) => Pretty.marks_str (Token.value_markup v, s)
       | SOME (Token.Text s) => Pretty.str (quote s)
       | SOME (Token.Typ T) => Syntax.pretty_typ ctxt T
       | SOME (Token.Term t) => Syntax.pretty_term ctxt t
       | SOME (Token.Fact ths) => Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
-      | _ => Pretty.mark_str (#1 (Token.markup arg), Token.unparse arg));
+      | _ => Pretty.mark_str (Token.markup arg, Token.unparse arg));
     val (s, args) = #1 (dest_src src);
   in Pretty.block (Pretty.breaks (Pretty.str s :: map prt args)) end;
 
diff -r c5b752d549e3 -r 607948c90bf0 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Wed Mar 05 13:11:08 2014 +0100
+++ b/src/Pure/Isar/token.ML	Wed Mar 05 14:19:54 2014 +0100
@@ -42,8 +42,11 @@
   val inner_syntax_of: T -> string
   val source_position_of: T -> Symbol_Pos.source
   val content_of: T -> string
-  val markup: T -> Markup.T * string
-  val value_markup: bool -> value -> Markup.T list
+  val keyword_markup: string -> Markup.T
+  val value_markup: value -> Markup.T list
+  val completion_report: T -> Position.report_text list
+  val report: T -> Position.report_text
+  val markup: T -> Markup.T
   val unparse: T -> string
   val print: T -> string
   val text_of: T -> string * string
@@ -225,7 +228,7 @@
 fun content_of (Token (_, (_, x), _)) = x;
 
 
-(* markup *)
+(* markup reports *)
 
 local
 
@@ -251,23 +254,29 @@
   | Sync          => (Markup.control, "")
   | EOF           => (Markup.control, "");
 
+in
+
 fun keyword_markup x =
   if Symbol.is_ascii_identifier x
   then Markup.keyword2
   else Markup.operator;
 
-in
+fun value_markup (Literal x) = keyword_markup x :: Completion.suppress_abbrevs x
+  | value_markup _ = [];
 
-fun markup tok =
+fun completion_report tok =
   if is_kind Keyword tok
-  then (keyword_markup (content_of tok), "")
-  else token_kind_markup (kind_of tok);
+  then map (fn m => ((pos_of tok, m), "")) (Completion.suppress_abbrevs (content_of tok))
+  else [];
 
-fun value_markup known_keyword (Literal x) =
-      (if known_keyword then [] else [keyword_markup x]) @
-      (if Symbol.is_ascii_identifier x orelse length (Symbol.explode x) > 1 then []
-       else [Markup.no_completion])
-  | value_markup _ _ = [];
+fun report tok =
+  if is_kind Keyword tok then
+    ((pos_of tok, keyword_markup (content_of tok)), "")
+  else
+    let val (m, text) = token_kind_markup (kind_of tok)
+    in ((pos_of tok, m), text) end;
+
+val markup = #2 o #1 o report;
 
 end;
 
@@ -285,14 +294,14 @@
   | EOF => ""
   | _ => x);
 
-fun print tok = Markup.markup (#1 (markup tok)) (unparse tok);
+fun print tok = Markup.markup (markup tok) (unparse tok);
 
 fun text_of tok =
   if is_semicolon tok then ("terminator", "")
   else
     let
       val k = str_of_kind (kind_of tok);
-      val (m, _) = markup tok;
+      val m = markup tok;
       val s = unparse tok;
     in
       if s = "" then (k, "")
@@ -327,13 +336,10 @@
   (case get_value tok of
     NONE => []
   | SOME v =>
-      let
-        val pos = pos_of tok;
-        val known_keyword = is_kind Keyword tok;
-      in
-        if Position.is_reported pos then map (pair pos) (value_markup known_keyword v)
-        else []
-      end);
+      if is_kind Keyword tok then []
+      else
+        let val pos = pos_of tok
+        in if Position.is_reported pos then map (pair pos) (value_markup v) else [] end);
 
 
 (* make values *)
diff -r c5b752d549e3 -r 607948c90bf0 src/Pure/Thy/thy_syntax.ML
--- a/src/Pure/Thy/thy_syntax.ML	Wed Mar 05 13:11:08 2014 +0100
+++ b/src/Pure/Thy/thy_syntax.ML	Wed Mar 05 14:19:54 2014 +0100
@@ -51,8 +51,7 @@
           if Symbol.is_malformed sym
           then SOME ((pos, Markup.bad), "Malformed symbolic character") else NONE);
     val is_malformed = Token.is_error tok orelse not (null malformed_symbols);
-    val (markup, msg) = Token.markup tok;
-    val reports = ((Token.pos_of tok, markup), msg) :: malformed_symbols;
+    val reports = Token.report tok :: Token.completion_report tok @ malformed_symbols;
   in (is_malformed, reports) end;
 
 in
@@ -62,7 +61,7 @@
   in (exists fst results, maps snd results) end;
 
 fun present_token tok =
-  Markup.enclose (fst (Token.markup tok)) (Output.output (Token.unparse tok));
+  Markup.enclose (Token.markup tok) (Output.output (Token.unparse tok));
 
 end;