# HG changeset patch
# User wenzelm
# Date 1393098763 -3600
# Node ID 5e25cc741ab967b46ba7a15ffa2b5ef1b7790b3f
# Parent  aeca05e62fef3f0adcae33d67cd636692f339868
support for completion within the formal context;
tuned signature;

diff -r aeca05e62fef -r 5e25cc741ab9 etc/options
--- 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"
+
diff -r aeca05e62fef -r 5e25cc741ab9 src/Pure/General/completion.ML
--- /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;
diff -r aeca05e62fef -r 5e25cc741ab9 src/Pure/General/name_space.ML
--- 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 =
diff -r aeca05e62fef -r 5e25cc741ab9 src/Pure/PIDE/markup.ML
--- 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 = ("", "");
diff -r aeca05e62fef -r 5e25cc741ab9 src/Pure/PIDE/markup.scala
--- 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"
diff -r aeca05e62fef -r 5e25cc741ab9 src/Pure/ROOT
--- 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"
diff -r aeca05e62fef -r 5e25cc741ab9 src/Pure/ROOT.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";
diff -r aeca05e62fef -r 5e25cc741ab9 src/Pure/Tools/find_theorems.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;
diff -r aeca05e62fef -r 5e25cc741ab9 src/Pure/context_position.ML
--- 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