1.1 --- a/src/Pure/Isar/completion.scala	Wed Feb 19 21:38:44 2014 +0100
     1.2 +++ b/src/Pure/Isar/completion.scala	Thu Feb 20 12:53:12 2014 +0100
     1.3 @@ -13,6 +13,19 @@
     1.4  
     1.5  object Completion
     1.6  {
     1.7 +  /* context */
     1.8 +
     1.9 +  object Context
    1.10 +  {
    1.11 +    val default = Context("", true)
    1.12 +  }
    1.13 +
    1.14 +  sealed case class Context(language: String, symbols: Boolean)
    1.15 +  {
    1.16 +    def is_outer: Boolean = language == ""
    1.17 +  }
    1.18 +
    1.19 +
    1.20    /* result */
    1.21  
    1.22    sealed case class Item(
    1.23 @@ -113,20 +126,22 @@
    1.24    }
    1.25  
    1.26  
    1.27 -  /** word completion **/
    1.28 +  /** word parsers **/
    1.29  
    1.30 -  private val word_regex = "[a-zA-Z0-9_']+".r
    1.31 -  private def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
    1.32 -
    1.33 -  private object Parse extends RegexParsers
    1.34 +  private object Word_Parsers extends RegexParsers
    1.35    {
    1.36      override val whiteSpace = "".r
    1.37  
    1.38 -    def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
    1.39 -    def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
    1.40 -    def escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r
    1.41 -    def word: Parser[String] = word_regex
    1.42 -    def word3: Parser[String] = """[a-zA-Z0-9_']{3,}""".r
    1.43 +    private def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
    1.44 +    private def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
    1.45 +    private def escape: Parser[String] = """[a-zA-Z0-9_']+\\""".r
    1.46 +
    1.47 +    private val word_regex = "[a-zA-Z0-9_']+".r
    1.48 +    private def word: Parser[String] = word_regex
    1.49 +    private def word3: Parser[String] = """[a-zA-Z0-9_']{3,}""".r
    1.50 +
    1.51 +    def is_word(s: CharSequence): Boolean =
    1.52 +      word_regex.pattern.matcher(s).matches
    1.53  
    1.54      def read(explicit: Boolean, in: CharSequence): Option[String] =
    1.55      {
    1.56 @@ -141,6 +156,7 @@
    1.57  }
    1.58  
    1.59  final class Completion private(
    1.60 +  keywords: Set[String] = Set.empty,
    1.61    words_lex: Scan.Lexicon = Scan.Lexicon.empty,
    1.62    words_map: Multi_Map[String, String] = Multi_Map.empty,
    1.63    abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
    1.64 @@ -150,6 +166,7 @@
    1.65  
    1.66    def + (keyword: String, replace: String): Completion =
    1.67      new Completion(
    1.68 +      keywords + keyword,
    1.69        words_lex + keyword,
    1.70        words_map + (keyword -> replace),
    1.71        abbrevs_lex,
    1.72 @@ -160,15 +177,16 @@
    1.73    private def add_symbols(): Completion =
    1.74    {
    1.75      val words =
    1.76 -      (for ((x, _) <- Symbol.names) yield (x, x)).toList :::
    1.77 -      (for ((x, y) <- Symbol.names) yield ("\\" + y, x)).toList :::
    1.78 -      (for ((x, y) <- Symbol.abbrevs.iterator if Completion.is_word(y)) yield (y, x)).toList
    1.79 +      (for ((x, _) <- Symbol.names.toList) yield (x, x)) :::
    1.80 +      (for ((x, y) <- Symbol.names.toList) yield ("\\" + y, x)) :::
    1.81 +      (for ((x, y) <- Symbol.abbrevs.toList if Completion.Word_Parsers.is_word(y)) yield (y, x))
    1.82  
    1.83      val abbrs =
    1.84 -      (for ((x, y) <- Symbol.abbrevs.iterator if !Completion.is_word(y))
    1.85 -        yield (y.reverse.toString, (y, x))).toList
    1.86 +      (for ((x, y) <- Symbol.abbrevs.iterator if !Completion.Word_Parsers.is_word(y))
    1.87 +        yield (y.reverse, (y, x))).toList
    1.88  
    1.89      new Completion(
    1.90 +      keywords,
    1.91        words_lex ++ words.map(_._1),
    1.92        words_map ++ words,
    1.93        abbrevs_lex ++ abbrs.map(_._1),
    1.94 @@ -182,34 +200,45 @@
    1.95      history: Completion.History,
    1.96      decode: Boolean,
    1.97      explicit: Boolean,
    1.98 -    line: CharSequence): Option[Completion.Result] =
    1.99 +    text: CharSequence,
   1.100 +    context: Completion.Context): Option[Completion.Result] =
   1.101    {
   1.102 -    val raw_result =
   1.103 -      Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), new Library.Reverse(line)) match {
   1.104 -        case Scan.Parsers.Success(reverse_a, _) =>
   1.105 -          val abbrevs = abbrevs_map.get_list(reverse_a)
   1.106 -          abbrevs match {
   1.107 -            case Nil => None
   1.108 -            case (a, _) :: _ => Some((a, abbrevs.map(_._2)))
   1.109 -          }
   1.110 -        case _ =>
   1.111 -          Completion.Parse.read(explicit, line) match {
   1.112 -            case Some(word) =>
   1.113 -              words_lex.completions(word).map(words_map.get_list(_)).flatten match {
   1.114 -                case Nil => None
   1.115 -                case cs => Some(word, cs)
   1.116 -              }
   1.117 -            case None => None
   1.118 -          }
   1.119 +    val abbrevs_result =
   1.120 +      if (context.symbols)
   1.121 +        Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), new Library.Reverse(text)) match {
   1.122 +          case Scan.Parsers.Success(reverse_a, _) =>
   1.123 +            val abbrevs = abbrevs_map.get_list(reverse_a)
   1.124 +            abbrevs match {
   1.125 +              case Nil => None
   1.126 +              case (a, _) :: _ => Some((a, abbrevs.map(_._2)))
   1.127 +            }
   1.128 +          case _ => None
   1.129 +        }
   1.130 +      else None
   1.131 +
   1.132 +    val words_result =
   1.133 +      abbrevs_result orElse {
   1.134 +        Completion.Word_Parsers.read(explicit, text) match {
   1.135 +          case Some(word) =>
   1.136 +            val completions =
   1.137 +              for {
   1.138 +                s <- words_lex.completions(word)
   1.139 +                if (if (keywords(s)) context.is_outer else context.symbols)
   1.140 +                r <- words_map.get_list(s)
   1.141 +              } yield r
   1.142 +            if (completions.isEmpty) None
   1.143 +            else Some(word, completions)
   1.144 +          case None => None
   1.145 +        }
   1.146        }
   1.147 -    raw_result match {
   1.148 +
   1.149 +    words_result match {
   1.150        case Some((word, cs)) =>
   1.151 -        val ds =
   1.152 -          (if (decode) cs.map(Symbol.decode(_)) else cs).filter(_ != word)
   1.153 +        val ds = (if (decode) cs.map(Symbol.decode(_)) else cs).filter(_ != word)
   1.154          if (ds.isEmpty) None
   1.155          else {
   1.156            val immediate =
   1.157 -            !Completion.is_word(word) &&
   1.158 +            !Completion.Word_Parsers.is_word(word) &&
   1.159              Character.codePointCount(word, 0, word.length) > 1
   1.160            val items = ds.map(s => Completion.Item(word, s, s, explicit || immediate))
   1.161            Some(Completion.Result(word, cs.length == 1, items.sorted(history.ordering)))

     2.1 --- a/src/Pure/PIDE/markup.ML	Wed Feb 19 21:38:44 2014 +0100
     2.2 +++ b/src/Pure/PIDE/markup.ML	Thu Feb 20 12:53:12 2014 +0100
     2.3 @@ -20,7 +20,8 @@
     2.4    val name: string -> T -> T
     2.5    val kindN: string
     2.6    val instanceN: string
     2.7 -  val languageN: string val language: string -> T
     2.8 +  val symbolsN: string
     2.9 +  val languageN: string val language: string -> bool -> T
    2.10    val language_sort: T
    2.11    val language_type: T
    2.12    val language_term: T
    2.13 @@ -246,17 +247,19 @@
    2.14  
    2.15  (* embedded languages *)
    2.16  
    2.17 -val (languageN, language) = markup_string "language" nameN;
    2.18 +val symbolsN = "symbols";
    2.19 +val languageN = "language";
    2.20 +fun language name symbols = (languageN, [(nameN, name), (symbolsN, print_bool symbols)]);
    2.21  
    2.22 -val language_sort = language "sort";
    2.23 -val language_type = language "type";
    2.24 -val language_term = language "term";
    2.25 -val language_prop = language "prop";
    2.26 +val language_sort = language "sort" true;
    2.27 +val language_type = language "type" true;
    2.28 +val language_term = language "term" true;
    2.29 +val language_prop = language "prop" true;
    2.30  
    2.31 -val language_ML = language "ML";
    2.32 -val language_document = language "document";
    2.33 -val language_text = language "text";
    2.34 -val language_rail = language "rail";
    2.35 +val language_ML = language "ML" false;
    2.36 +val language_document = language "document" false;
    2.37 +val language_text = language "text" true;
    2.38 +val language_rail = language "rail" true;
    2.39  
    2.40  
    2.41  (* formal entities *)

     3.1 --- a/src/Pure/PIDE/markup.scala	Wed Feb 19 21:38:44 2014 +0100
     3.2 +++ b/src/Pure/PIDE/markup.scala	Thu Feb 20 12:53:12 2014 +0100
     3.3 @@ -59,7 +59,7 @@
     3.4        markup match {
     3.5          case Markup(ENTITY, props) =>
     3.6            (props, props) match {
     3.7 -            case (Kind(kind), Name(name)) => Some(kind, name)
     3.8 +            case (Kind(kind), Name(name)) => Some((kind, name))
     3.9              case _ => None
    3.10            }
    3.11          case _ => None
    3.12 @@ -87,8 +87,22 @@
    3.13  
    3.14    /* embedded languages */
    3.15  
    3.16 +  val SYMBOLS = "symbols"
    3.17 +  val Symbols = new Properties.Boolean(SYMBOLS)
    3.18 +
    3.19    val LANGUAGE = "language"
    3.20 -  val Language = new Markup_String(LANGUAGE, NAME)
    3.21 +  object Language
    3.22 +  {
    3.23 +    def unapply(markup: Markup): Option[(String, Boolean)] =
    3.24 +      markup match {
    3.25 +        case Markup(LANGUAGE, props) =>
    3.26 +          (props, props) match {
    3.27 +            case (Name(name), Symbols(symbols)) => Some((name, symbols))
    3.28 +            case _ => None
    3.29 +          }
    3.30 +        case _ => None
    3.31 +      }
    3.32 +  }
    3.33  
    3.34  
    3.35    /* external resources */

     4.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Wed Feb 19 21:38:44 2014 +0100
     4.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Feb 20 12:53:12 2014 +0100
     4.3 @@ -110,7 +110,12 @@
     4.4  
     4.5              val history = PIDE.completion_history.value
     4.6              val decode = Isabelle_Encoding.is_active(buffer)
     4.7 -            syntax.completion.complete(history, decode, explicit, text) match {
     4.8 +            val context =
     4.9 +              PIDE.document_view(text_area) match {
    4.10 +                case None => Completion.Context.default
    4.11 +                case Some(doc_view) => doc_view.get_rendering().completion_context(caret)
    4.12 +              }
    4.13 +            syntax.completion.complete(history, decode, explicit, text, context) match {
    4.14                case Some(result) =>
    4.15                  if (result.unique && result.items.head.immediate && immediate)
    4.16                    insert(result.items.head)
    4.17 @@ -277,7 +282,8 @@
    4.18            val caret = text_field.getCaret.getDot
    4.19            val text = text_field.getText.substring(0, caret)
    4.20  
    4.21 -          syntax.completion.complete(history, decode = true, explicit = false, text) match {
    4.22 +          syntax.completion.complete(
    4.23 +              history, decode = true, explicit = false, text, Completion.Context.default) match {
    4.24              case Some(result) =>
    4.25                val fm = text_field.getFontMetrics(text_field.getFont)
    4.26                val loc =

     5.1 --- a/src/Tools/jEdit/src/rendering.scala	Wed Feb 19 21:38:44 2014 +0100
     5.2 +++ b/src/Tools/jEdit/src/rendering.scala	Thu Feb 20 12:53:12 2014 +0100
     5.3 @@ -200,6 +200,31 @@
     5.4    val dynamic_color = color_value("dynamic_color")
     5.5  
     5.6  
     5.7 +  /* completion context */
     5.8 +
     5.9 +  private val completion_elements =
    5.10 +    Set(Markup.STRING, Markup.ALTSTRING, Markup.VERBATIM, Markup.CARTOUCHE,
    5.11 +      Markup.COMMENT, Markup.LANGUAGE)
    5.12 +
    5.13 +  def completion_context(caret: Text.Offset): Completion.Context =
    5.14 +    if (caret > 0) {
    5.15 +      val result =
    5.16 +        snapshot.select_markup(Text.Range(caret - 1, caret + 1), Some(completion_elements), _ =>
    5.17 +          {
    5.18 +            case Text.Info(_, XML.Elem(Markup.Language(language, symbols), _)) =>
    5.19 +              Some(Completion.Context(language, symbols))
    5.20 +            case Text.Info(_, XML.Elem(markup, _)) =>
    5.21 +              if (completion_elements(markup.name)) Some(Completion.Context("unknown", true))
    5.22 +              else None
    5.23 +          })
    5.24 +      result match {
    5.25 +        case Text.Info(_, context) :: _ => context
    5.26 +        case Nil => Completion.Context.default
    5.27 +      }
    5.28 +    }
    5.29 +    else Completion.Context.default
    5.30 +
    5.31 +
    5.32    /* command overview */
    5.33  
    5.34    val overview_limit = options.int("jedit_text_overview_limit")
    5.35 @@ -429,8 +454,8 @@
    5.36              Some(add(prev, r, (true, pretty_typing("::", body))))
    5.37            case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
    5.38              Some(add(prev, r, (false, pretty_typing("ML:", body))))
    5.39 -          case (prev, Text.Info(r, XML.Elem(Markup.Language(name), _))) =>
    5.40 -            Some(add(prev, r, (true, XML.Text("language: " + name))))
    5.41 +          case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _), _))) =>
    5.42 +            Some(add(prev, r, (true, XML.Text("language: " + language))))
    5.43            case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
    5.44              if (tooltips.isDefinedAt(name))
    5.45                Some(add(prev, r, (true, XML.Text(tooltips(name)))))