# HG changeset patch
# User wenzelm
# Date 1393101506 -3600
# Node ID 8a213ab0e78a8165f453b091c82a0d5c1fb5b48c
# Parent  0286219c1261da85fe1be6263583c0db830c1fbc
support for semantic completion on Scala side;

diff -r 0286219c1261 -r 8a213ab0e78a src/Pure/General/completion.ML
--- a/src/Pure/General/completion.ML	Sat Feb 22 20:56:50 2014 +0100
+++ b/src/Pure/General/completion.ML	Sat Feb 22 21:38:26 2014 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/Isar/completion.ML
     Author:     Makarius
 
-Completion within the formal context.
+Semantic completion within the formal context.
 *)
 
 signature COMPLETION =
diff -r 0286219c1261 -r 8a213ab0e78a src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Sat Feb 22 20:56:50 2014 +0100
+++ b/src/Pure/General/completion.scala	Sat Feb 22 21:38:26 2014 +0100
@@ -1,7 +1,9 @@
 /*  Title:      Pure/General/completion.scala
     Author:     Makarius
 
-Completion of keywords and symbols, with abbreviations.
+Semantic completion within the formal context (reported by prover).
+Syntactic completion of keywords and symbols, with abbreviations
+(based on language context).
 */
 
 package isabelle
@@ -14,7 +16,38 @@
 
 object Completion
 {
-  /* context */
+  /** semantic completion **/
+
+  object Reported
+  {
+    object Elem
+    {
+      private def decode: XML.Decode.T[(String, List[String])] =
+      {
+        import XML.Decode._
+        pair(string, list(string))
+      }
+
+      def unapply(tree: XML.Tree): Option[Reported] =
+        tree match {
+          case XML.Elem(Markup(Markup.COMPLETION, _), body) =>
+            try {
+              val (original, replacements) = decode(body)
+              Some(Reported(original, replacements))
+            }
+            catch { case _: XML.Error => None }
+          case _ => None
+        }
+    }
+  }
+
+  sealed case class Reported(original: String, replacements: List[String])
+
+
+
+  /** syntactic completion **/
+
+  /* language context */
 
   object Context
   {
diff -r 0286219c1261 -r 8a213ab0e78a src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Sat Feb 22 20:56:50 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Sat Feb 22 21:38:26 2014 +0100
@@ -150,7 +150,9 @@
 
   /* markup elements */
 
-  private val completion_elements =
+  private val completion_reported_elements = Set(Markup.COMPLETION)
+
+  private val completion_context_elements =
     Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
       Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
       Markup.ML_STRING, Markup.ML_COMMENT)
@@ -269,12 +271,30 @@
   val dynamic_color = color_value("dynamic_color")
 
 
-  /* completion context */
+  /* completion */
+
+  def completion_reported(caret: Text.Offset): Option[Completion.Reported] =
+    if (caret > 0)
+    {
+      val result =
+        snapshot.select(Text.Range(caret - 1, caret + 1),
+          Rendering.completion_reported_elements, _ =>
+          {
+            case Text.Info(_, Completion.Reported.Elem(reported)) => Some(reported)
+            case _ => None
+          })
+      result match {
+        case Text.Info(_, reported) :: _ => Some(reported)
+        case Nil => None
+      }
+    }
+    else None
 
   def completion_context(caret: Text.Offset): Option[Completion.Context] =
     if (caret > 0) {
       val result =
-        snapshot.select(Text.Range(caret - 1, caret + 1), Rendering.completion_elements, _ =>
+        snapshot.select(Text.Range(caret - 1, caret + 1),
+          Rendering.completion_context_elements, _ =>
           {
             case Text.Info(_, elem)
             if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>