src/Pure/General/completion.scala
author wenzelm
Sat, 01 Apr 2017 19:17:15 +0200
changeset 65344 b99283eed13c
parent 63887 2d9c12eba726
child 66055 07175635f78c
permissions -rw-r--r--
clarified YXML vs. symbol encoding: operate on whole message;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
55673
0286219c1261 clarified module location (again, see 763d35697338);
wenzelm
parents: 55666
diff changeset
     1
/*  Title:      Pure/General/completion.scala
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
     3
55687
78c83cd477c1 clarified completion names;
wenzelm
parents: 55674
diff changeset
     4
Semantic completion within the formal context (reported names).
55674
8a213ab0e78a support for semantic completion on Scala side;
wenzelm
parents: 55673
diff changeset
     5
Syntactic completion of keywords and symbols, with abbreviations
55992
wenzelm
parents: 55986
diff changeset
     6
(based on language context).
wenzelm
parents: 55986
diff changeset
     7
*/
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
     8
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
     9
package isabelle
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    10
55618
995162143ef4 tuned imports;
wenzelm
parents: 55615
diff changeset
    11
53337
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    12
import scala.collection.immutable.SortedMap
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    13
import scala.util.parsing.combinator.RegexParsers
57589
e0e4ac981cf1 always complete explicit symbols;
wenzelm
parents: 57588
diff changeset
    14
import scala.util.matching.Regex
53337
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    15
import scala.math.Ordering
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    16
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    17
46624
dc4c72092088 streamlined abstract datatype;
wenzelm
parents: 45900
diff changeset
    18
object Completion
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    19
{
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
    20
  /** completion result **/
53275
b34aac6511ab tuned signature;
wenzelm
parents: 53251
diff changeset
    21
53296
65c60c782da5 less aggressive immediate completion, based on input and text;
wenzelm
parents: 53295
diff changeset
    22
  sealed case class Item(
55692
19e8b00684f7 more explicit Completion.Item.range, independently of caret;
wenzelm
parents: 55687
diff changeset
    23
    range: Text.Range,
53296
65c60c782da5 less aggressive immediate completion, based on input and text;
wenzelm
parents: 53295
diff changeset
    24
    original: String,
55666
cc350eb1087e refined language context: antiquotes;
wenzelm
parents: 55618
diff changeset
    25
    name: String,
55978
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55977
diff changeset
    26
    description: List[String],
53296
65c60c782da5 less aggressive immediate completion, based on input and text;
wenzelm
parents: 53295
diff changeset
    27
    replacement: String,
55666
cc350eb1087e refined language context: antiquotes;
wenzelm
parents: 55618
diff changeset
    28
    move: Int,
53296
65c60c782da5 less aggressive immediate completion, based on input and text;
wenzelm
parents: 53295
diff changeset
    29
    immediate: Boolean)
53275
b34aac6511ab tuned signature;
wenzelm
parents: 53251
diff changeset
    30
55914
c5b752d549e3 clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents: 55813
diff changeset
    31
  object Result
c5b752d549e3 clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents: 55813
diff changeset
    32
  {
c5b752d549e3 clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents: 55813
diff changeset
    33
    def empty(range: Text.Range): Result = Result(range, "", false, Nil)
56175
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56174
diff changeset
    34
    def merge(history: History, result1: Option[Result], result2: Option[Result]): Option[Result] =
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56174
diff changeset
    35
      (result1, result2) match {
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56174
diff changeset
    36
        case (_, None) => result1
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56174
diff changeset
    37
        case (None, _) => result2
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56174
diff changeset
    38
        case (Some(res1), Some(res2)) =>
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56174
diff changeset
    39
          if (res1.range != res2.range || res1.original != res2.original) result1
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56174
diff changeset
    40
          else {
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56174
diff changeset
    41
            val items = (res1.items ::: res2.items).sorted(history.ordering)
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56174
diff changeset
    42
            Some(Result(res1.range, res1.original, false, items))
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56174
diff changeset
    43
          }
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56174
diff changeset
    44
      }
55914
c5b752d549e3 clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents: 55813
diff changeset
    45
  }
c5b752d549e3 clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents: 55813
diff changeset
    46
55693
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
    47
  sealed case class Result(
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
    48
    range: Text.Range,
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
    49
    original: String,
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
    50
    unique: Boolean,
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
    51
    items: List[Item])
53325
ffabc0083786 more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
wenzelm
parents: 53324
diff changeset
    52
53275
b34aac6511ab tuned signature;
wenzelm
parents: 53251
diff changeset
    53
46624
dc4c72092088 streamlined abstract datatype;
wenzelm
parents: 45900
diff changeset
    54
53337
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    55
  /** persistent history **/
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    56
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    57
  private val COMPLETION_HISTORY = Path.explode("$ISABELLE_HOME_USER/etc/completion_history")
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    58
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    59
  object History
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    60
  {
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    61
    val empty: History = new History()
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    62
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    63
    def load(): History =
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    64
    {
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    65
      def ignore_error(msg: String): Unit =
56782
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup);
wenzelm
parents: 56661
diff changeset
    66
        Output.warning("Ignoring bad content of file " + COMPLETION_HISTORY +
53337
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    67
          (if (msg == "") "" else "\n" + msg))
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    68
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    69
      val content =
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    70
        if (COMPLETION_HISTORY.is_file) {
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    71
          try {
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    72
            import XML.Decode._
65344
b99283eed13c clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents: 63887
diff changeset
    73
            list(pair(string, int))(Symbol.decode_yxml(File.read(COMPLETION_HISTORY)))
53337
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    74
          }
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    75
          catch {
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    76
            case ERROR(msg) => ignore_error(msg); Nil
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    77
            case _: XML.Error => ignore_error(""); Nil
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    78
          }
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    79
        }
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    80
        else Nil
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    81
      (empty /: content)(_ + _)
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    82
    }
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    83
  }
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    84
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    85
  final class History private(rep: SortedMap[String, Int] = SortedMap.empty)
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    86
  {
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    87
    override def toString: String = rep.mkString("Completion.History(", ",", ")")
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    88
56878
a5d082a85124 hardwired default_frequency to avoid fluctuation of popup content;
wenzelm
parents: 56800
diff changeset
    89
    def frequency(name: String): Int =
a5d082a85124 hardwired default_frequency to avoid fluctuation of popup content;
wenzelm
parents: 56800
diff changeset
    90
      default_frequency(Symbol.encode(name)) getOrElse
a5d082a85124 hardwired default_frequency to avoid fluctuation of popup content;
wenzelm
parents: 56800
diff changeset
    91
      rep.getOrElse(name, 0)
53337
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    92
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    93
    def + (entry: (String, Int)): History =
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    94
    {
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    95
      val (name, freq) = entry
56564
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name;
wenzelm
parents: 56278
diff changeset
    96
      if (name == "") this
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name;
wenzelm
parents: 56278
diff changeset
    97
      else new History(rep + (name -> (frequency(name) + freq)))
53337
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    98
    }
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
    99
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   100
    def ordering: Ordering[Item] =
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   101
      new Ordering[Item] {
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   102
        def compare(item1: Item, item2: Item): Int =
56162
ea6303e2261b clarified completion ordering: prefer local names;
wenzelm
parents: 56042
diff changeset
   103
          frequency(item2.name) compare frequency(item1.name)
ea6303e2261b clarified completion ordering: prefer local names;
wenzelm
parents: 56042
diff changeset
   104
      }
ea6303e2261b clarified completion ordering: prefer local names;
wenzelm
parents: 56042
diff changeset
   105
53337
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   106
    def save()
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   107
    {
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   108
      Isabelle_System.mkdirs(COMPLETION_HISTORY.dir)
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   109
      File.write_backup(COMPLETION_HISTORY,
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   110
        {
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   111
          import XML.Encode._
65344
b99283eed13c clarified YXML vs. symbol encoding: operate on whole message;
wenzelm
parents: 63887
diff changeset
   112
          Symbol.encode_yxml(list(pair(string, int))(rep.toList))
53337
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   113
        })
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   114
    }
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   115
  }
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   116
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   117
  class History_Variable
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   118
  {
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   119
    private var history = History.empty
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   120
    def value: History = synchronized { history }
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   121
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   122
    def load()
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   123
    {
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   124
      val h = History.load()
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   125
      synchronized { history = h }
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   126
    }
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   127
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   128
    def update(item: Item, freq: Int = 1): Unit = synchronized {
55666
cc350eb1087e refined language context: antiquotes;
wenzelm
parents: 55618
diff changeset
   129
      history = history + (item.name -> freq)
53337
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   130
    }
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   131
  }
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   132
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   133
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   134
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   135
  /** semantic completion **/
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   136
61100
4d9efd5004c8 clean name as in ML Completion.make;
wenzelm
parents: 60732
diff changeset
   137
  def clean_name(s: String): Option[String] =
