# HG changeset patch
# User wenzelm
# Date 1377774059 -7200
# Node ID b34aac6511aba83af9bcf3001c15adee0f0f5c38
# Parent  1760c01f1c7894f542e40825c790d88655fe6318
tuned signature;

diff -r 1760c01f1c78 -r b34aac6511ab src/Pure/Thy/completion.scala
--- a/src/Pure/Thy/completion.scala	Thu Aug 29 12:38:33 2013 +0200
+++ b/src/Pure/Thy/completion.scala	Thu Aug 29 13:00:59 2013 +0200
@@ -6,12 +6,19 @@
 
 package isabelle
 
-import scala.util.matching.Regex
 import scala.util.parsing.combinator.RegexParsers
 
 
 object Completion
 {
+  /* items */
+
+  sealed case class Item(original: String, replacement: String, description: String)
+  { override def toString: String = description }
+
+
+  /* init */
+
   val empty: Completion = new Completion()
   def init(): Completion = empty.add_symbols()
 
@@ -79,21 +86,29 @@
 
   /* complete */
 
-  def complete(line: CharSequence): Option[(String, List[String])] =
+  def complete(decode: Boolean, line: CharSequence): Option[(String, List[Completion.Item])] =
   {
-    abbrevs_lex.parse(abbrevs_lex.keyword, new Library.Reverse(line)) match {
-      case abbrevs_lex.Success(reverse_a, _) =>
-        val (word, c) = abbrevs_map(reverse_a)
-        Some(word, List(c))
-      case _ =>
-        Completion.Parse.read(line) match {
-          case Some(word) =>
-            words_lex.completions(word).map(words_map(_)) match {
-              case Nil => None
-              case cs => Some(word, cs.sorted)
-            }
-          case None => None
-        }
+    val raw_result =
+      abbrevs_lex.parse(abbrevs_lex.keyword, new Library.Reverse(line)) match {
+        case abbrevs_lex.Success(reverse_a, _) =>
+          val (word, c) = abbrevs_map(reverse_a)
+          Some(word, List(c))
+        case _ =>
+          Completion.Parse.read(line) match {
+            case Some(word) =>
+              words_lex.completions(word).map(words_map(_)) match {
+                case Nil => None
+                case cs => Some(word, cs.sorted)
+              }
+            case None => None
+          }
+      }
+    raw_result match {
+      case Some((word, cs)) =>
+        val ds = (if (decode) cs.map(Symbol.decode(_)).sorted else cs).filter(_ != word)
+        if (ds.isEmpty) None
+        else Some((word, ds.map(s => Completion.Item(word, s, s))))
+      case None => None
     }
   }
 }
diff -r 1760c01f1c78 -r b34aac6511ab src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 12:38:33 2013 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 13:00:59 2013 +0200
@@ -22,12 +22,6 @@
 
 object Completion_Popup
 {
-  /* items */
-
-  private sealed case class Item(original: String, replacement: String, description: String)
-  { override def toString: String = description }
-
-
   /* setup for jEdit text area */
 
   object Text_Area
@@ -93,7 +87,7 @@
 
     /* insert selected item */
 
-    private def insert(item: Item)
+    private def insert(item: Completion.Item)
     {
       Swing_Thread.require()
 
@@ -143,24 +137,11 @@
           Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
             case Some(syntax) =>
               val caret = text_area.getCaretPosition
-              val result =
-              {
-                val line = buffer.getLineOfOffset(caret)
-                val start = buffer.getLineStartOffset(line)
-                val text = buffer.getSegment(start, caret - start)
+              val line = buffer.getLineOfOffset(caret)
+              val start = buffer.getLineStartOffset(line)
+              val text = buffer.getSegment(start, caret - start)
 
-                syntax.completion.complete(text) match {
-                  case Some((word, cs)) =>
-                    val ds =
-                      (if (Isabelle_Encoding.is_active(buffer))
-                        cs.map(Symbol.decode(_)).sorted
-                       else cs).filter(_ != word)
-                    if (ds.isEmpty) None
-                    else Some((word, ds.map(s => Item(word, s, s))))
-                  case None => None
-                }
-              }
-              result match {
+              syntax.completion.complete(Isabelle_Encoding.is_active(buffer), text) match {
                 case Some((original, items)) =>
                   val font =
                     painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
@@ -173,10 +154,10 @@
 
                     val completion =
                       new Completion_Popup(layered, loc2, font, items) {
-                        override def complete(item: Item) { insert(item) }
-                        override def propagate(e: KeyEvent) {
-                          JEdit_Lib.propagate_key(view, e)
-                          input(e)
+                        override def complete(item: Completion.Item) { insert(item) }
+                        override def propagate(evt: KeyEvent) {
+                          JEdit_Lib.propagate_key(view, evt)
+                          input(evt)
                         }
                         override def refocus() { text_area.requestFocus }
                       }
@@ -214,7 +195,7 @@
   layered: JLayeredPane,
   location: Point,
   font: Font,
-  items: List[Completion_Popup.Item]) extends JPanel(new BorderLayout)
+  items: List[Completion.Item]) extends JPanel(new BorderLayout)
 {
   completion =>
 
@@ -224,7 +205,7 @@
 
   /* actions */
 
-  def complete(item: Completion_Popup.Item) { }
+  def complete(item: Completion.Item) { }
   def propagate(evt: KeyEvent) { }
   def refocus() { }