44 } |
44 } |
45 |
45 |
46 final class Outer_Syntax private( |
46 final class Outer_Syntax private( |
47 val keywords: Keyword.Keywords = Keyword.Keywords.empty, |
47 val keywords: Keyword.Keywords = Keyword.Keywords.empty, |
48 val completion: Completion = Completion.empty, |
48 val completion: Completion = Completion.empty, |
|
49 val rev_abbrevs: Thy_Header.Abbrevs = Nil, |
49 val language_context: Completion.Language_Context = Completion.Language_Context.outer, |
50 val language_context: Completion.Language_Context = Completion.Language_Context.outer, |
50 val has_tokens: Boolean = true) |
51 val has_tokens: Boolean = true) |
51 { |
52 { |
52 /** syntax content **/ |
53 /** syntax content **/ |
53 |
54 |
54 override def toString: String = keywords.toString |
55 override def toString: String = keywords.toString |
55 |
56 |
56 |
57 |
57 /* add keywords */ |
58 /* keywords */ |
58 |
59 |
59 def + (name: String, kind: String = "", tags: List[String] = Nil): Outer_Syntax = |
60 def + (name: String, kind: String = "", tags: List[String] = Nil): Outer_Syntax = |
60 { |
61 { |
61 val keywords1 = keywords + (name, kind, tags) |
62 val keywords1 = keywords + (name, kind, tags) |
62 val completion1 = |
63 val completion1 = |
63 completion.add_keyword(name). |
64 completion.add_keyword(name). |
64 add_abbrevs( |
65 add_abbrevs( |
65 (if (Keyword.theory_block.contains(kind)) List((name, name + "\nbegin\n\u0007\nend")) |
66 (if (Keyword.theory_block.contains(kind)) List((name, name + "\nbegin\n\u0007\nend")) |
66 else Nil) ::: |
67 else Nil) ::: |
67 (if (Completion.Word_Parsers.is_word(name)) List((name, name)) else Nil)) |
68 (if (Completion.Word_Parsers.is_word(name)) List((name, name)) else Nil)) |
68 new Outer_Syntax(keywords1, completion1, language_context, true) |
69 new Outer_Syntax(keywords1, completion1, rev_abbrevs, language_context, true) |
69 } |
70 } |
70 |
71 |
71 def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax = |
72 def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax = |
72 (this /: keywords) { |
73 (this /: keywords) { |
73 case (syntax, (name, ((kind, tags), _))) => |
74 case (syntax, (name, ((kind, tags), _))) => |
74 syntax + (Symbol.decode(name), kind, tags) + (Symbol.encode(name), kind, tags) |
75 syntax + (Symbol.decode(name), kind, tags) + (Symbol.encode(name), kind, tags) |
75 } |
76 } |
76 |
77 |
77 def add_abbrevs(abbrevs: Thy_Header.Abbrevs): Outer_Syntax = |
78 |
78 if (abbrevs.isEmpty) this |
79 /* abbrevs */ |
|
80 |
|
81 def abbrevs: Thy_Header.Abbrevs = rev_abbrevs.reverse |
|
82 |
|
83 def add_abbrevs(new_abbrevs: Thy_Header.Abbrevs): Outer_Syntax = |
|
84 if (new_abbrevs.isEmpty) this |
79 else { |
85 else { |
80 val completion1 = |
86 val completion1 = |
81 completion.add_abbrevs( |
87 completion.add_abbrevs( |
82 (for ((a, b) <- abbrevs) yield { |
88 (for ((a, b) <- new_abbrevs) yield { |
83 val a1 = Symbol.decode(a) |
89 val a1 = Symbol.decode(a) |
84 val a2 = Symbol.encode(a) |
90 val a2 = Symbol.encode(a) |
85 val b1 = Symbol.decode(b) |
91 val b1 = Symbol.decode(b) |
86 List((a1, b1), (a2, b1)) |
92 List((a1, b1), (a2, b1)) |
87 }).flatten) |
93 }).flatten) |
88 new Outer_Syntax(keywords, completion1, language_context, has_tokens) |
94 val rev_abbrevs1 = Library.distinct(new_abbrevs) reverse_::: rev_abbrevs |
|
95 new Outer_Syntax(keywords, completion1, rev_abbrevs1, language_context, has_tokens) |
89 } |
96 } |
90 |
97 |
91 |
98 |
92 /* merge */ |
99 /* merge */ |
93 |
100 |
94 def ++ (other: Outer_Syntax): Outer_Syntax = |
101 def ++ (other: Outer_Syntax): Outer_Syntax = |
95 if (this eq other) this |
102 if (this eq other) this |
96 else { |
103 else { |
97 val keywords1 = keywords ++ other.keywords |
104 val keywords1 = keywords ++ other.keywords |
98 val completion1 = completion ++ other.completion |
105 val completion1 = completion ++ other.completion |
|
106 val rev_abbrevs1 = Library.merge(rev_abbrevs, other.rev_abbrevs) |
99 if ((keywords eq keywords1) && (completion eq completion1)) this |
107 if ((keywords eq keywords1) && (completion eq completion1)) this |
100 else new Outer_Syntax(keywords1, completion1, language_context, has_tokens) |
108 else new Outer_Syntax(keywords1, completion1, rev_abbrevs1, language_context, has_tokens) |
101 } |
109 } |
102 |
110 |
103 |
111 |
104 /* load commands */ |
112 /* load commands */ |
105 |
113 |