src/Pure/General/completion.ML
author wenzelm
Thu, 16 Jul 2015 14:40:23 +0200
changeset 60731 4ac4b314d93c
parent 59812 675d0c692c41
child 67208 16519cd83ed4
permissions -rw-r--r--
additional ML parse tree components for Poly/ML 5.5.3, or later; support for ML completion; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
59720
f893472fff31 proper headers;
wenzelm
parents: 56293
diff changeset
     1
(*  Title:      Pure/General/completion.ML
55672
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
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
     9
  type T
55977
ec4830499634 more detailed description of completion items;
wenzelm
parents: 55917
diff changeset
    10
  val names: Position.T -> (string * (string * string)) list -> T
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    11
  val none: T
59812
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59720
diff changeset
    12
  val make: string * Position.T -> ((string -> bool) -> (string * (string * string)) list) -> T
60731
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 59812
diff changeset
    13
  val encode: T -> XML.body
55840
2982d233d798 consider completion report as part of error message -- less stateful, may get handled;
wenzelm
parents: 55694
diff changeset
    14
  val reported_text: T -> string
55915
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55840
diff changeset
    15
  val suppress_abbrevs: string -> Markup.T list
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    16
end;
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    17
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    18
structure Completion: COMPLETION =
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    19
struct
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    20
59812
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59720
diff changeset
    21
(* completion of names *)
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59720
diff changeset
    22
55977
ec4830499634 more detailed description of completion items;
wenzelm
parents: 55917
diff changeset
    23
abstype T =
ec4830499634 more detailed description of completion items;
wenzelm
parents: 55917
diff changeset
    24
  Completion of {pos: Position.T, total: int, names: (string * (string * string)) list}
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    25
with
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    26
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    27
fun dest (Completion args) = args;
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    28
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55687
diff changeset
    29
fun names pos names =
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    30
  Completion
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    31
   {pos = pos,
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    32
    total = length names,
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    33
    names = take (Options.default_int "completion_limit") names};
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    34
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    35
end;
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    36
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55687
diff changeset
    37
val none = names Position.none [];
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    38
59812
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59720
diff changeset
    39
fun make (name, pos) make_names =
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59720
diff changeset
    40
  if Position.is_reported pos andalso name <> "" andalso name <> "_"
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59720
diff changeset
    41
  then names pos (make_names (String.isPrefix (Name.clean name)))
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59720
diff changeset
    42
  else none;
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59720
diff changeset
    43
60731
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 59812
diff changeset
    44
fun encode completion =
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 59812
diff changeset
    45
  let
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 59812
diff changeset
    46
    val {total, names, ...} = dest completion;
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 59812
diff changeset
    47
    open XML.Encode;
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 59812
diff changeset
    48
  in pair int (list (pair string (pair string string))) (total, names) end;
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 59812
diff changeset
    49
55840
2982d233d798 consider completion report as part of error message -- less stateful, may get handled;
wenzelm
parents: 55694
diff changeset
    50
fun reported_text completion =
60731
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 59812
diff changeset
    51
  let val {pos, names, ...} = dest completion in
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    52
    if Position.is_reported pos andalso not (null names) then
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    53
      let
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55687
diff changeset
    54
        val markup = Position.markup pos Markup.completion;
60731
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 59812
diff changeset
    55
      in YXML.string_of (XML.Elem (markup, encode completion)) end
55840
2982d233d798 consider completion report as part of error message -- less stateful, may get handled;
wenzelm
parents: 55694
diff changeset
    56
    else ""
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    57
  end;
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    58
55915
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55840
diff changeset
    59
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55840
diff changeset
    60
(* suppress short abbreviations *)
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55840
diff changeset
    61
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55840
diff changeset
    62
fun suppress_abbrevs s =
55917
5438ed05e1c9 special treatment of method combinators like Args.$$$ keywords, although parsed via Parse.$$$;
wenzelm
parents: 55915
diff changeset
    63
  if not (Symbol.is_ascii_identifier s) andalso (length (Symbol.explode s) <= 1 orelse s = "::")
55915
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55840
diff changeset
    64
  then [Markup.no_completion]
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55840
diff changeset
    65
  else [];
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55840
diff changeset
    66
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    67
end;