src/Pure/General/completion.ML
author wenzelm
Tue, 27 Nov 2018 16:20:08 +0100
changeset 69347 54b95d2ec040
parent 69289 bf6937af7fe8
child 71911 d25093536482
permissions -rw-r--r--
more robust: avoid broken YXML due to Markup.empty;
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
69289
bf6937af7fe8 clarified signature;
wenzelm
parents: 67208
diff changeset
     9
  type name = string * (string * string)
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    10
  type T
69289
bf6937af7fe8 clarified signature;
wenzelm
parents: 67208
diff changeset
    11
  val names: Position.T -> name list -> T
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    12
  val none: T
69289
bf6937af7fe8 clarified signature;
wenzelm
parents: 67208
diff changeset
    13
  val make: string * Position.T -> ((string -> bool) -> name list) -> T
60731
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 59812
diff changeset
    14
  val encode: T -> XML.body
69347
54b95d2ec040 more robust: avoid broken YXML due to Markup.empty;
wenzelm
parents: 69289
diff changeset
    15
  val markup_element: T -> (Markup.T * XML.body) option
69289
bf6937af7fe8 clarified signature;
wenzelm
parents: 67208
diff changeset
    16
  val markup_report: T list -> string
bf6937af7fe8 clarified signature;
wenzelm
parents: 67208
diff changeset
    17
  val make_report: string * Position.T -> ((string -> bool) -> name list) -> string
55915
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55840
diff changeset
    18
  val suppress_abbrevs: string -> Markup.T list
67208
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    19
  val check_option: Options.T -> Proof.context -> string * Position.T -> string
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    20
  val check_option_value:
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    21
    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
    22
end;
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
structure Completion: COMPLETION =
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    25
struct
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    26
59812
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59720
diff changeset
    27
(* completion of names *)
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59720
diff changeset
    28
69289
bf6937af7fe8 clarified signature;
wenzelm
parents: 67208
diff changeset
    29
type name = string * (string * string);  (*external name, kind, internal name*)
bf6937af7fe8 clarified signature;
wenzelm
parents: 67208
diff changeset
    30
bf6937af7fe8 clarified signature;
wenzelm
parents: 67208
diff changeset
    31
abstype T = Completion of {pos: Position.T, total: int, names: name list}
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    32
with
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    33
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    34
fun dest (Completion args) = args;
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    35
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55687
diff changeset
    36
fun names pos names =
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    37
  Completion
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    38
   {pos = pos,
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    39
    total = length names,
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    40
    names = take (Options.default_int "completion_limit") names};
55672
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    41
5e25cc741ab9 support for completion within the formal context;
wenzelm
parents:
diff changeset
    42
end;
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    43
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55687
diff changeset
    44
val none = names Position.none [];
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    45
59812
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59720
diff changeset
    46
fun make (name, pos) make_names =
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59720
diff changeset
    47
  if Position.is_reported pos andalso name <> "" andalso name <> "_"
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59720
diff changeset
    48
  then names pos (make_names (String.isPrefix (Name.clean name)))
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59720
diff changeset
    49
  else none;
675d0c692c41 semantic completion for @{system_option};
wenzelm
parents: 59720
diff changeset
    50
60731
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 59812
diff changeset
    51
fun encode completion =
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 59812
diff changeset
    52
  let
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 59812
diff changeset
    53
    val {total, names, ...} = dest completion;
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 59812
diff changeset
    54
    open XML.Encode;
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 59812
diff changeset
    55
  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
    56
69289
bf6937af7fe8 clarified signature;
wenzelm
parents: 67208
diff changeset
    57
fun markup_element completion =
60731
4ac4b314d93c additional ML parse tree components for Poly/ML 5.5.3, or later;
wenzelm
parents: 59812
diff changeset
    58
  let val {pos, names, ...} = dest completion in
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    59
    if Position.is_reported pos andalso not (null names) then
69347
54b95d2ec040 more robust: avoid broken YXML due to Markup.empty;
wenzelm
parents: 69289
diff changeset
    60
      SOME (Position.markup pos Markup.completion, encode completion)
54b95d2ec040 more robust: avoid broken YXML due to Markup.empty;
wenzelm
parents: 69289
diff changeset
    61
    else NONE
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    62
  end;
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
    63
69289
bf6937af7fe8 clarified signature;
wenzelm
parents: 67208
diff changeset
    64
val markup_report =
69347
54b95d2ec040 more robust: avoid broken YXML due to Markup.empty;
wenzelm
parents: 69289
diff changeset
    65
  map_filter markup_element #> map XML.Elem #> YXML.string_of_body #> Markup.markup_report;
69289
bf6937af7fe8 clarified signature;
wenzelm
parents: 67208
diff changeset
    66
bf6937af7fe8 clarified signature;
wenzelm
parents: 67208
diff changeset
    67
val make_report = markup_report oo (single oo make);
bf6937af7fe8 clarified signature;
wenzelm
parents: 67208
diff changeset
    68
55915
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55840
diff changeset
    69
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55840
diff changeset
    70
(* suppress short abbreviations *)
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55840
diff changeset
    71
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55840
diff changeset
    72
fun suppress_abbrevs s =
55917
5438ed05e1c9 special treatment of method combinators like Args.$$$ keywords, although parsed via Parse.$$$;
wenzelm
parents: 55915
diff changeset
    73
  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
    74
  then [Markup.no_completion]
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55840
diff changeset
    75
  else [];
607948c90bf0 suppress short abbreviations more uniformly, for outer and quasi-outer syntax;
wenzelm
parents: 55840
diff changeset
    76
67208
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    77
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    78
(* system options *)
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    79
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    80
fun check_option options ctxt (name, pos) =
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    81
  let
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    82
    val markup =
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    83
      Options.markup options (name, pos) handle ERROR msg =>
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    84
        let
69289
bf6937af7fe8 clarified signature;
wenzelm
parents: 67208
diff changeset
    85
          val completion_report =
bf6937af7fe8 clarified signature;
wenzelm
parents: 67208
diff changeset
    86
            make_report (name, pos) (fn completed =>
67208
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    87
                Options.names options
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    88
                |> filter completed
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    89
                |> map (fn a => (a, ("system_option", a))));
69289
bf6937af7fe8 clarified signature;
wenzelm
parents: 67208
diff changeset
    90
        in error (msg ^ completion_report) end;
67208
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    91
    val _ = Context_Position.report ctxt pos markup;
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    92
  in name end;
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    93
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    94
fun check_option_value ctxt (name, pos) (value, pos') options =
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    95
  let
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    96
    val _ = check_option options ctxt (name, pos);
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    97
    val options' =
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    98
      Options.update name value options
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
    99
        handle ERROR msg => error (msg ^ Position.here pos');
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
   100
  in (name, options') end;
16519cd83ed4 clarified signature;
wenzelm
parents: 60731
diff changeset
   101
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
   102
end;