tuned signature;
authorwenzelm
Mon Mar 17 12:24:00 2014 +0100 (2014-03-17 ago)
changeset 5617362f10624339a
parent 56172 31289387fdf8
child 56174 23ec13bb3db6
tuned signature;
src/Pure/General/completion.scala
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/General/completion.scala	Mon Mar 17 11:39:46 2014 +0100
     1.2 +++ b/src/Pure/General/completion.scala	Mon Mar 17 12:24:00 2014 +0100
     1.3 @@ -131,11 +131,11 @@
     1.4  
     1.5    /** semantic completion **/
     1.6  
     1.7 -  object Names
     1.8 +  object Semantic
     1.9    {
    1.10      object Info
    1.11      {
    1.12 -      def unapply(info: Text.Markup): Option[Names] =
    1.13 +      def unapply(info: Text.Markup): Option[Text.Info[Semantic]] =
    1.14          info.info match {
    1.15            case XML.Elem(Markup(Markup.COMPLETION, _), body) =>
    1.16              try {
    1.17 @@ -144,22 +144,32 @@
    1.18                  import XML.Decode._
    1.19                  pair(int, list(pair(string, pair(string, string))))(body)
    1.20                }
    1.21 -              Some(Names(info.range, total, names))
    1.22 +              Some(Text.Info(info.range, Names(total, names)))
    1.23              }
    1.24              catch { case _: XML.Error => None }
    1.25            case XML.Elem(Markup(Markup.NO_COMPLETION, _), _) =>
    1.26 -            Some(Names(info.range, 0, Nil))
    1.27 +            Some(Text.Info(info.range, No_Completion))
    1.28            case _ => None
    1.29          }
    1.30      }
    1.31    }
    1.32  
    1.33 -  sealed case class Names(
    1.34 -    range: Text.Range, total: Int, names: List[(String, (String, String))])
    1.35 +  sealed abstract class Semantic
    1.36    {
    1.37 -    def no_completion: Boolean = total == 0 && names.isEmpty
    1.38 -
    1.39 +    def no_completion: Boolean = this == No_Completion
    1.40      def complete(
    1.41 +      range: Text.Range,
    1.42 +      history: Completion.History,
    1.43 +      do_decode: Boolean,
    1.44 +      original: String): Option[Completion.Result] = None
    1.45 +  }
    1.46 +  case object No_Completion extends Semantic
    1.47 +  case class Names(
    1.48 +    total: Int,
    1.49 +    names: List[(String, (String, String))]) extends Semantic
    1.50 +  {
    1.51 +    override def complete(
    1.52 +      range: Text.Range,
    1.53        history: Completion.History,
    1.54        do_decode: Boolean,
    1.55        original: String): Option[Completion.Result] =
     2.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Mon Mar 17 11:39:46 2014 +0100
     2.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Mar 17 12:24:00 2014 +0100
     2.3 @@ -139,10 +139,10 @@
     2.4            if (line_range.contains(text_area.getCaretPosition)) {
     2.5              before_caret_range(rendering).try_restrict(line_range) match {
     2.6                case Some(range) if !range.is_singularity =>
     2.7 -                rendering.completion_names(range) match {
     2.8 -                  case Some(names) =>
     2.9 -                    if (names.no_completion) None
    2.10 -                    else Some(names.range)
    2.11 +                rendering.semantic_completion(range) match {
    2.12 +                  case Some(semantic) =>
    2.13 +                    if (semantic.info.no_completion) None
    2.14 +                    else Some(semantic.range)
    2.15                    case None =>
    2.16                      syntax_completion(false, Some(rendering)) match {
    2.17                        case Some(result) => Some(result.range)
    2.18 @@ -178,7 +178,7 @@
    2.19            val context =
    2.20              (opt_rendering orElse PIDE.document_view(text_area).map(_.get_rendering()) match {
    2.21                case Some(rendering) =>
    2.22 -                rendering.completion_language(before_caret_range(rendering))
    2.23 +                rendering.language_context(before_caret_range(rendering))
    2.24                case None => None
    2.25              }) getOrElse syntax.language_context
    2.26  
    2.27 @@ -260,13 +260,14 @@
    2.28          PIDE.document_view(text_area) match {
    2.29            case Some(doc_view) =>
    2.30              val rendering = doc_view.get_rendering()
    2.31 -            rendering.completion_names(before_caret_range(rendering)) match {
    2.32 -              case Some(names) =>
    2.33 -                if (names.no_completion)
    2.34 -                  Some(Completion.Result.empty(names.range))
    2.35 +            rendering.semantic_completion(before_caret_range(rendering)) match {
    2.36 +              case Some(semantic) =>
    2.37 +                if (semantic.info.no_completion)
    2.38 +                  Some(Completion.Result.empty(semantic.range))
    2.39                  else
    2.40 -                  JEdit_Lib.try_get_text(buffer, names.range) match {
    2.41 -                    case Some(original) => names.complete(history, decode, original)
    2.42 +                  JEdit_Lib.try_get_text(buffer, semantic.range) match {
    2.43 +                    case Some(original) =>
    2.44 +                      semantic.info.complete(semantic.range, history, decode, original)
    2.45                      case None => None
    2.46                    }
    2.47                case None => None
     3.1 --- a/src/Tools/jEdit/src/rendering.scala	Mon Mar 17 11:39:46 2014 +0100
     3.2 +++ b/src/Tools/jEdit/src/rendering.scala	Mon Mar 17 12:24:00 2014 +0100
     3.3 @@ -128,10 +128,10 @@
     3.4  
     3.5    /* markup elements */
     3.6  
     3.7 -  private val completion_names_elements =
     3.8 +  private val semantic_completion_elements =
     3.9      Document.Elements(Markup.COMPLETION, Markup.NO_COMPLETION)
    3.10  
    3.11 -  private val completion_language_elements =
    3.12 +  private val language_context_elements =
    3.13      Document.Elements(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
    3.14        Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
    3.15        Markup.ML_STRING, Markup.ML_COMMENT)
    3.16 @@ -258,18 +258,18 @@
    3.17  
    3.18    /* completion */
    3.19  
    3.20 -  def completion_names(range: Text.Range): Option[Completion.Names] =
    3.21 +  def semantic_completion(range: Text.Range): Option[Text.Info[Completion.Semantic]] =
    3.22      if (snapshot.is_outdated) None
    3.23      else {
    3.24 -      snapshot.select(range, Rendering.completion_names_elements, _ =>
    3.25 +      snapshot.select(range, Rendering.semantic_completion_elements, _ =>
    3.26          {
    3.27 -          case Completion.Names.Info(names) => Some(names)
    3.28 +          case Completion.Semantic.Info(info) => Some(info)
    3.29            case _ => None
    3.30          }).headOption.map(_.info)
    3.31      }
    3.32  
    3.33 -  def completion_language(range: Text.Range): Option[Completion.Language_Context] =
    3.34 -    snapshot.select(range, Rendering.completion_language_elements, _ =>
    3.35 +  def language_context(range: Text.Range): Option[Completion.Language_Context] =
    3.36 +    snapshot.select(range, Rendering.language_context_elements, _ =>
    3.37        {
    3.38          case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes, delimited), _)) =>
    3.39            if (delimited) Some(Completion.Language_Context(language, symbols, antiquotes))