--- a/src/Pure/PIDE/rendering.scala Fri Jun 09 17:13:50 2017 +0200
+++ b/src/Pure/PIDE/rendering.scala Fri Jun 09 19:23:29 2017 +0200
@@ -153,6 +153,18 @@
/* markup elements */
+ val semantic_completion_elements =
+ Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
+
+ val language_context_elements =
+ Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
+ Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
+ Markup.ML_STRING, Markup.ML_COMMENT)
+
+ val language_elements = Markup.Elements(Markup.LANGUAGE)
+
+ val citation_elements = Markup.Elements(Markup.CITATION)
+
val active_elements =
Markup.Elements(Markup.DIALOG, Markup.BROWSER, Markup.GRAPHVIEW,
Markup.SENDBACK, Markup.JEDIT_ACTION, Markup.SIMP_TRACE_PANEL)
@@ -169,9 +181,6 @@
Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
Markup.CARTOUCHE, Markup.ANTIQUOTED)
- val semantic_completion_elements =
- Markup.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
-
val tooltip_elements =
Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
@@ -212,6 +221,35 @@
}).headOption.map(_.info)
}
+ def language_context(range: Text.Range): Option[Completion.Language_Context] =
+ snapshot.select(range, Rendering.language_context_elements, _ =>
+ {
+ case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes, delimited), _)) =>
+ if (delimited) Some(Completion.Language_Context(language, symbols, antiquotes))
+ else None
+ case Text.Info(_, elem)
+ if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
+ Some(Completion.Language_Context.ML_inner)
+ case Text.Info(_, _) =>
+ Some(Completion.Language_Context.inner)
+ }).headOption.map(_.info)
+
+ def language_path(range: Text.Range): Option[Text.Range] =
+ snapshot.select(range, Rendering.language_elements, _ =>
+ {
+ case Text.Info(info_range, XML.Elem(Markup.Language(Markup.Language.PATH, _, _, _), _)) =>
+ Some(snapshot.convert(info_range))
+ case _ => None
+ }).headOption.map(_.info)
+
+ def citation(range: Text.Range): Option[Text.Info[String]] =
+ snapshot.select(range, Rendering.citation_elements, _ =>
+ {
+ case Text.Info(info_range, XML.Elem(Markup.Citation(name), _)) =>
+ Some(Text.Info(snapshot.convert(info_range), name))
+ case _ => None
+ }).headOption.map(_.info)
+
/* spell checker */
--- a/src/Tools/jEdit/src/jedit_rendering.scala Fri Jun 09 17:13:50 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Fri Jun 09 19:23:29 2017 +0200
@@ -113,15 +113,6 @@
private val indentation_elements =
Markup.Elements(Markup.Command_Indent.name)
- private val language_context_elements =
- Markup.Elements(Markup.STRING, Markup.ALT_STRING, Markup.VERBATIM,
- Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
- Markup.ML_STRING, Markup.ML_COMMENT)
-
- private val language_elements = Markup.Elements(Markup.LANGUAGE)
-
- private val citation_elements = Markup.Elements(Markup.CITATION)
-
private val breakpoint_elements = Markup.Elements(Markup.ML_BREAKPOINT)
private val highlight_elements =
@@ -199,38 +190,6 @@
}).headOption.map(_.info).getOrElse(0)
- /* completion */
-
- def language_context(range: Text.Range): Option[Completion.Language_Context] =
- snapshot.select(range, JEdit_Rendering.language_context_elements, _ =>
- {
- case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes, delimited), _)) =>
- if (delimited) Some(Completion.Language_Context(language, symbols, antiquotes))
- else None
- case Text.Info(_, elem)
- if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
- Some(Completion.Language_Context.ML_inner)
- case Text.Info(_, _) =>
- Some(Completion.Language_Context.inner)
- }).headOption.map(_.info)
-
- def language_path(range: Text.Range): Option[Text.Range] =
- snapshot.select(range, JEdit_Rendering.language_elements, _ =>
- {
- case Text.Info(info_range, XML.Elem(Markup.Language(Markup.Language.PATH, _, _, _), _)) =>
- Some(snapshot.convert(info_range))
- case _ => None
- }).headOption.map(_.info)
-
- def citation(range: Text.Range): Option[Text.Info[String]] =
- snapshot.select(range, JEdit_Rendering.citation_elements, _ =>
- {
- case Text.Info(info_range, XML.Elem(Markup.Citation(name), _)) =>
- Some(Text.Info(snapshot.convert(info_range), name))
- case _ => None
- }).headOption.map(_.info)
-
-
/* breakpoints */
def breakpoint(range: Text.Range): Option[(Command, Long)] =