src/Pure/General/completion.ML
author wenzelm
Sat, 22 Feb 2014 21:38:26 +0100
changeset 55674 8a213ab0e78a
parent 55672 5e25cc741ab9
child 55687 78c83cd477c1
permissions -rw-r--r--
support for semantic completion on Scala side;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Isar/completion.ML
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
     3
55674
8a213ab0e78a support for semantic completion on Scala side;
wenzelm
parents: 55672
diff changeset
     4
Semantic completion within the formal context.
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
     5
*)
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
     6
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
     7
signature COMPLETION =
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
     8
sig
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
     9
  val limit: unit -> int
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    10
  type T = {original: string, replacements: string list}
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    11
  val none: T
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    12
  val reported_text: Position.T -> T -> string
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    13
  val report: Position.T -> T -> unit
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    14
end;
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    15
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    16
structure Completion: COMPLETION =
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    17
struct
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    18
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    19
fun limit () = Options.default_int "completion_limit";
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    20
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    21
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    22
type T = {original: string, replacements: string list};
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    23
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    24
val none: T = {original = "", replacements = []};
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    25
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    26
fun encode ({original, replacements}: T) =
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    27
  (original, replacements)
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    28
  |> let open XML.Encode in pair string (list string) end;
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    29
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    30
fun reported_text pos (completion: T) =
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    31
  if null (#replacements completion) then ""
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    32
  else Position.reported_text pos Markup.completion (YXML.string_of_body (encode completion));
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    33
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    34
fun report pos completion =
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    35
  Output.report (reported_text pos completion);
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    36
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    37
end;