--- 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 =
--- 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
{
--- 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 =>