4d9efd5004c8 clean name as in ML Completion.make;
wenzelm
parents: 60732
diff changeset
   138
    if (s == "" || s == "_") None
4d9efd5004c8 clean name as in ML Completion.make;
wenzelm
parents: 60732
diff changeset
   139
    else Some(s.reverseIterator.dropWhile(_ == '_').toList.reverse.mkString)
4d9efd5004c8 clean name as in ML Completion.make;
wenzelm
parents: 60732
diff changeset
   140
59717
44a3ed0b8265 support for completion reports produced in Scala (inlined into messages);
wenzelm
parents: 59319
diff changeset
   141
  def report_no_completion(pos: Position.T): String =
44a3ed0b8265 support for completion reports produced in Scala (inlined into messages);
wenzelm
parents: 59319
diff changeset
   142
    YXML.string_of_tree(Semantic.Info(pos, No_Completion))
44a3ed0b8265 support for completion reports produced in Scala (inlined into messages);
wenzelm
parents: 59319
diff changeset
   143
44a3ed0b8265 support for completion reports produced in Scala (inlined into messages);
wenzelm
parents: 59319
diff changeset
   144
  def report_names(pos: Position.T, total: Int, names: List[(String, (String, String))]): String =
44a3ed0b8265 support for completion reports produced in Scala (inlined into messages);
wenzelm
parents: 59319
diff changeset
   145
    YXML.string_of_tree(Semantic.Info(pos, Names(total, names)))
44a3ed0b8265 support for completion reports produced in Scala (inlined into messages);
wenzelm
parents: 59319
diff changeset
   146
56173
62f10624339a tuned signature;
wenzelm
parents: 56162
diff changeset
   147
  object Semantic
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   148
  {
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   149
    object Info
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   150
    {
59717
44a3ed0b8265 support for completion reports produced in Scala (inlined into messages);
wenzelm
parents: 59319
diff changeset
   151
      def apply(pos: Position.T, semantic: Semantic): XML.Elem =
44a3ed0b8265 support for completion reports produced in Scala (inlined into messages);
wenzelm
parents: 59319
diff changeset
   152
      {
44a3ed0b8265 support for completion reports produced in Scala (inlined into messages);
wenzelm
parents: 59319
diff changeset
   153
        val elem =
44a3ed0b8265 support for completion reports produced in Scala (inlined into messages);
wenzelm
parents: 59319
diff changeset
   154
          semantic match {
44a3ed0b8265 support for completion reports produced in Scala (inlined into messages);
wenzelm
parents: 59319
diff changeset
   155
            case No_Completion => XML.Elem(Markup(Markup.NO_COMPLETION, pos), Nil)
44a3ed0b8265 support for completion reports produced in Scala (inlined into messages);
wenzelm
parents: 59319
diff changeset
   156
            case Names(total, names) =>
44a3ed0b8265 support for completion reports produced in Scala (inlined into messages);
wenzelm
parents: 59319
diff changeset
   157
              XML.Elem(Markup(Markup.COMPLETION, pos),
44a3ed0b8265 support for completion reports produced in Scala (inlined into messages);
wenzelm
parents: 59319
diff changeset
   158
                {
44a3ed0b8265 support for completion reports produced in Scala (inlined into messages);
wenzelm
parents: 59319
diff changeset
   159
                  import XML.Encode._
44a3ed0b8265 support for completion reports produced in Scala (inlined into messages);
wenzelm
parents: 59319
diff changeset
   160
                  pair(int, list(pair(string, pair(string, string))))(total, names)
44a3ed0b8265 support for completion reports produced in Scala (inlined into messages);
wenzelm
parents: 59319
diff changeset
   161
                })
44a3ed0b8265 support for completion reports produced in Scala (inlined into messages);
wenzelm
parents: 59319
diff changeset
   162
          }
44a3ed0b8265 support for completion reports produced in Scala (inlined into messages);
wenzelm
parents: 59319
diff changeset
   163
        XML.Elem(Markup(Markup.REPORT, pos), List(elem))
44a3ed0b8265 support for completion reports produced in Scala (inlined into messages);
wenzelm
parents: 59319
diff changeset
   164
      }
44a3ed0b8265 support for completion reports produced in Scala (inlined into messages);
wenzelm
parents: 59319
diff changeset
   165
56173
62f10624339a tuned signature;
wenzelm
parents: 56162
diff changeset
   166
      def unapply(info: Text.Markup): Option[Text.Info[Semantic]] =
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   167
        info.info match {
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   168
          case XML.Elem(Markup(Markup.COMPLETION, _), body) =>
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   169
            try {
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   170
              val (total, names) =
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   171
              {
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   172
                import XML.Decode._
55977
ec4830499634 more detailed description of completion items;
wenzelm
parents: 55914
diff changeset
   173
                pair(int, list(pair(string, pair(string, string))))(body)
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   174
              }
56173
62f10624339a tuned signature;
wenzelm
parents: 56162
diff changeset
   175
              Some(Text.Info(info.range, Names(total, names)))
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   176
            }
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   177
            catch { case _: XML.Error => None }
55914
c5b752d549e3 clarified init_assignable: make double-sure that initial values are reset;
wenzelm
parents: 55813
diff changeset
   178
          case XML.Elem(Markup(Markup.NO_COMPLETION, _), _) =>
56173
62f10624339a tuned signature;
wenzelm
parents: 56162
diff changeset
   179
            Some(Text.Info(info.range, No_Completion))
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   180
          case _ => None
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   181
        }
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   182
    }
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   183
  }
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   184
56173
62f10624339a tuned signature;
wenzelm
parents: 56162
diff changeset
   185
  sealed abstract class Semantic
