65 /* popup window bounds */ |
65 /* popup window bounds */ |
66 |
66 |
67 def popup_bounds: Double = (PIDE.options.real("jedit_popup_bounds") max 0.2) min 0.8 |
67 def popup_bounds: Double = (PIDE.options.real("jedit_popup_bounds") max 0.2) min 0.8 |
68 |
68 |
69 |
69 |
70 /* token markup -- text styles */ |
70 /* Isabelle/Isar token markup */ |
71 |
71 |
72 private val command_style: Map[String, Byte] = |
72 private val command_style: Map[String, Byte] = |
73 { |
73 { |
74 import JEditToken._ |
74 import JEditToken._ |
75 Map[String, Byte]( |
75 Map[String, Byte]( |
109 def token_markup(syntax: Outer_Syntax, token: Token): Byte = |
109 def token_markup(syntax: Outer_Syntax, token: Token): Byte = |
110 if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse("")) |
110 if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse("")) |
111 else if (token.is_operator) JEditToken.OPERATOR |
111 else if (token.is_operator) JEditToken.OPERATOR |
112 else token_style(token.kind) |
112 else token_style(token.kind) |
113 |
113 |
|
114 |
|
115 /* Isabelle/ML token markup */ |
|
116 |
|
117 private val ml_keyword2: Set[String] = |
|
118 Set("case", "do", "else", "end", "if", "in", "let", "local", "of", |
|
119 "sig", "struct", "then", "while", "with") |
|
120 |
|
121 private val ml_keyword3: Set[String] = |
|
122 Set("handle", "open", "raise") |
|
123 |
114 private val ml_token_style: Map[ML_Lex.Kind.Value, Byte] = |
124 private val ml_token_style: Map[ML_Lex.Kind.Value, Byte] = |
115 { |
125 { |
116 import JEditToken._ |
126 import JEditToken._ |
117 Map[ML_Lex.Kind.Value, Byte]( |
127 Map[ML_Lex.Kind.Value, Byte]( |
118 ML_Lex.Kind.KEYWORD -> KEYWORD1, |
|
119 ML_Lex.Kind.IDENT -> NULL, |
128 ML_Lex.Kind.IDENT -> NULL, |
120 ML_Lex.Kind.LONG_IDENT -> NULL, |
129 ML_Lex.Kind.LONG_IDENT -> NULL, |
121 ML_Lex.Kind.TYPE_VAR -> NULL, |
130 ML_Lex.Kind.TYPE_VAR -> NULL, |
122 ML_Lex.Kind.WORD -> NULL, |
131 ML_Lex.Kind.WORD -> NULL, |
123 ML_Lex.Kind.INT -> NULL, |
132 ML_Lex.Kind.INT -> NULL, |
129 ML_Lex.Kind.ERROR -> INVALID |
138 ML_Lex.Kind.ERROR -> INVALID |
130 ).withDefaultValue(NULL) |
139 ).withDefaultValue(NULL) |
131 } |
140 } |
132 |
141 |
133 def ml_token_markup(token: ML_Lex.Token): Byte = |
142 def ml_token_markup(token: ML_Lex.Token): Byte = |
134 if (token.is_operator) JEditToken.OPERATOR |
143 if (!token.is_keyword) ml_token_style(token.kind) |
135 else ml_token_style(token.kind) |
144 else if (token.is_operator) JEditToken.OPERATOR |
|
145 else if (ml_keyword2(token.source)) JEditToken.KEYWORD2 |
|
146 else if (ml_keyword3(token.source)) JEditToken.KEYWORD3 |
|
147 else JEditToken.KEYWORD1 |
136 } |
148 } |
137 |
149 |
138 |
150 |
139 class Rendering private(val snapshot: Document.Snapshot, val options: Options) |
151 class Rendering private(val snapshot: Document.Snapshot, val options: Options) |
140 { |
152 { |