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