# HG changeset patch
# User wenzelm
# Date 1497029009 -7200
# Node ID cd8d0ad5ac1990938f161b86fd69791a3f845594
# Parent  39eb61b1fa51bee4b2b9614125091511f8ee7111
clarified modules;

diff -r 39eb61b1fa51 -r cd8d0ad5ac19 src/Pure/PIDE/rendering.scala
--- 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 */
 
diff -r 39eb61b1fa51 -r cd8d0ad5ac19 src/Tools/jEdit/src/jedit_rendering.scala
--- 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)] =