56175
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56174
diff changeset
   186
  case object No_Completion extends Semantic
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56174
diff changeset
   187
  case class Names(total: Int, names: List[(String, (String, String))]) extends Semantic
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   188
  {
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   189
    def complete(
56173
62f10624339a tuned signature;
wenzelm
parents: 56162
diff changeset
   190
      range: Text.Range,
62f10624339a tuned signature;
wenzelm
parents: 56162
diff changeset
   191
      history: Completion.History,
62f10624339a tuned signature;
wenzelm
parents: 56162
diff changeset
   192
      do_decode: Boolean,
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   193
      original: String): Option[Completion.Result] =
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   194
    {
55977
ec4830499634 more detailed description of completion items;
wenzelm
parents: 55914
diff changeset
   195
      def decode(s: String): String = if (do_decode) Symbol.decode(s) else s
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   196
      val items =
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   197
        for {
55977
ec4830499634 more detailed description of completion items;
wenzelm
parents: 55914
diff changeset
   198
          (xname, (kind, name)) <- names
ec4830499634 more detailed description of completion items;
wenzelm
parents: 55914
diff changeset
   199
          xname1 = decode(xname)
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   200
          if xname1 != original
55977
ec4830499634 more detailed description of completion items;
wenzelm
parents: 55914
diff changeset
   201
          (full_name, descr_name) =
ec4830499634 more detailed description of completion items;
wenzelm
parents: 55914
diff changeset
   202
            if (kind == "") (name, quote(decode(name)))
56600
628e039cc34d more specific support for sequence of words;
wenzelm
parents: 56599
diff changeset
   203
            else
56800
b904ea8edd73 support for long names in Scala;
wenzelm
parents: 56782
diff changeset
   204
             (Long_Name.qualify(kind, name),
60732
18299765542e clarified boundary cases of completion;
wenzelm
parents: 60215
diff changeset
   205
              Word.implode(Word.explode('_', kind)) +
18299765542e clarified boundary cases of completion;
wenzelm
parents: 60215
diff changeset
   206
              (if (xname == name) "" else " " + quote(decode(name))))
61622
8bb7848b3d47 smart quoting of non-identifiers, e.g. jEdit actions;
wenzelm
parents: 61613
diff changeset
   207
        } yield {
8bb7848b3d47 smart quoting of non-identifiers, e.g. jEdit actions;
wenzelm
parents: 61613
diff changeset
   208
          val description = List(xname1, "(" + descr_name + ")")
8bb7848b3d47 smart quoting of non-identifiers, e.g. jEdit actions;
wenzelm
parents: 61613
diff changeset
   209
          val replacement =
63761
2ca536d0163e more careful quoting, e.g. relevant for \<^control>cartouche;
wenzelm
parents: 63587
diff changeset
   210
            List(original, xname1).map(Token.explode(Keyword.Keywords.empty, _)) match {
2ca536d0163e more careful quoting, e.g. relevant for \<^control>cartouche;
wenzelm
parents: 63587
diff changeset
   211
              case List(List(tok), _) if tok.kind == Token.Kind.CARTOUCHE =>
2ca536d0163e more careful quoting, e.g. relevant for \<^control>cartouche;
wenzelm
parents: 63587
diff changeset
   212
                Symbol.open_decoded + xname1 + Symbol.close_decoded
2ca536d0163e more careful quoting, e.g. relevant for \<^control>cartouche;
wenzelm
parents: 63587
diff changeset
   213
              case List(_, List(tok)) if tok.is_name => xname1
61622
8bb7848b3d47 smart quoting of non-identifiers, e.g. jEdit actions;
wenzelm
parents: 61613
diff changeset
   214
              case _ => quote(xname1)
8bb7848b3d47 smart quoting of non-identifiers, e.g. jEdit actions;
wenzelm
parents: 61613
diff changeset
   215
            }
8bb7848b3d47 smart quoting of non-identifiers, e.g. jEdit actions;
wenzelm
parents: 61613
diff changeset
   216
          Item(range, original, full_name, description, replacement, 0, true)
8bb7848b3d47 smart quoting of non-identifiers, e.g. jEdit actions;
wenzelm
parents: 61613
diff changeset
   217
        }
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   218
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   219
      if (items.isEmpty) None
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   220
      else Some(Result(range, original, names.length == 1, items.sorted(history.ordering)))
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   221
    }
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   222
  }
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   223
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   224
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   225
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   226
  /** syntactic completion **/
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   227
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   228
  /* language context */
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   229
55749
75a48dc4383e tuned signature;
wenzelm
parents: 55748
diff changeset
   230
  object Language_Context
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   231
  {
55749
75a48dc4383e tuned signature;
wenzelm
parents: 55748
diff changeset
   232
    val outer = Language_Context("", true, false)
75a48dc4383e tuned signature;
wenzelm
parents: 55748
diff changeset
   233
    val inner = Language_Context(Markup.Language.UNKNOWN, true, false)
75a48dc4383e tuned signature;
wenzelm
parents: 55748
diff changeset
   234
    val ML_outer = Language_Context(Markup.Language.ML, false, true)
75a48dc4383e tuned signature;
wenzelm
parents: 55748
diff changeset
   235
    val ML_inner = Language_Context(Markup.Language.ML, true, false)
56278
2576d3a40ed6 separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents: 56221
diff changeset
   236
    val SML_outer = Language_Context(Markup.Language.SML, false, false)
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   237
  }
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   238
55749
75a48dc4383e tuned signature;
wenzelm
parents: 55748
diff changeset
   239
  sealed case class Language_Context(language: String, symbols: Boolean, antiquotes: Boolean)
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   240
  {
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   241
    def is_outer: Boolean = language == ""
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   242
  }
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   243
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   244
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   245
  /* init */
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   246
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   247
  val empty: Completion = new Completion()
63871
f745c6e683b7 discontinued global etc/abbrevs;
wenzelm
parents: 63869
diff changeset
   248
  def init(): Completion =
f745c6e683b7 discontinued global etc/abbrevs;
wenzelm
parents: 63869
diff changeset
   249
    empty.add_symbols.add_abbrevs(Completion.symbol_abbrevs ::: Completion.default_abbrevs)
55694
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   250
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   251
a1184dfb8e00 clarified semantic completion: retain kind.full_name as official item name for history;
wenzelm
parents: 55693
diff changeset
   252
  /* word parsers */
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   253
63587
881e8e2cfec2 implicit keyword completion only for actual words (amending 73939a9b70a3);
wenzelm
parents: 63579
diff changeset
   254
  object Word_Parsers extends RegexParsers
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   255
  {
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   256
    override val whiteSpace = "".r
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   257
61613
e4194168a1eb allow open symboloid;
wenzelm
parents: 61600
diff changeset
   258
    private val symboloid_regex: Regex = """\\([A-Za-z0-9_']+|<\^?[A-Za-z0-9_']+>?)""".r
61600
1ca11ddfcc70 clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);
wenzelm
parents: 61599
diff changeset
   259
    def is_symboloid(s: CharSequence): Boolean = symboloid_regex.pattern.matcher(s).matches
57589
e0e4ac981cf1 always complete explicit symbols;
wenzelm
parents: 57588
diff changeset
   260
55615
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55497
diff changeset
   261
    private def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55497
diff changeset
   262
    private def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
61599
wenzelm
parents: 61100
diff changeset
   263
    private def reverse_escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r
55615
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55497
diff changeset
   264
56039
5ff5208de089 include long identifiers in the reckoning of words (e.g. "integer.lifting" vs. 'lifting_update');
wenzelm
parents: 56001
diff changeset
   265
    private val word_regex = "[a-zA-Z0-9_'.]+".r
63887
2d9c12eba726 more uniform completion of short word: exclude single character prefix but include two chracter prefix (see also 31633e503c17);
wenzelm
parents: 63873
diff changeset
   266
    private def word2: Parser[String] = "[a-zA-Z0-9_'.]{2,}".r
55996
13a7d9661ffc allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents: 55994
diff changeset
   267
    private def underscores: Parser[String] = "_*".r
55615
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55497
diff changeset
   268
55813
08a1c860bc12 allow completion within a word (or symbol), like semantic completion;
wenzelm
parents: 55749
diff changeset
   269
    def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
56042
d3c35a300433 proper Char comparison, despite weakly-typed Scala (cf. 5ff5208de089);
wenzelm
parents: 56039
diff changeset
   270
    def is_word_char(c: Char): Boolean = Symbol.is_ascii_letdig(c) || c == '.'
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   271
55813
08a1c860bc12 allow completion within a word (or symbol), like semantic completion;
wenzelm
parents: 55749
diff changeset
   272
    def read_symbol(in: CharSequence): Option[String] =
08a1c860bc12 allow completion within a word (or symbol), like semantic completion;
wenzelm
parents: 55749
diff changeset
   273
    {
08a1c860bc12 allow completion within a word (or symbol), like semantic completion;
wenzelm
parents: 55749
diff changeset
   274
      val reverse_in = new Library.Reverse(in)
08a1c860bc12 allow completion within a word (or symbol), like semantic completion;
wenzelm
parents: 55749
diff changeset
   275
      parse(reverse_symbol ^^ (_.reverse), reverse_in) match {
08a1c860bc12 allow completion within a word (or symbol), like semantic completion;
wenzelm
parents: 55749
diff changeset
   276
        case Success(result, _) => Some(result)
08a1c860bc12 allow completion within a word (or symbol), like semantic completion;
wenzelm
parents: 55749
diff changeset
   277
        case _ => None
08a1c860bc12 allow completion within a word (or symbol), like semantic completion;
wenzelm
parents: 55749
diff changeset
   278
      }
08a1c860bc12 allow completion within a word (or symbol), like semantic completion;
wenzelm
parents: 55749
diff changeset
   279
    }
08a1c860bc12 allow completion within a word (or symbol), like semantic completion;
wenzelm
parents: 55749
diff changeset
   280
63887
2d9c12eba726 more uniform completion of short word: exclude single character prefix but include two chracter prefix (see also 31633e503c17);
wenzelm
parents: 63873
diff changeset
   281
    def read_word(in: CharSequence): Option[(String, String)] =
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   282
    {
37072
9105c8237c7a renamed "rev" to "reverse" following usual Scala conventions;
wenzelm
parents: 36012
diff changeset
   283
      val reverse_in = new Library.Reverse(in)
55996
13a7d9661ffc allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents: 55994
diff changeset
   284
      val parser =
61599
wenzelm
parents: 61100
diff changeset
   285
        (reverse_symbol | reverse_symb | reverse_escape) ^^ (x => (x.reverse, "")) |
63887
2d9c12eba726 more uniform completion of short word: exclude single character prefix but include two chracter prefix (see also 31633e503c17);
wenzelm
parents: 63873
diff changeset
   286
        underscores ~ word2 ~ opt("?") ^^
56221
a8dfbe9f25da accomodate word as part of schematic variable name;
wenzelm
parents: 56175
diff changeset
   287
        { case x ~ y ~ z => (z.getOrElse("") + y.reverse, x) }
55996
13a7d9661ffc allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents: 55994
diff changeset
   288
      parse(parser, reverse_in) match {
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   289
        case Success(result, _) => Some(result)
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   290
        case _ => None
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   291
      }
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   292
    }
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   293
  }
55666
cc350eb1087e refined language context: antiquotes;
wenzelm
parents: 55618
diff changeset
   294
cc350eb1087e refined language context: antiquotes;
wenzelm
parents: 55618
diff changeset
   295
63871
f745c6e683b7 discontinued global etc/abbrevs;
wenzelm
parents: 63869
diff changeset
   296
  /* templates */
61960
20c1321378db support additional abbrevs;
wenzelm
parents: 61622
diff changeset
   297
63869
wenzelm
parents: 63808
diff changeset
   298
  val caret_indicator = '\u0007'
63871
f745c6e683b7 discontinued global etc/abbrevs;
wenzelm
parents: 63869
diff changeset
   299
63869
wenzelm
parents: 63808
diff changeset
   300
  def split_template(s: String): (String, String) =
wenzelm
parents: 63808
diff changeset
   301
    space_explode(caret_indicator, s) match {
wenzelm
parents: 63808
diff changeset
   302
      case List(s1, s2) => (s1, s2)
wenzelm
parents: 63808
diff changeset
   303
      case _ => (s, "")
wenzelm
parents: 63808
diff changeset
   304
    }
wenzelm
parents: 63808
diff changeset
   305
63871
f745c6e683b7 discontinued global etc/abbrevs;
wenzelm
parents: 63869
diff changeset
   306
f745c6e683b7 discontinued global etc/abbrevs;
wenzelm
parents: 63869
diff changeset
   307
  /* abbreviations */
f745c6e683b7 discontinued global etc/abbrevs;
wenzelm
parents: 63869
diff changeset
   308
f745c6e683b7 discontinued global etc/abbrevs;
wenzelm
parents: 63869
diff changeset
   309
  private def symbol_abbrevs: Thy_Header.Abbrevs =
f745c6e683b7 discontinued global etc/abbrevs;
wenzelm
parents: 63869
diff changeset
   310
    for ((sym, abbr) <- Symbol.abbrevs.toList) yield (abbr, sym)
f745c6e683b7 discontinued global etc/abbrevs;
wenzelm
parents: 63869
diff changeset
   311
55666
cc350eb1087e refined language context: antiquotes;
wenzelm
parents: 55618
diff changeset
   312
  private val antiquote = "@{"
56878
a5d082a85124 hardwired default_frequency to avoid fluctuation of popup content;
wenzelm
parents: 56800
diff changeset
   313
63578
wenzelm
parents: 63135
diff changeset
   314
  private val default_abbrevs =
56878
a5d082a85124 hardwired default_frequency to avoid fluctuation of popup content;
wenzelm
parents: 56800
diff changeset
   315
    List("@{" -> "@{\u0007}",
a5d082a85124 hardwired default_frequency to avoid fluctuation of popup content;
wenzelm
parents: 56800
diff changeset
   316
      "`" -> "\\<close>",
a5d082a85124 hardwired default_frequency to avoid fluctuation of popup content;
wenzelm
parents: 56800
diff changeset
   317
      "`" -> "\\<open>",
63135
035785035a1a cartouche abbreviations work both for " as well;
wenzelm
parents: 62969
diff changeset
   318
      "`" -> "\\<open>\u0007\\<close>",
035785035a1a cartouche abbreviations work both for " as well;
wenzelm
parents: 62969
diff changeset
   319
      "\"" -> "\\<close>",
035785035a1a cartouche abbreviations work both for " as well;
wenzelm
parents: 62969
diff changeset
   320
      "\"" -> "\\<open>",
035785035a1a cartouche abbreviations work both for " as well;
wenzelm
parents: 62969
diff changeset
   321
      "\"" -> "\\<open>\u0007\\<close>")
56878
a5d082a85124 hardwired default_frequency to avoid fluctuation of popup content;
wenzelm
parents: 56800
diff changeset
   322
a5d082a85124 hardwired default_frequency to avoid fluctuation of popup content;
wenzelm
parents: 56800
diff changeset
   323
  private def default_frequency(name: String): Option[Int] =
63578
wenzelm
parents: 63135
diff changeset
   324
    default_abbrevs.iterator.map(_._2).zipWithIndex.find(_._1 == name).map(_._2)
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   325
}
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   326
46712
8650d9a95736 prefer final ADTs -- prevent ooddities;
wenzelm
parents: 46625
diff changeset
   327
