merge semantic and syntax completion;
authorwenzelm
Mon Mar 17 13:53:02 2014 +0100 (2014-03-17 ago)
changeset 5617579c29244b377
parent 56174 23ec13bb3db6
child 56176 0bc9b0ad6287
merge semantic and syntax completion;
tuned;
src/Pure/General/completion.scala
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/src/Pure/General/completion.scala	Mon Mar 17 12:58:44 2014 +0100
     1.2 +++ b/src/Pure/General/completion.scala	Mon Mar 17 13:53:02 2014 +0100
     1.3 @@ -30,6 +30,17 @@
     1.4    object Result
     1.5    {
     1.6      def empty(range: Text.Range): Result = Result(range, "", false, Nil)
     1.7 +    def merge(history: History, result1: Option[Result], result2: Option[Result]): Option[Result] =
     1.8 +      (result1, result2) match {
     1.9 +        case (_, None) => result1
    1.10 +        case (None, _) => result2
    1.11 +        case (Some(res1), Some(res2)) =>
    1.12 +          if (res1.range != res2.range || res1.original != res2.original) result1
    1.13 +          else {
    1.14 +            val items = (res1.items ::: res2.items).sorted(history.ordering)
    1.15 +            Some(Result(res1.range, res1.original, false, items))
    1.16 +          }
    1.17 +      }
    1.18    }
    1.19  
    1.20    sealed case class Result(
    1.21 @@ -144,23 +155,13 @@
    1.22    }
    1.23  
    1.24    sealed abstract class Semantic
    1.25 +  case object No_Completion extends Semantic
    1.26 +  case class Names(total: Int, names: List[(String, (String, String))]) extends Semantic
    1.27    {
    1.28 -    def no_completion: Boolean = this == No_Completion
    1.29      def complete(
    1.30        range: Text.Range,
    1.31        history: Completion.History,
    1.32        do_decode: Boolean,
    1.33 -      original: String): Option[Completion.Result] = None
    1.34 -  }
    1.35 -  case object No_Completion extends Semantic
    1.36 -  case class Names(
    1.37 -    total: Int,
    1.38 -    names: List[(String, (String, String))]) extends Semantic
    1.39 -  {
    1.40 -    override def complete(
    1.41 -      range: Text.Range,
    1.42 -      history: Completion.History,
    1.43 -      do_decode: Boolean,
    1.44        original: String): Option[Completion.Result] =
    1.45      {
    1.46        def decode(s: String): String = if (do_decode) Symbol.decode(s) else s
     2.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Mon Mar 17 12:58:44 2014 +0100
     2.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Mar 17 13:53:02 2014 +0100
     2.3 @@ -140,14 +140,10 @@
     2.4              before_caret_range(rendering).try_restrict(line_range) match {
     2.5                case Some(range) if !range.is_singularity =>
     2.6                  rendering.semantic_completion(range) match {
     2.7 -                  case Some(semantic) =>
     2.8 -                    if (semantic.info.no_completion) None
     2.9 -                    else Some(semantic.range)
    2.10 +                  case Some(Text.Info(_, Completion.No_Completion)) => None
    2.11 +                  case Some(Text.Info(range1, _: Completion.Names)) => Some(range1)
    2.12                    case None =>
    2.13 -                    syntax_completion(false, Some(rendering)) match {
    2.14 -                      case Some(result) => Some(result.range)
    2.15 -                      case None => None
    2.16 -                    }
    2.17 +                    syntax_completion(Completion.History.empty, false, Some(rendering)).map(_.range)
    2.18                  }
    2.19                case _ => None
    2.20              }
    2.21 @@ -160,10 +156,11 @@
    2.22      /* syntax completion */
    2.23  
    2.24      def syntax_completion(
    2.25 -      explicit: Boolean, opt_rendering: Option[Rendering] = None): Option[Completion.Result] =
    2.26 +      history: Completion.History,
    2.27 +      explicit: Boolean,
    2.28 +      opt_rendering: Option[Rendering]): Option[Completion.Result] =
    2.29      {
    2.30        val buffer = text_area.getBuffer
    2.31 -      val history = PIDE.completion_history.value
    2.32        val decode = Isabelle_Encoding.is_active(buffer)
    2.33  
    2.34        Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
    2.35 @@ -176,7 +173,7 @@
    2.36            val line_text = buffer.getSegment(line_start, line_length)
    2.37  
    2.38            val context =
    2.39 -            (opt_rendering orElse PIDE.document_view(text_area).map(_.get_rendering()) match {
    2.40 +            (opt_rendering match {
    2.41                case Some(rendering) =>
    2.42                  rendering.language_context(before_caret_range(rendering))
    2.43                case None => None
    2.44 @@ -256,36 +253,47 @@
    2.45          }
    2.46        }
    2.47  
    2.48 -      def semantic_completion(): Option[Completion.Result] =
    2.49 -        PIDE.document_view(text_area) match {
    2.50 -          case Some(doc_view) =>
    2.51 -            val rendering = doc_view.get_rendering()
    2.52 -            rendering.semantic_completion(before_caret_range(rendering)) match {
    2.53 -              case Some(semantic) =>
    2.54 -                if (semantic.info.no_completion)
    2.55 -                  Some(Completion.Result.empty(semantic.range))
    2.56 -                else
    2.57 -                  JEdit_Lib.try_get_text(buffer, semantic.range) match {
    2.58 -                    case Some(original) =>
    2.59 -                      semantic.info.complete(semantic.range, history, decode, original)
    2.60 -                    case None => None
    2.61 -                  }
    2.62 -              case None => None
    2.63 -            }
    2.64 -          case None => None
    2.65 +      if (buffer.isEditable) {
    2.66 +        val (no_completion, semantic_completion, opt_rendering) =
    2.67 +        {
    2.68 +          PIDE.document_view(text_area) match {
    2.69 +            case Some(doc_view) =>
    2.70 +              val rendering = doc_view.get_rendering()
    2.71 +              val (no_completion, result) =
    2.72 +                rendering.semantic_completion(before_caret_range(rendering)) match {
    2.73 +                  case Some(Text.Info(_, Completion.No_Completion)) =>
    2.74 +                    (true, None)
    2.75 +                  case Some(Text.Info(range, names: Completion.Names)) =>
    2.76 +                    val result =
    2.77 +                      JEdit_Lib.try_get_text(buffer, range) match {
    2.78 +                        case Some(original) => names.complete(range, history, decode, original)
    2.79 +                        case None => None
    2.80 +                      }
    2.81 +                    (false, result)
    2.82 +                  case None =>
    2.83 +                    (false, None)
    2.84 +                }
    2.85 +              (no_completion, result, Some(rendering))
    2.86 +            case None =>
    2.87 +              (false, None, None)
    2.88 +          }
    2.89          }
    2.90 +        if (!no_completion) {
    2.91 +          val result =
    2.92 +            Completion.Result.merge(history,
    2.93 +              semantic_completion, syntax_completion(history, explicit, opt_rendering))
    2.94  
    2.95 -      if (buffer.isEditable) {
    2.96 -        semantic_completion() orElse syntax_completion(explicit) match {
    2.97 -          case Some(result) =>
    2.98 -            result.items match {
    2.99 -              case List(item) if result.unique && item.immediate && immediate =>
   2.100 -                insert(item)
   2.101 -              case _ :: _ =>
   2.102 -                open_popup(result)
   2.103 -              case _ =>
   2.104 -            }
   2.105 -          case None =>
   2.106 +          result match {
   2.107 +            case Some(result) =>
   2.108 +              result.items match {
   2.109 +                case List(item) if result.unique && item.immediate && immediate =>
   2.110 +                  insert(item)
   2.111 +                case _ :: _ =>
   2.112 +                  open_popup(result)
   2.113 +                case _ =>
   2.114 +              }
   2.115 +            case None =>
   2.116 +          }
   2.117          }
   2.118        }
   2.119      }