equal
deleted
inserted
replaced
39 val empty: Outer_Syntax = new Outer_Syntax() |
39 val empty: Outer_Syntax = new Outer_Syntax() |
40 def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init()) |
40 def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init()) |
41 } |
41 } |
42 |
42 |
43 final class Outer_Syntax private( |
43 final class Outer_Syntax private( |
44 keywords: Map[String, String] = Map((";" -> Keyword.DIAG)), |
44 keywords: Map[String, String] = Map.empty, |
45 lexicon: Scan.Lexicon = Scan.Lexicon.empty, |
45 lexicon: Scan.Lexicon = Scan.Lexicon.empty, |
46 val completion: Completion = Completion.empty) |
46 val completion: Completion = Completion.empty) |
47 { |
47 { |
48 def keyword_kind(name: String): Option[String] = keywords.get(name) |
48 def keyword_kind(name: String): Option[String] = keywords.get(name) |
49 |
49 |