support for completion within the formal context;
authorwenzelm
Sat Feb 22 20:52:43 2014 +0100 (2014-02-22)
changeset 556725e25cc741ab9
parent 55671 aeca05e62fef
child 55673 0286219c1261
support for completion within the formal context;
tuned signature;
etc/options
src/Pure/General/completion.ML
src/Pure/General/name_space.ML
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/Tools/find_theorems.ML
src/Pure/context_position.ML
     1.1 --- a/etc/options	Sat Feb 22 18:07:31 2014 +0100
     1.2 +++ b/etc/options	Sat Feb 22 20:52:43 2014 +0100
     1.3 @@ -136,3 +136,9 @@
     1.4  public option find_theorems_tac_limit : int = 5
     1.5    -- "limit of tactic search for 'solves' criterion"
     1.6  
     1.7 +
     1.8 +section "Completion"
     1.9 +
    1.10 +public option completion_limit : int = 40
    1.11 +  -- "limit for completion within the formal context"
    1.12 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/General/completion.ML	Sat Feb 22 20:52:43 2014 +0100
     2.3 @@ -0,0 +1,37 @@
     2.4 +(*  Title:      Pure/Isar/completion.ML
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Completion within the formal context.
     2.8 +*)
     2.9 +
    2.10 +signature COMPLETION =
    2.11 +sig
    2.12 +  val limit: unit -> int
    2.13 +  type T = {original: string, replacements: string list}
    2.14 +  val none: T
    2.15 +  val reported_text: Position.T -> T -> string
    2.16 +  val report: Position.T -> T -> unit
    2.17 +end;
    2.18 +
    2.19 +structure Completion: COMPLETION =
    2.20 +struct
    2.21 +
    2.22 +fun limit () = Options.default_int "completion_limit";
    2.23 +
    2.24 +
    2.25 +type T = {original: string, replacements: string list};
    2.26 +
    2.27 +val none: T = {original = "", replacements = []};
    2.28 +
    2.29 +fun encode ({original, replacements}: T) =
    2.30 +  (original, replacements)
    2.31 +  |> let open XML.Encode in pair string (list string) end;
    2.32 +
    2.33 +fun reported_text pos (completion: T) =
    2.34 +  if null (#replacements completion) then ""
    2.35 +  else Position.reported_text pos Markup.completion (YXML.string_of_body (encode completion));
    2.36 +
    2.37 +fun report pos completion =
    2.38 +  Output.report (reported_text pos completion);
    2.39 +
    2.40 +end;
     3.1 --- a/src/Pure/General/name_space.ML	Sat Feb 22 18:07:31 2014 +0100
     3.2 +++ b/src/Pure/General/name_space.ML	Sat Feb 22 20:52:43 2014 +0100
     3.3 @@ -27,8 +27,10 @@
     3.4    val names_unique: bool Config.T
     3.5    val extern: Proof.context -> T -> string -> xstring
     3.6    val extern_ord: Proof.context -> T -> string * string -> order
     3.7 +  val extern_shortest: Proof.context -> T -> string -> xstring
     3.8    val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
     3.9    val pretty: Proof.context -> T -> string -> Pretty.T
    3.10 +  val completion: Context.generic -> T -> xstring * Position.T -> Completion.T
    3.11    val hide: bool -> string -> T -> T
    3.12    val merge: T * T -> T
    3.13    type naming
    3.14 @@ -151,11 +153,13 @@
    3.15      if not (null names) andalso hd names = name then cons xname else I) internals [];
    3.16  
    3.17  
    3.18 -(* intern and extern *)
    3.19 +(* intern *)
    3.20  
    3.21  fun intern space xname = #1 (lookup space xname);
    3.22  
    3.23  
    3.24 +(* extern *)
    3.25 +
    3.26  val names_long_raw = Config.declare_option "names_long";
    3.27  val names_long = Config.bool names_long_raw;
    3.28  
    3.29 @@ -185,9 +189,30 @@
    3.30  
    3.31  fun extern_ord ctxt space = string_ord o pairself (extern ctxt space);
    3.32  
    3.33 +fun extern_shortest ctxt =
    3.34 +  extern
    3.35 +    (ctxt
    3.36 +      |> Config.put names_long false
    3.37 +      |> Config.put names_short false
    3.38 +      |> Config.put names_unique false);
    3.39 +
    3.40  fun markup_extern ctxt space name = (markup space name, extern ctxt space name);
    3.41 +fun pretty ctxt space name = Pretty.mark_str (markup_extern ctxt space name);
    3.42 +
    3.43  
    3.44 -fun pretty ctxt space name = Pretty.mark_str (markup_extern ctxt space name);
    3.45 +(* completion *)
    3.46 +
    3.47 +fun completion context (space as Name_Space {internals, ...}) (xname, pos) =
    3.48 +  if Context_Position.is_visible_generic context andalso Position.is_reported pos then
    3.49 +    let
    3.50 +      val replacements =
    3.51 +        Symtab.fold (fn (a, (b :: _, _)) => String.isPrefix xname a ? cons b | _ => I)
    3.52 +          internals []
    3.53 +        |> take (Completion.limit ())
    3.54 +        |> map (extern_shortest (Context.proof_of context) space)
    3.55 +        |> sort_distinct string_ord;
    3.56 +    in {original = xname, replacements = replacements} end
    3.57 +  else Completion.none;
    3.58  
    3.59  
    3.60  (* modify internals *)
    3.61 @@ -421,7 +446,9 @@
    3.62    let val name = intern space xname in
    3.63      (case Symtab.lookup tab name of
    3.64        SOME x => (Context_Position.report_generic context pos (markup space name); (name, x))
    3.65 -    | NONE => error (undefined (kind_of space) name ^ Position.here pos))
    3.66 +    | NONE =>
    3.67 +       (Completion.report pos (completion context space (xname, pos));
    3.68 +        error (undefined (kind_of space) name ^ Position.here pos)))
    3.69    end;
    3.70  
    3.71  fun get (space, tab) name =
     4.1 --- a/src/Pure/PIDE/markup.ML	Sat Feb 22 18:07:31 2014 +0100
     4.2 +++ b/src/Pure/PIDE/markup.ML	Sat Feb 22 20:52:43 2014 +0100
     4.3 @@ -37,6 +37,7 @@
     4.4    val get_entity_kind: T -> string option
     4.5    val defN: string
     4.6    val refN: string
     4.7 +  val completionN: string val completion: T
     4.8    val lineN: string
     4.9    val offsetN: string
    4.10    val end_offsetN: string
    4.11 @@ -283,6 +284,11 @@
    4.12  val refN = "ref";
    4.13  
    4.14  
    4.15 +(* completion *)
    4.16 +
    4.17 +val (completionN, completion) = markup_elem "completion";
    4.18 +
    4.19 +
    4.20  (* position *)
    4.21  
    4.22  val lineN = "line";
    4.23 @@ -546,6 +552,7 @@
    4.24  fun simp_trace_cancel i = [(functionN, "simp_trace_cancel"), (serialN, print_int i)];
    4.25  
    4.26  
    4.27 +
    4.28  (** print mode operations **)
    4.29  
    4.30  val no_output = ("", "");
     5.1 --- a/src/Pure/PIDE/markup.scala	Sat Feb 22 18:07:31 2014 +0100
     5.2 +++ b/src/Pure/PIDE/markup.scala	Sat Feb 22 20:52:43 2014 +0100
     5.3 @@ -67,6 +67,11 @@
     5.4    }
     5.5  
     5.6  
     5.7 +  /* completion */
     5.8 +
     5.9 +  val COMPLETION = "completion"
    5.10 +
    5.11 +
    5.12    /* position */
    5.13  
    5.14    val LINE = "line"
     6.1 --- a/src/Pure/ROOT	Sat Feb 22 18:07:31 2014 +0100
     6.2 +++ b/src/Pure/ROOT	Sat Feb 22 20:52:43 2014 +0100
     6.3 @@ -71,6 +71,7 @@
     6.4      "General/basics.ML"
     6.5      "General/binding.ML"
     6.6      "General/buffer.ML"
     6.7 +    "General/completion.ML"
     6.8      "General/file.ML"
     6.9      "General/graph.ML"
    6.10      "General/graph_display.ML"
     7.1 --- a/src/Pure/ROOT.ML	Sat Feb 22 18:07:31 2014 +0100
     7.2 +++ b/src/Pure/ROOT.ML	Sat Feb 22 20:52:43 2014 +0100
     7.3 @@ -146,6 +146,7 @@
     7.4  use "term_ord.ML";
     7.5  use "term_subst.ML";
     7.6  use "term_xml.ML";
     7.7 +use "General/completion.ML";
     7.8  use "General/name_space.ML";
     7.9  use "sorts.ML";
    7.10  use "type.ML";
     8.1 --- a/src/Pure/Tools/find_theorems.ML	Sat Feb 22 18:07:31 2014 +0100
     8.2 +++ b/src/Pure/Tools/find_theorems.ML	Sat Feb 22 20:52:43 2014 +0100
     8.3 @@ -355,16 +355,10 @@
     8.4  fun nicer_shortest ctxt =
     8.5    let
     8.6      val space = Facts.space_of (Proof_Context.facts_of ctxt);
     8.7 -
     8.8 -    val shorten =
     8.9 -      Name_Space.extern
    8.10 -        (ctxt
    8.11 -          |> Config.put Name_Space.names_long false
    8.12 -          |> Config.put Name_Space.names_short false
    8.13 -          |> Config.put Name_Space.names_unique false) space;
    8.14 +    val extern_shortest = Name_Space.extern_shortest ctxt space;
    8.15  
    8.16      fun nicer (Facts.Named ((x, _), i)) (Facts.Named ((y, _), j)) =
    8.17 -          nicer_name (shorten x, i) (shorten y, j)
    8.18 +          nicer_name (extern_shortest x, i) (extern_shortest y, j)
    8.19        | nicer (Facts.Fact _) (Facts.Named _) = true
    8.20        | nicer (Facts.Named _) (Facts.Fact _) = false
    8.21        | nicer (Facts.Fact _) (Facts.Fact _) = true;
     9.1 --- a/src/Pure/context_position.ML	Sat Feb 22 18:07:31 2014 +0100
     9.2 +++ b/src/Pure/context_position.ML	Sat Feb 22 20:52:43 2014 +0100
     9.3 @@ -6,6 +6,7 @@
     9.4  
     9.5  signature CONTEXT_POSITION =
     9.6  sig
     9.7 +  val is_visible_generic: Context.generic -> bool
     9.8    val is_visible: Proof.context -> bool
     9.9    val is_visible_global: theory -> bool
    9.10    val if_visible: Proof.context -> ('a -> unit) -> 'a -> unit