239 |
239 |
240 |
240 |
241 /* markup selectors */ |
241 /* markup selectors */ |
242 |
242 |
243 private val highlight_include = |
243 private val highlight_include = |
244 Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE, |
244 Set(Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE, |
245 Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING, Markup.TYPING, Markup.FREE, |
245 Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING, |
246 Markup.SKOLEM, Markup.BOUND, Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, |
246 Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND, |
247 Markup.DOCUMENT_SOURCE) |
247 Markup.VAR, Markup.TFREE, Markup.TVAR) |
248 |
248 |
249 def highlight(range: Text.Range): Option[Text.Info[Color]] = |
249 def highlight(range: Text.Range): Option[Text.Info[Color]] = |
250 { |
250 { |
251 snapshot.select_markup(range, Some(highlight_include), _ => |
251 snapshot.select_markup(range, Some(highlight_include), _ => |
252 { |
252 { |
373 } |
373 } |
374 |
374 |
375 |
375 |
376 private val tooltips: Map[String, String] = |
376 private val tooltips: Map[String, String] = |
377 Map( |
377 Map( |
378 Markup.SORT -> "sort", |
|
379 Markup.TYP -> "type", |
|
380 Markup.TERM -> "term", |
|
381 Markup.PROP -> "proposition", |
|
382 Markup.TOKEN_RANGE -> "inner syntax token", |
378 Markup.TOKEN_RANGE -> "inner syntax token", |
383 Markup.FREE -> "free variable", |
379 Markup.FREE -> "free variable", |
384 Markup.SKOLEM -> "skolem variable", |
380 Markup.SKOLEM -> "skolem variable", |
385 Markup.BOUND -> "bound variable", |
381 Markup.BOUND -> "bound variable", |
386 Markup.VAR -> "schematic variable", |
382 Markup.VAR -> "schematic variable", |
387 Markup.TFREE -> "free type variable", |
383 Markup.TFREE -> "free type variable", |
388 Markup.TVAR -> "schematic type variable", |
384 Markup.TVAR -> "schematic type variable") |
389 Markup.ML_SOURCE -> "ML source", |
|
390 Markup.DOCUMENT_SOURCE -> "document source") |
|
391 |
385 |
392 private val tooltip_elements = |
386 private val tooltip_elements = |
393 Set(Markup.TIMING, Markup.ENTITY, Markup.SORTING, Markup.TYPING, |
387 Set(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING, |
394 Markup.ML_TYPING, Markup.PATH, Markup.URL) ++ tooltips.keys |
388 Markup.TYPING, Markup.ML_TYPING, Markup.PATH, Markup.URL) ++ |
|
389 tooltips.keys |
395 |
390 |
396 private def pretty_typing(kind: String, body: XML.Body): XML.Tree = |
391 private def pretty_typing(kind: String, body: XML.Body): XML.Tree = |
397 Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body) |
392 Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body) |
398 |
393 |
399 private val timing_threshold: Double = options.real("jedit_timing_threshold") |
394 private val timing_threshold: Double = options.real("jedit_timing_threshold") |
432 case (prev, Text.Info(r, XML.Elem(Markup(name, _), body))) |
427 case (prev, Text.Info(r, XML.Elem(Markup(name, _), body))) |
433 if name == Markup.SORTING || name == Markup.TYPING => |
428 if name == Markup.SORTING || name == Markup.TYPING => |
434 Some(add(prev, r, (true, pretty_typing("::", body)))) |
429 Some(add(prev, r, (true, pretty_typing("::", body)))) |
435 case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) => |
430 case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) => |
436 Some(add(prev, r, (false, pretty_typing("ML:", body)))) |
431 Some(add(prev, r, (false, pretty_typing("ML:", body)))) |
|
432 case (prev, Text.Info(r, XML.Elem(Markup.Language(name), _))) => |
|
433 Some(add(prev, r, (true, XML.Text("language: " + name)))) |
437 case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) => |
434 case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) => |
438 if (tooltips.isDefinedAt(name)) |
435 if (tooltips.isDefinedAt(name)) |
439 Some(add(prev, r, (true, XML.Text(tooltips(name))))) |
436 Some(add(prev, r, (true, XML.Text(tooltips(name))))) |
440 else None |
437 else None |
441 }).map(_.info) |
438 }).map(_.info) |