src/Pure/PIDE/rendering.scala
changeset 66053 cd8d0ad5ac19
parent 65913 f330f538dae6
child 66054 fb0eea226a4d
--- 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 */