--- a/src/Pure/General/completion.ML Sun Feb 23 10:44:57 2014 +0100
+++ b/src/Pure/General/completion.ML Sun Feb 23 14:39:51 2014 +0100
@@ -6,32 +6,40 @@
signature COMPLETION =
sig
- val limit: unit -> int
- type T = {original: string, replacements: string list}
+ type T
+ val make: Position.T -> string list -> T
val none: T
- val reported_text: Position.T -> T -> string
- val report: Position.T -> T -> unit
+ val report: T -> unit
end;
structure Completion: COMPLETION =
struct
-fun limit () = Options.default_int "completion_limit";
-
+abstype T = Completion of {pos: Position.T, total: int, names: string list}
+with
-type T = {original: string, replacements: string list};
-
-val none: T = {original = "", replacements = []};
+fun dest (Completion args) = args;
-fun encode ({original, replacements}: T) =
- (original, replacements)
- |> let open XML.Encode in pair string (list string) end;
-
-fun reported_text pos (completion: T) =
- if null (#replacements completion) then ""
- else Position.reported_text pos Markup.completion (YXML.string_of_body (encode completion));
-
-fun report pos completion =
- Output.report (reported_text pos completion);
+fun make pos names =
+ Completion
+ {pos = pos,
+ total = length names,
+ names = take (Options.default_int "completion_limit") names};
end;
+
+val none = make Position.none [];
+
+fun report completion =
+ let val {pos, total, names} = dest completion in
+ if Position.is_reported pos andalso not (null names) then
+ let
+ val props =
+ (Markup.totalN, Markup.print_int total) ::
+ (map Markup.print_int (1 upto length names) ~~ names);
+ val markup = (Markup.completionN, Position.properties_of pos @ props);
+ in Output.report (Markup.markup markup "") end
+ else ()
+ end;
+
+end;
--- a/src/Pure/General/completion.scala Sun Feb 23 10:44:57 2014 +0100
+++ b/src/Pure/General/completion.scala Sun Feb 23 14:39:51 2014 +0100
@@ -1,10 +1,9 @@
/* Title: Pure/General/completion.scala
Author: Makarius
-Semantic completion within the formal context (reported by prover).
+Semantic completion within the formal context (reported names).
Syntactic completion of keywords and symbols, with abbreviations
-(based on language context).
-*/
+(based on language context). */
package isabelle
@@ -18,30 +17,21 @@
{
/** semantic completion **/
- object Reported
+ object Names
{
- object Elem
+ object Info
{
- private def decode: XML.Decode.T[(String, List[String])] =
- {
- import XML.Decode._
- pair(string, list(string))
- }
-
- def unapply(tree: XML.Tree): Option[Reported] =
- tree match {
- case XML.Elem(Markup(Markup.COMPLETION, _), body) =>
- try {
- val (original, replacements) = decode(body)
- Some(Reported(original, replacements))
- }
- catch { case _: XML.Error => None }
+ def unapply(info: Text.Markup): Option[Names] =
+ info.info match {
+ case XML.Elem(Markup(Markup.COMPLETION,
+ (Markup.TOTAL, Properties.Value.Int(total)) :: names), _) =>
+ Some(Names(info.range, total, names.map(_._2)))
case _ => None
}
}
}
- sealed case class Reported(original: String, replacements: List[String])
+ sealed case class Names(range: Text.Range, total: Int, names: List[String])
--- a/src/Pure/General/name_space.ML Sun Feb 23 10:44:57 2014 +0100
+++ b/src/Pure/General/name_space.ML Sun Feb 23 14:39:51 2014 +0100
@@ -205,13 +205,12 @@
fun completion context (space as Name_Space {internals, ...}) (xname, pos) =
if Context_Position.is_visible_generic context andalso Position.is_reported pos then
let
- val replacements =
+ val names =
Symtab.fold (fn (a, (b :: _, _)) => String.isPrefix xname a ? cons b | _ => I)
internals []
- |> take (Completion.limit ())
|> map (extern_shortest (Context.proof_of context) space)
|> sort_distinct string_ord;
- in {original = xname, replacements = replacements} end
+ in Completion.make pos names end
else Completion.none;
@@ -447,7 +446,7 @@
(case Symtab.lookup tab name of
SOME x => (Context_Position.report_generic context pos (markup space name); (name, x))
| NONE =>
- (Completion.report pos (completion context space (xname, pos));
+ (Completion.report (completion context space (xname, pos));
error (undefined (kind_of space) name ^ Position.here pos)))
end;
--- a/src/Pure/PIDE/markup.ML Sun Feb 23 10:44:57 2014 +0100
+++ b/src/Pure/PIDE/markup.ML Sun Feb 23 14:39:51 2014 +0100
@@ -37,7 +37,8 @@
val get_entity_kind: T -> string option
val defN: string
val refN: string
- val completionN: string val completion: T
+ val totalN: string
+ val completionN: string
val lineN: string
val offsetN: string
val end_offsetN: string
@@ -286,7 +287,8 @@
(* completion *)
-val (completionN, completion) = markup_elem "completion";
+val totalN = "total";
+val completionN = "completion";
(* position *)
--- a/src/Pure/PIDE/markup.scala Sun Feb 23 10:44:57 2014 +0100
+++ b/src/Pure/PIDE/markup.scala Sun Feb 23 14:39:51 2014 +0100
@@ -69,6 +69,7 @@
/* completion */
+ val TOTAL = "total"
val COMPLETION = "completion"
--- a/src/Tools/jEdit/src/rendering.scala Sun Feb 23 10:44:57 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Sun Feb 23 14:39:51 2014 +0100
@@ -150,7 +150,7 @@
/* markup elements */
- private val completion_reported_elements = Set(Markup.COMPLETION)
+ private val completion_names_elements = Set(Markup.COMPLETION)
private val completion_context_elements =
Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
@@ -273,20 +273,17 @@
/* completion */
- def completion_reported(caret: Text.Offset): Option[Completion.Reported] =
- if (caret > 0)
+ def completion_names(caret: Text.Offset): Option[Completion.Names] =
+ if (caret > 0 && !snapshot.is_outdated)
{
val result =
snapshot.select(Text.Range(caret - 1, caret + 1),
- Rendering.completion_reported_elements, _ =>
+ Rendering.completion_names_elements, _ =>
{
- case Text.Info(_, Completion.Reported.Elem(reported)) => Some(reported)
+ case Completion.Names.Info(names) => Some(names)
case _ => None
})
- result match {
- case Text.Info(_, reported) :: _ => Some(reported)
- case Nil => None
- }
+ result.headOption.map(_.info)
}
else None
@@ -304,10 +301,7 @@
case Text.Info(_, _) =>
Some(Completion.Context.inner)
})
- result match {
- case Text.Info(_, context) :: _ => Some(context)
- case Nil => None
- }
+ result.headOption.map(_.info)
}
else None