src/Pure/General/completion.ML
author wenzelm
Sat, 16 Dec 2017 12:16:40 +0100
changeset 67208 16519cd83ed4
parent 60731 4ac4b314d93c
child 69289 bf6937af7fe8
permissions -rw-r--r--
clarified signature;
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
67208
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    16
  val check_option: Options.T -> Proof.context -> string * Position.T -> string
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    17
  val check_option_value:
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    18
    Proof.context -> string * Position.T -> string * Position.T -> Options.T -> string * Options.T
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    19
end;
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
structure Completion: COMPLETION =
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    22
struct
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    23
59812
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59720
diff changeset
    24
(* completion of names *)
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59720
diff changeset
    25
55977
ec4830499634 more detailed description of completion items;
wenzelm
parents: 55917
diff changeset
    26
abstype T =
ec4830499634 more detailed description of completion items;
wenzelm
parents: 55917
diff changeset
    27
  Completion of {pos: Position.T, total: int, names: (string * (string * string)) list}
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    28
with
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    29
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    30
fun dest (Completion args) = args;
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    31
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55687
diff changeset
    32
fun names pos names =
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    33
  Completion
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    34
   {pos = pos,
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    35
    total = length names,
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    36
    names = take (Options.default_int "completion_limit") names};
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    37
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    38
end;
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    39
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55687
diff changeset
    40
val none = names Position.none [];
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    41
59812
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59720
diff changeset
    42
fun make (name, pos) make_names =
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59720
diff changeset
    43
  if Position.is_reported pos andalso name <> "" andalso name <> "_"
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59720
diff changeset
    44
  then names pos (make_names (String.isPrefix (Name.clean name)))
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59720
diff changeset
    45
  else none;
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59720
diff changeset
    46
60731
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 59812
diff changeset
    47
fun encode completion =
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 59812
diff changeset
    48
  let
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 59812
diff changeset
    49
    val {total, names, ...} = dest completion;
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 59812
diff changeset
    50
    open XML.Encode;
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 59812
diff changeset
    51
  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
    52
55840
2982d233d798 consider completion report as part of error message -- less stateful, may get handled;
wenzelm
parents: 55694
diff changeset
    53
fun reported_text completion =
60731
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 59812
diff changeset
    54
  let val {pos, names, ...} = dest completion in
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    55
    if Position.is_reported pos andalso not (null names) then
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    56
      let
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55687
diff changeset
    57
        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
    58
      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
    59
    else ""
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    60
  end;
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    61
55915
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55840
diff changeset
    62
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55840
diff changeset
    63
(* suppress short abbreviations *)
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55840
diff changeset
    64
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55840
diff changeset
    65
fun suppress_abbrevs s =
55917
5438ed05e1c9 special treatment of method combinators like Args.$$$ keywords, although parsed via Parse.$$$;
wenzelm
parents: 55915
diff changeset
    66
  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
    67
  then [Markup.no_completion]
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55840
diff changeset
    68
  else [];
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55840
diff changeset
    69
67208
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    70
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    71
(* system options *)
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    72
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    73
fun check_option options ctxt (name, pos) =
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    74
  let
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    75
    val markup =
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    76
      Options.markup options (name, pos) handle ERROR msg =>
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    77
        let
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    78
          val completion =
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    79
            make (name, pos) (fn completed =>
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    80
                Options.names options
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    81
                |> filter completed
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    82
                |> map (fn a => (a, ("system_option", a))));
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    83
          val report = Markup.markup_report (reported_text completion);
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    84
        in error (msg ^ report) end;
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    85
    val _ = Context_Position.report ctxt pos markup;
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    86
  in name end;
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    87
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    88
fun check_option_value ctxt (name, pos) (value, pos') options =
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    89
  let
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    90
    val _ = check_option options ctxt (name, pos);
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    91
    val options' =
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    92
      Options.update name value options
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    93
        handle ERROR msg => error (msg ^ Position.here pos');
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    94
  in (name, options') end;
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    95
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    96
end;