tuned signature;
authorwenzelm
Thu Aug 29 13:00:59 2013 +0200 (2013-08-29 ago)
changeset 53275b34aac6511ab
parent 53274 1760c01f1c78
child 53276 cbed0aa0b0db
tuned signature;
src/Pure/Thy/completion.scala
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/src/Pure/Thy/completion.scala	Thu Aug 29 12:38:33 2013 +0200
     1.2 +++ b/src/Pure/Thy/completion.scala	Thu Aug 29 13:00:59 2013 +0200
     1.3 @@ -6,12 +6,19 @@
     1.4  
     1.5  package isabelle
     1.6  
     1.7 -import scala.util.matching.Regex
     1.8  import scala.util.parsing.combinator.RegexParsers
     1.9  
    1.10  
    1.11  object Completion
    1.12  {
    1.13 +  /* items */
    1.14 +
    1.15 +  sealed case class Item(original: String, replacement: String, description: String)
    1.16 +  { override def toString: String = description }
    1.17 +
    1.18 +
    1.19 +  /* init */
    1.20 +
    1.21    val empty: Completion = new Completion()
    1.22    def init(): Completion = empty.add_symbols()
    1.23  
    1.24 @@ -79,21 +86,29 @@
    1.25  
    1.26    /* complete */
    1.27  
    1.28 -  def complete(line: CharSequence): Option[(String, List[String])] =
    1.29 +  def complete(decode: Boolean, line: CharSequence): Option[(String, List[Completion.Item])] =
    1.30    {
    1.31 -    abbrevs_lex.parse(abbrevs_lex.keyword, new Library.Reverse(line)) match {
    1.32 -      case abbrevs_lex.Success(reverse_a, _) =>
    1.33 -        val (word, c) = abbrevs_map(reverse_a)
    1.34 -        Some(word, List(c))
    1.35 -      case _ =>
    1.36 -        Completion.Parse.read(line) match {
    1.37 -          case Some(word) =>
    1.38 -            words_lex.completions(word).map(words_map(_)) match {
    1.39 -              case Nil => None
    1.40 -              case cs => Some(word, cs.sorted)
    1.41 -            }
    1.42 -          case None => None
    1.43 -        }
    1.44 +    val raw_result =
    1.45 +      abbrevs_lex.parse(abbrevs_lex.keyword, new Library.Reverse(line)) match {
    1.46 +        case abbrevs_lex.Success(reverse_a, _) =>
    1.47 +          val (word, c) = abbrevs_map(reverse_a)
    1.48 +          Some(word, List(c))
    1.49 +        case _ =>
    1.50 +          Completion.Parse.read(line) match {
    1.51 +            case Some(word) =>
    1.52 +              words_lex.completions(word).map(words_map(_)) match {
    1.53 +                case Nil => None
    1.54 +                case cs => Some(word, cs.sorted)
    1.55 +              }
    1.56 +            case None => None
    1.57 +          }
    1.58 +      }
    1.59 +    raw_result match {
    1.60 +      case Some((word, cs)) =>
    1.61 +        val ds = (if (decode) cs.map(Symbol.decode(_)).sorted else cs).filter(_ != word)
    1.62 +        if (ds.isEmpty) None
    1.63 +        else Some((word, ds.map(s => Completion.Item(word, s, s))))
    1.64 +      case None => None
    1.65      }
    1.66    }
    1.67  }
     2.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 12:38:33 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 13:00:59 2013 +0200
     2.3 @@ -22,12 +22,6 @@
     2.4  
     2.5  object Completion_Popup
     2.6  {
     2.7 -  /* items */
     2.8 -
     2.9 -  private sealed case class Item(original: String, replacement: String, description: String)
    2.10 -  { override def toString: String = description }
    2.11 -
    2.12 -
    2.13    /* setup for jEdit text area */
    2.14  
    2.15    object Text_Area
    2.16 @@ -93,7 +87,7 @@
    2.17  
    2.18      /* insert selected item */
    2.19  
    2.20 -    private def insert(item: Item)
    2.21 +    private def insert(item: Completion.Item)
    2.22      {
    2.23        Swing_Thread.require()
    2.24  
    2.25 @@ -143,24 +137,11 @@
    2.26            Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
    2.27              case Some(syntax) =>
    2.28                val caret = text_area.getCaretPosition
    2.29 -              val result =
    2.30 -              {
    2.31 -                val line = buffer.getLineOfOffset(caret)
    2.32 -                val start = buffer.getLineStartOffset(line)
    2.33 -                val text = buffer.getSegment(start, caret - start)
    2.34 +              val line = buffer.getLineOfOffset(caret)
    2.35 +              val start = buffer.getLineStartOffset(line)
    2.36 +              val text = buffer.getSegment(start, caret - start)
    2.37  
    2.38 -                syntax.completion.complete(text) match {
    2.39 -                  case Some((word, cs)) =>
    2.40 -                    val ds =
    2.41 -                      (if (Isabelle_Encoding.is_active(buffer))
    2.42 -                        cs.map(Symbol.decode(_)).sorted
    2.43 -                       else cs).filter(_ != word)
    2.44 -                    if (ds.isEmpty) None
    2.45 -                    else Some((word, ds.map(s => Item(word, s, s))))
    2.46 -                  case None => None
    2.47 -                }
    2.48 -              }
    2.49 -              result match {
    2.50 +              syntax.completion.complete(Isabelle_Encoding.is_active(buffer), text) match {
    2.51                  case Some((original, items)) =>
    2.52                    val font =
    2.53                      painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
    2.54 @@ -173,10 +154,10 @@
    2.55  
    2.56                      val completion =
    2.57                        new Completion_Popup(layered, loc2, font, items) {
    2.58 -                        override def complete(item: Item) { insert(item) }
    2.59 -                        override def propagate(e: KeyEvent) {
    2.60 -                          JEdit_Lib.propagate_key(view, e)
    2.61 -                          input(e)
    2.62 +                        override def complete(item: Completion.Item) { insert(item) }
    2.63 +                        override def propagate(evt: KeyEvent) {
    2.64 +                          JEdit_Lib.propagate_key(view, evt)
    2.65 +                          input(evt)
    2.66                          }
    2.67                          override def refocus() { text_area.requestFocus }
    2.68                        }
    2.69 @@ -214,7 +195,7 @@
    2.70    layered: JLayeredPane,
    2.71    location: Point,
    2.72    font: Font,
    2.73 -  items: List[Completion_Popup.Item]) extends JPanel(new BorderLayout)
    2.74 +  items: List[Completion.Item]) extends JPanel(new BorderLayout)
    2.75  {
    2.76    completion =>
    2.77  
    2.78 @@ -224,7 +205,7 @@
    2.79  
    2.80    /* actions */
    2.81  
    2.82 -  def complete(item: Completion_Popup.Item) { }
    2.83 +  def complete(item: Completion.Item) { }
    2.84    def propagate(evt: KeyEvent) { }
    2.85    def refocus() { }
    2.86