--- a/etc/options Sat Feb 22 18:07:31 2014 +0100
+++ b/etc/options Sat Feb 22 20:52:43 2014 +0100
@@ -136,3 +136,9 @@
public option find_theorems_tac_limit : int = 5
-- "limit of tactic search for 'solves' criterion"
+
+section "Completion"
+
+public option completion_limit : int = 40
+ -- "limit for completion within the formal context"
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/completion.ML Sat Feb 22 20:52:43 2014 +0100
@@ -0,0 +1,37 @@
+(* Title: Pure/Isar/completion.ML
+ Author: Makarius
+
+Completion within the formal context.
+*)
+
+signature COMPLETION =
+sig
+ val limit: unit -> int
+ type T = {original: string, replacements: string list}
+ val none: T
+ val reported_text: Position.T -> T -> string
+ val report: Position.T -> T -> unit
+end;
+
+structure Completion: COMPLETION =
+struct
+
+fun limit () = Options.default_int "completion_limit";
+
+
+type T = {original: string, replacements: string list};
+
+val none: T = {original = "", replacements = []};
+
+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);
+
+end;
--- a/src/Pure/General/name_space.ML Sat Feb 22 18:07:31 2014 +0100
+++ b/src/Pure/General/name_space.ML Sat Feb 22 20:52:43 2014 +0100
@@ -27,8 +27,10 @@
val names_unique: bool Config.T
val extern: Proof.context -> T -> string -> xstring
val extern_ord: Proof.context -> T -> string * string -> order
+ val extern_shortest: Proof.context -> T -> string -> xstring
val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
val pretty: Proof.context -> T -> string -> Pretty.T
+ val completion: Context.generic -> T -> xstring * Position.T -> Completion.T
val hide: bool -> string -> T -> T
val merge: T * T -> T
type naming
@@ -151,11 +153,13 @@
if not (null names) andalso hd names = name then cons xname else I) internals [];
-(* intern and extern *)
+(* intern *)
fun intern space xname = #1 (lookup space xname);
+(* extern *)
+
val names_long_raw = Config.declare_option "names_long";
val names_long = Config.bool names_long_raw;
@@ -185,9 +189,30 @@
fun extern_ord ctxt space = string_ord o pairself (extern ctxt space);
+fun extern_shortest ctxt =
+ extern
+ (ctxt
+ |> Config.put names_long false
+ |> Config.put names_short false
+ |> Config.put names_unique false);
+
fun markup_extern ctxt space name = (markup space name, extern ctxt space name);
+fun pretty ctxt space name = Pretty.mark_str (markup_extern ctxt space name);
+
-fun pretty ctxt space name = Pretty.mark_str (markup_extern ctxt space name);
+(* completion *)
+
+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 =
+ 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
+ else Completion.none;
(* modify internals *)
@@ -421,7 +446,9 @@
let val name = intern space xname in
(case Symtab.lookup tab name of
SOME x => (Context_Position.report_generic context pos (markup space name); (name, x))
- | NONE => error (undefined (kind_of space) name ^ Position.here pos))
+ | NONE =>
+ (Completion.report pos (completion context space (xname, pos));
+ error (undefined (kind_of space) name ^ Position.here pos)))
end;
fun get (space, tab) name =
--- a/src/Pure/PIDE/markup.ML Sat Feb 22 18:07:31 2014 +0100
+++ b/src/Pure/PIDE/markup.ML Sat Feb 22 20:52:43 2014 +0100
@@ -37,6 +37,7 @@
val get_entity_kind: T -> string option
val defN: string
val refN: string
+ val completionN: string val completion: T
val lineN: string
val offsetN: string
val end_offsetN: string
@@ -283,6 +284,11 @@
val refN = "ref";
+(* completion *)
+
+val (completionN, completion) = markup_elem "completion";
+
+
(* position *)
val lineN = "line";
@@ -546,6 +552,7 @@
fun simp_trace_cancel i = [(functionN, "simp_trace_cancel"), (serialN, print_int i)];
+
(** print mode operations **)
val no_output = ("", "");
--- a/src/Pure/PIDE/markup.scala Sat Feb 22 18:07:31 2014 +0100
+++ b/src/Pure/PIDE/markup.scala Sat Feb 22 20:52:43 2014 +0100
@@ -67,6 +67,11 @@
}
+ /* completion */
+
+ val COMPLETION = "completion"
+
+
/* position */
val LINE = "line"
--- a/src/Pure/ROOT Sat Feb 22 18:07:31 2014 +0100
+++ b/src/Pure/ROOT Sat Feb 22 20:52:43 2014 +0100
@@ -71,6 +71,7 @@
"General/basics.ML"
"General/binding.ML"
"General/buffer.ML"
+ "General/completion.ML"
"General/file.ML"
"General/graph.ML"
"General/graph_display.ML"
--- a/src/Pure/ROOT.ML Sat Feb 22 18:07:31 2014 +0100
+++ b/src/Pure/ROOT.ML Sat Feb 22 20:52:43 2014 +0100
@@ -146,6 +146,7 @@
use "term_ord.ML";
use "term_subst.ML";
use "term_xml.ML";
+use "General/completion.ML";
use "General/name_space.ML";
use "sorts.ML";
use "type.ML";
--- a/src/Pure/Tools/find_theorems.ML Sat Feb 22 18:07:31 2014 +0100
+++ b/src/Pure/Tools/find_theorems.ML Sat Feb 22 20:52:43 2014 +0100
@@ -355,16 +355,10 @@
fun nicer_shortest ctxt =
let
val space = Facts.space_of (Proof_Context.facts_of ctxt);
-
- val shorten =
- Name_Space.extern
- (ctxt
- |> Config.put Name_Space.names_long false
- |> Config.put Name_Space.names_short false
- |> Config.put Name_Space.names_unique false) space;
+ val extern_shortest = Name_Space.extern_shortest ctxt space;
fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
- nicer_name (shorten x, i) (shorten y, j)
+ nicer_name (extern_shortest x, i) (extern_shortest y, j)
| nicer (Facts.Fact _) (Facts.Named _) = true
| nicer (Facts.Named _) (Facts.Fact _) = false
| nicer (Facts.Fact _) (Facts.Fact _) = true;
--- a/src/Pure/context_position.ML Sat Feb 22 18:07:31 2014 +0100
+++ b/src/Pure/context_position.ML Sat Feb 22 20:52:43 2014 +0100
@@ -6,6 +6,7 @@
signature CONTEXT_POSITION =
sig
+ val is_visible_generic: Context.generic -> bool
val is_visible: Proof.context -> bool
val is_visible_global: theory -> bool
val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit