src/Tools/jEdit/src/completion_popup.scala
changeset 55615 bf4bbe72f740
parent 54377 750561986828
child 55616 25a7a998852a
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Wed Feb 19 21:38:44 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Feb 20 12:53:12 2014 +0100
     1.3 @@ -110,7 +110,12 @@
     1.4  
     1.5              val history = PIDE.completion_history.value
     1.6              val decode = Isabelle_Encoding.is_active(buffer)
     1.7 -            syntax.completion.complete(history, decode, explicit, text) match {
     1.8 +            val context =
     1.9 +              PIDE.document_view(text_area) match {
    1.10 +                case None => Completion.Context.default
    1.11 +                case Some(doc_view) => doc_view.get_rendering().completion_context(caret)
    1.12 +              }
    1.13 +            syntax.completion.complete(history, decode, explicit, text, context) match {
    1.14                case Some(result) =>
    1.15                  if (result.unique && result.items.head.immediate && immediate)
    1.16                    insert(result.items.head)
    1.17 @@ -277,7 +282,8 @@
    1.18            val caret = text_field.getCaret.getDot
    1.19            val text = text_field.getText.substring(0, caret)
    1.20  
    1.21 -          syntax.completion.complete(history, decode = true, explicit = false, text) match {
    1.22 +          syntax.completion.complete(
    1.23 +              history, decode = true, explicit = false, text, Completion.Context.default) match {
    1.24              case Some(result) =>
    1.25                val fm = text_field.getFontMetrics(text_field.getFont)
    1.26                val loc =