support for semantic completion on Scala side;
authorwenzelm
Sat Feb 22 21:38:26 2014 +0100 (2014-02-22 ago)
changeset 556748a213ab0e78a
parent 55673 0286219c1261
child 55675 ccbf1722ae32
support for semantic completion on Scala side;
src/Pure/General/completion.ML
src/Pure/General/completion.scala
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/General/completion.ML	Sat Feb 22 20:56:50 2014 +0100
     1.2 +++ b/src/Pure/General/completion.ML	Sat Feb 22 21:38:26 2014 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      Pure/Isar/completion.ML
     1.5      Author:     Makarius
     1.6  
     1.7 -Completion within the formal context.
     1.8 +Semantic completion within the formal context.
     1.9  *)
    1.10  
    1.11  signature COMPLETION =
     2.1 --- a/src/Pure/General/completion.scala	Sat Feb 22 20:56:50 2014 +0100
     2.2 +++ b/src/Pure/General/completion.scala	Sat Feb 22 21:38:26 2014 +0100
     2.3 @@ -1,7 +1,9 @@
     2.4  /*  Title:      Pure/General/completion.scala
     2.5      Author:     Makarius
     2.6  
     2.7 -Completion of keywords and symbols, with abbreviations.
     2.8 +Semantic completion within the formal context (reported by prover).
     2.9 +Syntactic completion of keywords and symbols, with abbreviations
    2.10 +(based on language context).
    2.11  */
    2.12  
    2.13  package isabelle
    2.14 @@ -14,7 +16,38 @@
    2.15  
    2.16  object Completion
    2.17  {
    2.18 -  /* context */
    2.19 +  /** semantic completion **/
    2.20 +
    2.21 +  object Reported
    2.22 +  {
    2.23 +    object Elem
    2.24 +    {
    2.25 +      private def decode: XML.Decode.T[(String, List[String])] =
    2.26 +      {
    2.27 +        import XML.Decode._
    2.28 +        pair(string, list(string))
    2.29 +      }
    2.30 +
    2.31 +      def unapply(tree: XML.Tree): Option[Reported] =
    2.32 +        tree match {
    2.33 +          case XML.Elem(Markup(Markup.COMPLETION, _), body) =>
    2.34 +            try {
    2.35 +              val (original, replacements) = decode(body)
    2.36 +              Some(Reported(original, replacements))
    2.37 +            }
    2.38 +            catch { case _: XML.Error => None }
    2.39 +          case _ => None
    2.40 +        }
    2.41 +    }
    2.42 +  }
    2.43 +
    2.44 +  sealed case class Reported(original: String, replacements: List[String])
    2.45 +
    2.46 +
    2.47 +
    2.48 +  /** syntactic completion **/
    2.49 +
    2.50 +  /* language context */
    2.51  
    2.52    object Context
    2.53    {
     3.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Feb 22 20:56:50 2014 +0100
     3.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Feb 22 21:38:26 2014 +0100
     3.3 @@ -150,7 +150,9 @@
     3.4  
     3.5    /* markup elements */
     3.6  
     3.7 -  private val completion_elements =
     3.8 +  private val completion_reported_elements = Set(Markup.COMPLETION)
     3.9 +
    3.10 +  private val completion_context_elements =
    3.11      Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM,
    3.12        Markup.CARTOUCHE, Markup.COMMENT, Markup.LANGUAGE,
    3.13        Markup.ML_STRING, Markup.ML_COMMENT)
    3.14 @@ -269,12 +271,30 @@
    3.15    val dynamic_color = color_value("dynamic_color")
    3.16  
    3.17  
    3.18 -  /* completion context */
    3.19 +  /* completion */
    3.20 +
    3.21 +  def completion_reported(caret: Text.Offset): Option[Completion.Reported] =
    3.22 +    if (caret > 0)
    3.23 +    {
    3.24 +      val result =
    3.25 +        snapshot.select(Text.Range(caret - 1, caret + 1),
    3.26 +          Rendering.completion_reported_elements, _ =>
    3.27 +          {
    3.28 +            case Text.Info(_, Completion.Reported.Elem(reported)) => Some(reported)
    3.29 +            case _ => None
    3.30 +          })
    3.31 +      result match {
    3.32 +        case Text.Info(_, reported) :: _ => Some(reported)
    3.33 +        case Nil => None
    3.34 +      }
    3.35 +    }
    3.36 +    else None
    3.37  
    3.38    def completion_context(caret: Text.Offset): Option[Completion.Context] =
    3.39      if (caret > 0) {
    3.40        val result =
    3.41 -        snapshot.select(Text.Range(caret - 1, caret + 1), Rendering.completion_elements, _ =>
    3.42 +        snapshot.select(Text.Range(caret - 1, caret + 1),
    3.43 +          Rendering.completion_context_elements, _ =>
    3.44            {
    3.45              case Text.Info(_, elem)
    3.46              if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>