final class Completion private(
63579
73939a9b70a3 support 'abbrevs' within theory header;
wenzelm
parents: 63578
diff changeset
   328
  protected val keywords: Set[String] = Set.empty,
59073
dcecfcc56dce more merge operations;
wenzelm
parents: 57602
diff changeset
   329
  protected val words_lex: Scan.Lexicon = Scan.Lexicon.empty,
dcecfcc56dce more merge operations;
wenzelm
parents: 57602
diff changeset
   330
  protected val words_map: Multi_Map[String, String] = Multi_Map.empty,
dcecfcc56dce more merge operations;
wenzelm
parents: 57602
diff changeset
   331
  protected val abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
dcecfcc56dce more merge operations;
wenzelm
parents: 57602
diff changeset
   332
  protected val abbrevs_map: Multi_Map[String, (String, String)] = Multi_Map.empty)
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   333
{
59073
dcecfcc56dce more merge operations;
wenzelm
parents: 57602
diff changeset
   334
  /* merge */
dcecfcc56dce more merge operations;
wenzelm
parents: 57602
diff changeset
   335
dcecfcc56dce more merge operations;
wenzelm
parents: 57602
diff changeset
   336
  def is_empty: Boolean =
dcecfcc56dce more merge operations;
wenzelm
parents: 57602
diff changeset
   337
    keywords.isEmpty &&
dcecfcc56dce more merge operations;
wenzelm
parents: 57602
diff changeset
   338
    words_lex.is_empty &&
dcecfcc56dce more merge operations;
wenzelm
parents: 57602
diff changeset
   339
    words_map.isEmpty &&
dcecfcc56dce more merge operations;
wenzelm
parents: 57602
diff changeset
   340
    abbrevs_lex.is_empty &&
dcecfcc56dce more merge operations;
wenzelm
parents: 57602
diff changeset
   341
    abbrevs_map.isEmpty
dcecfcc56dce more merge operations;
wenzelm
parents: 57602
diff changeset
   342
dcecfcc56dce more merge operations;
wenzelm
parents: 57602
diff changeset
   343
  def ++ (other: Completion): Completion =
dcecfcc56dce more merge operations;
wenzelm
parents: 57602
diff changeset
   344
    if (this eq other) this
dcecfcc56dce more merge operations;
wenzelm
parents: 57602
diff changeset
   345
    else if (is_empty) other
dcecfcc56dce more merge operations;
wenzelm
parents: 57602
diff changeset
   346
    else {
63579
73939a9b70a3 support 'abbrevs' within theory header;
wenzelm
parents: 63578
diff changeset
   347
      val keywords1 = (keywords /: other.keywords) { case (ks, k) => if (ks(k)) ks else ks + k }
59073
dcecfcc56dce more merge operations;
wenzelm
parents: 57602
diff changeset
   348
      val words_lex1 = words_lex ++ other.words_lex
dcecfcc56dce more merge operations;
wenzelm
parents: 57602
diff changeset
   349
      val words_map1 = words_map ++ other.words_map
dcecfcc56dce more merge operations;
wenzelm
parents: 57602
diff changeset
   350
      val abbrevs_lex1 = abbrevs_lex ++ other.abbrevs_lex
dcecfcc56dce more merge operations;
wenzelm
parents: 57602
diff changeset
   351
      val abbrevs_map1 = abbrevs_map ++ other.abbrevs_map
dcecfcc56dce more merge operations;
wenzelm
parents: 57602
diff changeset
   352
      new Completion(keywords1, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
dcecfcc56dce more merge operations;
wenzelm
parents: 57602
diff changeset
   353
    }
dcecfcc56dce more merge operations;
wenzelm
parents: 57602
diff changeset
   354
dcecfcc56dce more merge operations;
wenzelm
parents: 57602
diff changeset
   355
55983
fc5977bd4829 misc tuning and clarification;
wenzelm
parents: 55982
diff changeset
   356
  /* keywords */
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   357
55986
61b0021ed674 more strict discrimination: symbols vs. keywords could overlap;
wenzelm
parents: 55985
diff changeset
   358
  private def is_symbol(name: String): Boolean = Symbol.names.isDefinedAt(name)
63579
73939a9b70a3 support 'abbrevs' within theory header;
wenzelm
parents: 63578
diff changeset
   359
  private def is_keyword(name: String): Boolean = !is_symbol(name) && keywords(name)
56001
2df1e7bca361 do allow replacement of words where this is appropriate, notably symbol abbrevs and keyword templates (see also 1c42ebdb3a58);
wenzelm
parents: 55996
diff changeset
   360
  private def is_keyword_template(name: String, template: Boolean): Boolean =
63579
73939a9b70a3 support 'abbrevs' within theory header;
wenzelm
parents: 63578
diff changeset
   361
    is_keyword(name) && (words_map.getOrElse(name, name) != name) == template
55984
2aaecd737d75 more accurate description;
wenzelm
parents: 55983
diff changeset
   362
63579
73939a9b70a3 support 'abbrevs' within theory header;
wenzelm
parents: 63578
diff changeset
   363
  def add_keyword(keyword: String): Completion =
73939a9b70a3 support 'abbrevs' within theory header;
wenzelm
parents: 63578
diff changeset
   364
    new Completion(keywords + keyword, words_lex, words_map, abbrevs_lex, abbrevs_map)
40533
e38e80686ce5 somewhat adhoc replacement for 'thus' and 'hence';
wenzelm
parents: 37072
diff changeset
   365
55983
fc5977bd4829 misc tuning and clarification;
wenzelm
parents: 55982
diff changeset
   366
63578
wenzelm
parents: 63135
diff changeset
   367
  /* symbols and abbrevs */
55983
fc5977bd4829 misc tuning and clarification;
wenzelm
parents: 55982
diff changeset
   368
63871
f745c6e683b7 discontinued global etc/abbrevs;
wenzelm
parents: 63869
diff changeset
   369
  def add_symbols: Completion =
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   370
  {
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   371
    val words =
61599
wenzelm
parents: 61100
diff changeset
   372
      (for ((sym, _) <- Symbol.names.toList) yield (sym, sym)) :::
63578
wenzelm
parents: 63135
diff changeset
   373
      (for ((sym, name) <- Symbol.names.toList) yield ("\\" + name, sym))
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   374
63578
wenzelm
parents: 63135
diff changeset
   375
    new Completion(
wenzelm
parents: 63135
diff changeset
   376
      keywords,
wenzelm
parents: 63135
diff changeset
   377
      words_lex ++ words.map(_._1),
wenzelm
parents: 63135
diff changeset
   378
      words_map ++ words,
wenzelm
parents: 63135
diff changeset
   379
      abbrevs_lex,
wenzelm
parents: 63135
diff changeset
   380
      abbrevs_map)
wenzelm
parents: 63135
diff changeset
   381
  }
55666
cc350eb1087e refined language context: antiquotes;
wenzelm
parents: 55618
diff changeset
   382
63578
wenzelm
parents: 63135
diff changeset
   383
  def add_abbrevs(abbrevs: List[(String, String)]): Completion =
63808
e8462a4349fc strictly sequential abbrevs;
wenzelm
parents: 63761
diff changeset
   384
    (this /: abbrevs)(_.add_abbrev(_))
e8462a4349fc strictly sequential abbrevs;
wenzelm
parents: 63761
diff changeset
   385
e8462a4349fc strictly sequential abbrevs;
wenzelm
parents: 63761
diff changeset
   386
  private def add_abbrev(abbrev: (String, String)): Completion =
63873
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents: 63871
diff changeset
   387
    abbrev match {
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents: 63871
diff changeset
   388
      case ("", _) => this
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents: 63871
diff changeset
   389
      case (abbr, text) =>
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents: 63871
diff changeset
   390
        val rev_abbr = abbr.reverse
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents: 63871
diff changeset
   391
        val is_word = Completion.Word_Parsers.is_word(abbr)
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   392
63873
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents: 63871
diff changeset
   393
        val (words_lex1, words_map1) =
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents: 63871
diff changeset
   394
          if (!is_word) (words_lex, words_map)
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents: 63871
diff changeset
   395
          else if (text != "") (words_lex + abbr, words_map + abbrev)
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents: 63871
diff changeset
   396
          else (words_lex -- List(abbr), words_map - abbr)
63808
e8462a4349fc strictly sequential abbrevs;
wenzelm
parents: 63761
diff changeset
   397
63873
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents: 63871
diff changeset
   398
        val (abbrevs_lex1, abbrevs_map1) =
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents: 63871
diff changeset
   399
          if (is_word) (abbrevs_lex, abbrevs_map)
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents: 63871
diff changeset
   400
          else if (text != "") (abbrevs_lex + rev_abbr, abbrevs_map + (rev_abbr -> abbrev))
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents: 63871
diff changeset
   401
          else (abbrevs_lex -- List(rev_abbr), abbrevs_map - rev_abbr)
63808
e8462a4349fc strictly sequential abbrevs;
wenzelm
parents: 63761
diff changeset
   402
63873
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents: 63871
diff changeset
   403
        new Completion(keywords, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs;
wenzelm
parents: 63871
diff changeset
   404
    }
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   405
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   406
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   407
  /* complete */
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   408
53337
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   409
  def complete(
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   410
    history: Completion.History,
55977
ec4830499634 more detailed description of completion items;
wenzelm
parents: 55914
diff changeset
   411
    do_decode: Boolean,
53337
b3817a0e3211 sort items according to persistent history of frequency of use;
wenzelm
parents: 53325
diff changeset
   412
    explicit: Boolean,
55813
08a1c860bc12 allow completion within a word (or symbol), like semantic completion;
wenzelm
parents: 55749
diff changeset
   413
    start: Text.Offset,
55615
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55497
diff changeset
   414
    text: CharSequence,
55813
08a1c860bc12 allow completion within a word (or symbol), like semantic completion;
wenzelm
parents: 55749
diff changeset
   415
    caret: Int,
55749
75a48dc4383e tuned signature;
wenzelm
parents: 55748
diff changeset
   416
    language_context: Completion.Language_Context): Option[Completion.Result] =
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   417
  {
55977
ec4830499634 more detailed description of completion items;
wenzelm
parents: 55914
diff changeset
   418
    def decode(s: String): String = if (do_decode) Symbol.decode(s) else s
55813
08a1c860bc12 allow completion within a word (or symbol), like semantic completion;
wenzelm
parents: 55749
diff changeset
   419
    val length = text.length
08a1c860bc12 allow completion within a word (or symbol), like semantic completion;
wenzelm
parents: 55749
diff changeset
   420
55615
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55497
diff changeset
   421
    val abbrevs_result =
55813
08a1c860bc12 allow completion within a word (or symbol), like semantic completion;
wenzelm
parents: 55749
diff changeset
   422
    {
08a1c860bc12 allow completion within a word (or symbol), like semantic completion;
wenzelm
parents: 55749
diff changeset
   423
      val reverse_in = new Library.Reverse(text.subSequence(0, caret))
08a1c860bc12 allow completion within a word (or symbol), like semantic completion;
wenzelm
parents: 55749
diff changeset
   424
      Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), reverse_in) match {
61599
wenzelm
parents: 61100
diff changeset
   425
        case Scan.Parsers.Success(reverse_abbr, _) =>
wenzelm
parents: 61100
diff changeset
   426
          val abbrevs = abbrevs_map.get_list(reverse_abbr)
55666
cc350eb1087e refined language context: antiquotes;
wenzelm
parents: 55618
diff changeset
   427
          abbrevs match {
cc350eb1087e refined language context: antiquotes;
wenzelm
parents: 55618
diff changeset
   428
            case Nil => None
61599
wenzelm
parents: 61100
diff changeset
   429
            case (abbr, _) :: _ =>
55666
cc350eb1087e refined language context: antiquotes;
wenzelm
parents: 55618
diff changeset
   430
              val ok =
61599
wenzelm
parents: 61100
diff changeset
   431
                if (abbr == Completion.antiquote) language_context.antiquotes
63578
wenzelm
parents: 63135
diff changeset
   432
                else language_context.symbols || Completion.default_abbrevs.exists(_._1 == abbr)
61599
wenzelm
parents: 61100
diff changeset
   433
              if (ok) Some((abbr, abbrevs))
55813
08a1c860bc12 allow completion within a word (or symbol), like semantic completion;
wenzelm
parents: 55749
diff changeset
   434
              else None
55666
cc350eb1087e refined language context: antiquotes;
wenzelm
parents: 55618
diff changeset
   435
          }
cc350eb1087e refined language context: antiquotes;
wenzelm
parents: 55618
diff changeset
   436
        case _ => None
cc350eb1087e refined language context: antiquotes;
wenzelm
parents: 55618
diff changeset
   437
      }
55813
08a1c860bc12 allow completion within a word (or symbol), like semantic completion;
wenzelm
parents: 55749
diff changeset
   438
    }
55615
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55497
diff changeset
   439
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55497
diff changeset
   440
    val words_result =
55982
b719781c7396 more accurate description;
wenzelm
parents: 55978
diff changeset
   441
      if (abbrevs_result.isDefined) None
b719781c7396 more accurate description;
wenzelm
parents: 55978
diff changeset
   442
      else {
57602
0f708666eb7c no keyword completion within word context -- especially avoid its odd visual rendering;
wenzelm
parents: 57589
diff changeset
   443
        val word_context =
0f708666eb7c no keyword completion within word context -- especially avoid its odd visual rendering;
wenzelm
parents: 57589
diff changeset
   444
          caret < length && Completion.Word_Parsers.is_word_char(text.charAt(caret))
55996
13a7d9661ffc allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents: 55994
diff changeset
   445
        val result =
57588
ff31aad27661 discontinued unfinished attempts at syntactic word context (see 2e1398b484aa, 08a1c860bc12, 7f229b0212fe) -- back to more basic completion of Isabelle2013-2;
wenzelm
parents: 56878
diff changeset
   446
          Completion.Word_Parsers.read_symbol(text.subSequence(0, caret)) match {
55996
13a7d9661ffc allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents: 55994
diff changeset
   447
            case Some(symbol) => Some((symbol, ""))
63887
2d9c12eba726 more uniform completion of short word: exclude single character prefix but include two chracter prefix (see also 31633e503c17);
wenzelm
parents: 63873
diff changeset
   448
            case None => Completion.Word_Parsers.read_word(text.subSequence(0, caret))
55992
wenzelm
parents: 55986
diff changeset
   449
          }
55996
13a7d9661ffc allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents: 55994
diff changeset
   450
        result.map(
55992
wenzelm
parents: 55986
diff changeset
   451
          {
55996
13a7d9661ffc allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents: 55994
diff changeset
   452
            case (word, underscores) =>
13a7d9661ffc allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents: 55994
diff changeset
   453
              val complete_words = words_lex.completions(word)
13a7d9661ffc allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents: 55994
diff changeset
   454
              val full_word = word + underscores
13a7d9661ffc allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents: 55994
diff changeset
   455
              val completions =
56001
2df1e7bca361 do allow replacement of words where this is appropriate, notably symbol abbrevs and keyword templates (see also 1c42ebdb3a58);
wenzelm
parents: 55996
diff changeset
   456
                if (complete_words.contains(full_word) && is_keyword_template(full_word, false)) Nil
55996
13a7d9661ffc allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents: 55994
diff changeset
   457
                else
13a7d9661ffc allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents: 55994
diff changeset
   458
                  for {
13a7d9661ffc allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents: 55994
diff changeset
   459
                    complete_word <- complete_words
13a7d9661ffc allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents: 55994
diff changeset
   460
                    ok =
57602
0f708666eb7c no keyword completion within word context -- especially avoid its odd visual rendering;
wenzelm
parents: 57589
diff changeset
   461
                      if (is_keyword(complete_word)) !word_context && language_context.is_outer
61600
1ca11ddfcc70 clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);
wenzelm
parents: 61599
diff changeset
   462
                      else language_context.symbols || Completion.Word_Parsers.is_symboloid(word)
55996
13a7d9661ffc allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents: 55994
diff changeset
   463
                    if ok
13a7d9661ffc allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents: 55994
diff changeset
   464
                    completion <- words_map.get_list(complete_word)
13a7d9661ffc allow suffix of underscores for words (notably keywords), similar to semantic completion;
wenzelm
parents: 55994
diff changeset
   465
                  } yield (complete_word, completion)
60215
5fb4990dfc73 misc tuning, based on warnings by IntelliJ IDEA;
wenzelm
parents: 59717
diff changeset
   466
              (full_word, completions)
55992
wenzelm
parents: 55986
diff changeset
   467
          })
53275
b34aac6511ab tuned signature;
wenzelm
parents: 53251
diff changeset
   468
      }
55615
bf4bbe72f740 completion of keywords and symbols based on language context;
wenzelm
parents: 55497
diff changeset
   469
55982
b719781c7396 more accurate description;
wenzelm
parents: 55978
diff changeset
   470
    (abbrevs_result orElse words_result) match {
59319
wenzelm
parents: 59073
diff changeset
   471
      case Some((original, completions)) if completions.nonEmpty =>
57588
ff31aad27661 discontinued unfinished attempts at syntactic word context (see 2e1398b484aa, 08a1c860bc12, 7f229b0212fe) -- back to more basic completion of Isabelle2013-2;
wenzelm
parents: 56878
diff changeset
   472
        val range = Text.Range(- original.length, 0) + caret + start
55985
wenzelm
parents: 55984
diff changeset
   473
        val immediate =
wenzelm
parents: 55984
diff changeset
   474
          explicit ||
wenzelm
parents: 55984
diff changeset
   475
            (!Completion.Word_Parsers.is_word(original) &&
61600
1ca11ddfcc70 clarified completion of explicit symbols (see also f6bd97a587b7, e0e4ac981cf1);
wenzelm
parents: 61599
diff changeset
   476
             !Completion.Word_Parsers.is_symboloid(original) &&
55985
wenzelm
parents: 55984
diff changeset
   477
              Character.codePointCount(original, 0, original.length) > 1)
55993
4c17e46c44c1 clarified description;
wenzelm
parents: 55992
diff changeset
   478
        val unique = completions.length == 1
55985
wenzelm
parents: 55984
diff changeset
   479
wenzelm
parents: 55984
diff changeset
   480
        val items =
wenzelm
parents: 55984
diff changeset
   481
          for {
55993
4c17e46c44c1 clarified description;
wenzelm
parents: 55992
diff changeset
   482
            (complete_word, name0) <- completions
4c17e46c44c1 clarified description;
wenzelm
parents: 55992
diff changeset
   483
            name1 = decode(name0)
55985
wenzelm
parents: 55984
diff changeset
   484
            if name1 != original
63869
wenzelm
parents: 63808
diff changeset
   485
            (s1, s2) = Completion.split_template(name1)
55985
wenzelm
parents: 55984
diff changeset
   486
            move = - s2.length
wenzelm
parents: 55984
diff changeset
   487
            description =
wenzelm
parents: 55984
diff changeset
   488
              if (is_symbol(name0)) {
wenzelm
parents: 55984
diff changeset
   489
                if (name0 == name1) List(name0)
wenzelm
parents: 55984
diff changeset
   490
                else List(name1, "(symbol " + quote(name0) + ")")
wenzelm
parents: 55984
diff changeset
   491
              }
56001
2df1e7bca361 do allow replacement of words where this is appropriate, notably symbol abbrevs and keyword templates (see also 1c42ebdb3a58);
wenzelm
parents: 55996
diff changeset
   492
              else if (is_keyword_template(complete_word, true))
55993
4c17e46c44c1 clarified description;
wenzelm
parents: 55992
diff changeset
   493
                List(name1, "(template " + quote(complete_word) + ")")
4c17e46c44c1 clarified description;
wenzelm
parents: 55992
diff changeset
   494
              else if (move != 0) List(name1, "(template)")
4c17e46c44c1 clarified description;
wenzelm
parents: 55992
diff changeset
   495
              else if (is_keyword(complete_word)) List(name1, "(keyword)")
55985
wenzelm
parents: 55984
diff changeset
   496
              else List(name1)
wenzelm
parents: 55984
diff changeset
   497
          }
wenzelm
parents: 55984
diff changeset
   498
          yield Completion.Item(range, original, name1, description, s1 + s2, move, immediate)
wenzelm
parents: 55984
diff changeset
   499
wenzelm
parents: 55984
diff changeset
   500
        if (items.isEmpty) None
56174
wenzelm
parents: 56173
diff changeset
   501
        else
wenzelm
parents: 56173
diff changeset
   502
          Some(Completion.Result(range, original, unique,
wenzelm
parents: 56173
diff changeset
   503
            items.sortBy(_.name).sorted(history.ordering)))
55985
wenzelm
parents: 55984
diff changeset
   504
55992
wenzelm
parents: 55986
diff changeset
   505
      case _ => None
31765
a5fdf7a76f9d tuned input: require longer symbol prefix;
wenzelm
parents: 31763
diff changeset
   506
    }
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   507
  }
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   508
}