src/Pure/Thy/completion.scala
changeset 31780 d78e5cff9a9f
parent 31765 a5fdf7a76f9d
child 34093 3d654643cf56
equal deleted inserted replaced
31779:68eccca7f51c 31780:d78e5cff9a9f
    66 
    66 
    67 class Completion
    67 class Completion
    68 {
    68 {
    69   /* representation */
    69   /* representation */
    70 
    70 
    71   val words_lex = Scan.Lexicon()
    71   protected val words_lex = Scan.Lexicon()
    72   val words_map = Map[String, String]()
    72   protected val words_map = Map[String, String]()
    73 
    73 
    74   val abbrevs_lex = Scan.Lexicon()
    74   protected val abbrevs_lex = Scan.Lexicon()
    75   val abbrevs_map = Map[String, (String, String)]()
    75   protected val abbrevs_map = Map[String, (String, String)]()
    76 
    76 
    77 
    77 
    78   /* adding stuff */
    78   /* adding stuff */
    79 
    79 
    80   def + (keyword: String): Completion =
    80   def + (keyword: String): Completion =