# HG changeset patch
# User wenzelm
# Date 1395055440 -3600
# Node ID 62f10624339a9a7a255e7723280c53f1becbed7a
# Parent  31289387fdf80f9bb527941f2baa2a6996f6edb0
tuned signature;

diff -r 31289387fdf8 -r 62f10624339a src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Mon Mar 17 11:39:46 2014 +0100
+++ b/src/Pure/General/completion.scala	Mon Mar 17 12:24:00 2014 +0100
@@ -131,11 +131,11 @@
 
   /** semantic completion **/
 
-  object Names
+  object Semantic
   {
     object Info
     {
-      def unapply(info: Text.Markup): Option[Names] =
+      def unapply(info: Text.Markup): Option[Text.Info[Semantic]] =
         info.info match {
           case XML.Elem(Markup(Markup.COMPLETION, _), body) =>
             try {
@@ -144,22 +144,32 @@
                 import XML.Decode._
                 pair(int, list(pair(string, pair(string, string))))(body)
               }
-              Some(Names(info.range, total, names))
+              Some(Text.Info(info.range, Names(total, names)))
             }
             catch { case _: XML.Error => None }
           case XML.Elem(Markup(Markup.NO_COMPLETION, _), _) =>
-            Some(Names(info.range, 0, Nil))
+            Some(Text.Info(info.range, No_Completion))
           case _ => None
         }
     }
   }
 
-  sealed case class Names(
-    range: Text.Range, total: Int, names: List[(String, (String, String))])
+  sealed abstract class Semantic
   {
-    def no_completion: Boolean = total == 0 && names.isEmpty
-
+    def no_completion: Boolean = this == No_Completion
     def complete(
+      range: Text.Range,
+      history: Completion.History,
+      do_decode: Boolean,
+      original: String): Option[Completion.Result] = None
+  }
+  case object No_Completion extends Semantic
+  case class Names(
+    total: Int,
+    names: List[(String, (String, String))]) extends Semantic
+  {
+    override def complete(
+      range: Text.Range,
       history: Completion.History,
       do_decode: Boolean,
       original: String): Option[Completion.Result] =
diff -r 31289387fdf8 -r 62f10624339a src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Mon Mar 17 11:39:46 2014 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Mar 17 12:24:00 2014 +0100
@@ -139,10 +139,10 @@
           if (line_range.contains(text_area.getCaretPosition)) {
             before_caret_range(rendering).try_restrict(line_range) match {
               case Some(range) if !range.is_singularity =>
-                rendering.completion_names(range) match {
-                  case Some(names) =>
-                    if (names.no_completion) None
-                    else Some(names.range)
+                rendering.semantic_completion(range) match {
+                  case Some(semantic) =>
+                    if (semantic.info.no_completion) None
+                    else Some(semantic.range)
                   case None =>
                     syntax_completion(false, Some(rendering)) match {
                       case Some(result) => Some(result.range)
@@ -178,7 +178,7 @@
           val context =
             (opt_rendering orElse PIDE.document_view(text_area).map(_.get_rendering()) match {
               case Some(rendering) =>
-                rendering.completion_language(before_caret_range(rendering))
+                rendering.language_context(before_caret_range(rendering))
               case None => None
             }) getOrElse syntax.language_context
 
@@ -260,13 +260,14 @@
         PIDE.document_view(text_area) match {
           case Some(doc_view) =>
             val rendering = doc_view.get_rendering()
-            rendering.completion_names(before_caret_range(rendering)) match {
-              case Some(names) =>
-                if (names.no_completion)
-                  Some(Completion.Result.empty(names.range))
+            rendering.semantic_completion(before_caret_range(rendering)) match {
+              case Some(semantic) =>
+                if (semantic.info.no_completion)
+                  Some(Completion.Result.empty(semantic.range))
                 else
-                  JEdit_Lib.try_get_text(buffer, names.range) match {
-                    case Some(original) => names.complete(history, decode, original)
+                  JEdit_Lib.try_get_text(buffer, semantic.range) match {
+                    case Some(original) =>
+                      semantic.info.complete(semantic.range, history, decode, original)
                     case None => None
                   }
               case None => None
diff -r 31289387fdf8 -r 62f10624339a src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Mon Mar 17 11:39:46 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Mar 17 12:24:00 2014 +0100
@@ -128,10 +128,10 @@
 
   /* markup elements */
 
-  private val completion_names_elements =
+  private val semantic_completion_elements =
     Document.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
 
-  private val completion_language_elements =
+  private val language_context_elements =
     Document.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
       Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
       Markup.ML_STRING, Markup.ML_COMMENT)
@@ -258,18 +258,18 @@
 
   /* completion */
 
-  def completion_names(range: Text.Range): Option[Completion.Names] =
+  def semantic_completion(range: Text.Range): Option[Text.Info[Completion.Semantic]] =
     if (snapshot.is_outdated) None
     else {
-      snapshot.select(range, Rendering.completion_names_elements, _ =>
+      snapshot.select(range, Rendering.semantic_completion_elements, _ =>
         {
-          case Completion.Names.Info(names) => Some(names)
+          case Completion.Semantic.Info(info) => Some(info)
           case _ => None
         }).headOption.map(_.info)
     }
 
-  def completion_language(range: Text.Range): Option[Completion.Language_Context] =
-    snapshot.select(range, Rendering.completion_language_elements, _ =>
+  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))