more completion rendering: active, semantic, syntactic;
authorwenzelm
Tue Feb 25 20:15:47 2014 +0100 (2014-02-25)
changeset 55747bef19c929ba5
parent 55746 97f390fa0f3a
child 55748 2e1398b484aa
more completion rendering: active, semantic, syntactic;
tuned;
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/rendering.scala
src/Tools/jEdit/src/rich_text_area.scala
     1.1 --- a/src/Tools/jEdit/etc/options	Tue Feb 25 18:07:35 2014 +0100
     1.2 +++ b/src/Tools/jEdit/etc/options	Tue Feb 25 20:15:47 2014 +0100
     1.3 @@ -86,6 +86,7 @@
     1.4  option keyword2_color : string = "009966FF"
     1.5  option keyword3_color : string = "0099FFFF"
     1.6  option caret_invisible_color : string = "50000080"
     1.7 +option completion_color : string = "0000FFFF"
     1.8  
     1.9  option tfree_color : string = "A020F0FF"
    1.10  option tvar_color : string = "A020F0FF"
     2.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Tue Feb 25 18:07:35 2014 +0100
     2.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Feb 25 20:15:47 2014 +0100
     2.3 @@ -92,6 +92,65 @@
     2.4        }
     2.5  
     2.6  
     2.7 +    /* rendering */
     2.8 +
     2.9 +    def rendering(rendering: Rendering, line_range: Text.Range): Option[Text.Info[Color]] =
    2.10 +    {
    2.11 +      active_range match {
    2.12 +        case Some(range) => range.try_restrict(line_range)
    2.13 +        case None =>
    2.14 +          val buffer = text_area.getBuffer
    2.15 +          val caret = text_area.getCaretPosition
    2.16 +
    2.17 +          if (line_range.contains(caret)) {
    2.18 +            JEdit_Lib.stretch_point_range(buffer, caret).try_restrict(line_range) match {
    2.19 +              case Some(range) if !range.is_singularity =>
    2.20 +                rendering.completion_names(range) match {
    2.21 +                  case Some(names) => Some(names.range)
    2.22 +                  case None =>
    2.23 +                    syntax_completion(Some(rendering), false) match {
    2.24 +                      case Some(result) => Some(result.range)
    2.25 +                      case None => None
    2.26 +                    }
    2.27 +                }
    2.28 +              case _ => None
    2.29 +            }
    2.30 +          }
    2.31 +          else None
    2.32 +      }
    2.33 +    }.map(range => Text.Info(range, rendering.completion_color))
    2.34 +
    2.35 +
    2.36 +    /* syntax completion */
    2.37 +
    2.38 +    def syntax_completion(
    2.39 +      opt_rendering: Option[Rendering], explicit: Boolean): Option[Completion.Result] =
    2.40 +    {
    2.41 +      val buffer = text_area.getBuffer
    2.42 +      val history = PIDE.completion_history.value
    2.43 +      val decode = Isabelle_Encoding.is_active(buffer)
    2.44 +
    2.45 +      Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
    2.46 +        case Some(syntax) =>
    2.47 +          val caret = text_area.getCaretPosition
    2.48 +          val line = buffer.getLineOfOffset(caret)
    2.49 +          val start = buffer.getLineStartOffset(line)
    2.50 +          val text = buffer.getSegment(start, caret - start)
    2.51 +
    2.52 +          val context =
    2.53 +            (opt_rendering orElse PIDE.document_view(text_area).map(_.get_rendering()) match {
    2.54 +              case Some(rendering) =>
    2.55 +                rendering.completion_context(JEdit_Lib.stretch_point_range(buffer, caret))
    2.56 +              case None => None
    2.57 +            }) getOrElse syntax.completion_context
    2.58 +
    2.59 +          syntax.completion.complete(history, decode, explicit, start, text, context)
    2.60 +
    2.61 +        case None => None
    2.62 +      }
    2.63 +    }
    2.64 +
    2.65 +
    2.66      /* completion action */
    2.67  
    2.68      private def insert(item: Completion.Item)
    2.69 @@ -179,41 +238,20 @@
    2.70            }
    2.71          }
    2.72  
    2.73 -      def syntax_completion(): Boolean =
    2.74 -      {
    2.75 -        Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
    2.76 -          case Some(syntax) =>
    2.77 -            val line = buffer.getLineOfOffset(caret)
    2.78 -            val start = buffer.getLineStartOffset(line)
    2.79 -            val text = buffer.getSegment(start, caret - start)
    2.80 -
    2.81 -            val context =
    2.82 -              (PIDE.document_view(text_area) match {
    2.83 -                case None => None
    2.84 -                case Some(doc_view) =>
    2.85 -                  val rendering = doc_view.get_rendering()
    2.86 -                  rendering.completion_context(JEdit_Lib.stretch_point_range(buffer, caret))
    2.87 -              }) getOrElse syntax.completion_context
    2.88 -
    2.89 -            syntax.completion.complete(history, decode, explicit, start, text, context) match {
    2.90 -              case Some(result) =>
    2.91 -                result.items match {
    2.92 -                  case List(item) if result.unique && item.immediate && immediate =>
    2.93 -                    insert(item)
    2.94 -                    true
    2.95 -                  case _ :: _ =>
    2.96 -                    open_popup(result)
    2.97 -                    true
    2.98 -                  case _ => false
    2.99 -                }
   2.100 -              case None => false
   2.101 +      def syntactic_completion(): Boolean =
   2.102 +        syntax_completion(None, explicit) match {
   2.103 +          case Some(result) =>
   2.104 +            result.items match {
   2.105 +              case List(item) if result.unique && item.immediate && immediate =>
   2.106 +                insert(item); true
   2.107 +              case _ :: _ => open_popup(result); true
   2.108 +              case _ => false
   2.109              }
   2.110            case None => false
   2.111          }
   2.112 -      }
   2.113  
   2.114        if (buffer.isEditable)
   2.115 -        semantic_completion() || syntax_completion()
   2.116 +        semantic_completion() || syntactic_completion()
   2.117      }
   2.118  
   2.119  
     3.1 --- a/src/Tools/jEdit/src/rendering.scala	Tue Feb 25 18:07:35 2014 +0100
     3.2 +++ b/src/Tools/jEdit/src/rendering.scala	Tue Feb 25 20:15:47 2014 +0100
     3.3 @@ -261,6 +261,7 @@
     3.4    val keyword2_color = color_value("keyword2_color")
     3.5    val keyword3_color = color_value("keyword3_color")
     3.6    val caret_invisible_color = color_value("caret_invisible_color")
     3.7 +  val completion_color = color_value("completion_color")
     3.8  
     3.9    val tfree_color = color_value("tfree_color")
    3.10    val tvar_color = color_value("tvar_color")
     4.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Tue Feb 25 18:07:35 2014 +0100
     4.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Tue Feb 25 20:15:47 2014 +0100
     4.3 @@ -222,23 +222,6 @@
     4.4    }
     4.5  
     4.6  
     4.7 -  /* caret */
     4.8 -
     4.9 -  private def get_caret_range(stretch: Boolean): Text.Range =
    4.10 -    if (caret_visible) {
    4.11 -      val caret = text_area.getCaretPosition
    4.12 -      if (stretch) JEdit_Lib.stretch_point_range(buffer, caret)
    4.13 -      else JEdit_Lib.point_range(buffer, caret)
    4.14 -    }
    4.15 -    else Text.Range(-1)
    4.16 -
    4.17 -  private def get_caret_color(rendering: Rendering): Color =
    4.18 -  {
    4.19 -    if (text_area.isCaretVisible) text_area.getPainter.getCaretColor
    4.20 -    else rendering.caret_invisible_color
    4.21 -  }
    4.22 -
    4.23 -
    4.24    /* text background */
    4.25  
    4.26    private val background_painter = new TextAreaExtension
    4.27 @@ -312,13 +295,23 @@
    4.28  
    4.29    /* text */
    4.30  
    4.31 +  private def caret_color(rendering: Rendering): Color =
    4.32 +  {
    4.33 +    if (text_area.isCaretVisible)
    4.34 +      text_area.getPainter.getCaretColor
    4.35 +    else rendering.caret_invisible_color
    4.36 +  }
    4.37 +
    4.38    private def paint_chunk_list(rendering: Rendering,
    4.39      gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
    4.40    {
    4.41      val clip_rect = gfx.getClipBounds
    4.42      val painter = text_area.getPainter
    4.43      val font_context = painter.getFontRenderContext
    4.44 -    val caret_range = get_caret_range(false)
    4.45 +
    4.46 +    val caret_range =
    4.47 +      if (caret_visible) JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
    4.48 +      else Text.Range(-1)
    4.49  
    4.50      var w = 0.0f
    4.51      var chunk = head
    4.52 @@ -369,7 +362,7 @@
    4.53  
    4.54                val astr = new AttributedString(s2)
    4.55                astr.addAttribute(TextAttribute.FONT, chunk_font)
    4.56 -              astr.addAttribute(TextAttribute.FOREGROUND, get_caret_color(rendering))
    4.57 +              astr.addAttribute(TextAttribute.FOREGROUND, caret_color(rendering))
    4.58                astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
    4.59                gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
    4.60  
    4.61 @@ -455,9 +448,6 @@
    4.62        start: Array[Int], end: Array[Int], y: Int, line_height: Int)
    4.63      {
    4.64        robust_rendering { rendering =>
    4.65 -        val caret_range = get_caret_range(true)
    4.66 -        val caret_color = text_area.getPainter.getCaretColor
    4.67 -
    4.68          for (i <- 0 until physical_lines.length) {
    4.69            if (physical_lines(i) != -1) {
    4.70              val line_range = Text.Range(start(i), end(i))
    4.71 @@ -492,21 +482,14 @@
    4.72              }
    4.73  
    4.74              // completion range
    4.75 -            if (!hyperlink_area.is_active) {
    4.76 -              def paint_completion(range: Text.Range) {
    4.77 -                for (r <- JEdit_Lib.gfx_range(text_area, range)) {
    4.78 -                  gfx.setColor(caret_color)
    4.79 -                  gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
    4.80 -                }
    4.81 -              }
    4.82 -              Completion_Popup.Text_Area.active_range(text_area) match {
    4.83 -                case Some(range) if range.try_restrict(line_range).isDefined =>
    4.84 -                  paint_completion(range.try_restrict(line_range).get)
    4.85 -                case _ =>
    4.86 -                  for {
    4.87 -                    caret <- caret_range.try_restrict(line_range)
    4.88 -                    names <- rendering.completion_names(caret)
    4.89 -                  } paint_completion(names.range)
    4.90 +            if (!hyperlink_area.is_active && caret_visible) {
    4.91 +              for {
    4.92 +                completion <- Completion_Popup.Text_Area(text_area)
    4.93 +                Text.Info(range, color) <- completion.rendering(rendering, line_range)
    4.94 +                r <- JEdit_Lib.gfx_range(text_area, range)
    4.95 +              } {
    4.96 +                gfx.setColor(color)
    4.97 +                gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
    4.98                }
    4.99              }
   4.100            }
   4.101 @@ -550,7 +533,7 @@
   4.102  
   4.103              val offset = caret - text_area.getLineStartOffset(physical_line)
   4.104              val x = text_area.offsetToXY(physical_line, offset).x
   4.105 -            gfx.setColor(get_caret_color(rendering))
   4.106 +            gfx.setColor(caret_color(rendering))
   4.107              gfx.drawRect(x, y, (metric.unit * metric.average).round.toInt - 1, fm.getHeight - 1)
   4.108            }
   4.109          }