1.1 --- a/src/Pure/Isar/completion.scala	Fri Feb 21 23:42:43 2014 +0100
     1.2 +++ b/src/Pure/Isar/completion.scala	Sat Feb 22 15:07:33 2014 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  /*  Title:      Pure/Isar/completion.scala
     1.5      Author:     Makarius
     1.6  
     1.7 -Completion of symbols and keywords.
     1.8 +Completion of keywords and symbols, with abbreviations.
     1.9  */
    1.10  
    1.11  package isabelle
    1.12 @@ -18,10 +18,13 @@
    1.13  
    1.14    object Context
    1.15    {
    1.16 -    val default = Context("", true)
    1.17 +    val outer = Context("", true, false)
    1.18 +    val inner = Context(Markup.Language.UNKNOWN, true, false)
    1.19 +    val ML_outer = Context(Markup.Language.ML, false, false)
    1.20 +    val ML_inner = Context(Markup.Language.ML, true, true)
    1.21    }
    1.22  
    1.23 -  sealed case class Context(language: String, symbols: Boolean)
    1.24 +  sealed case class Context(language: String, symbols: Boolean, antiquotes: Boolean)
    1.25    {
    1.26      def is_outer: Boolean = language == ""
    1.27    }
    1.28 @@ -31,10 +34,11 @@
    1.29  
    1.30    sealed case class Item(
    1.31      original: String,
    1.32 +    name: String,
    1.33      replacement: String,
    1.34 -    description: String,
    1.35 +    move: Int,
    1.36      immediate: Boolean)
    1.37 -  { override def toString: String = description }
    1.38 +  { override def toString: String = name }
    1.39  
    1.40    sealed case class Result(original: String, unique: Boolean, items: List[Item])
    1.41  
    1.42 @@ -92,8 +96,8 @@
    1.43        new Ordering[Item] {
    1.44          def compare(item1: Item, item2: Item): Int =
    1.45          {
    1.46 -          frequency(item1.replacement) compare frequency(item2.replacement) match {
    1.47 -            case 0 => item1.replacement compare item2.replacement
    1.48 +          frequency(item1.name) compare frequency(item2.name) match {
    1.49 +            case 0 => item1.name compare item2.name
    1.50              case ord => - ord
    1.51            }
    1.52          }
    1.53 @@ -122,7 +126,7 @@
    1.54      }
    1.55  
    1.56      def update(item: Item, freq: Int = 1): Unit = synchronized {
    1.57 -      history = history + (item.replacement -> freq)
    1.58 +      history = history + (item.name -> freq)
    1.59      }
    1.60    }
    1.61  
    1.62 @@ -154,6 +158,14 @@
    1.63        }
    1.64      }
    1.65    }
    1.66 +
    1.67 +
    1.68 +  /* abbreviations */
    1.69 +
    1.70 +  private val caret = '\007'
    1.71 +  private val antiquote = "@{"
    1.72 +  private val default_abbrs =
    1.73 +    Map("@{" -> "@{\007}", "`" -> "\\<open>\007\\<close>")
    1.74  }
    1.75  
    1.76  final class Completion private(
    1.77 @@ -182,9 +194,13 @@
    1.78        (for ((x, y) <- Symbol.names.toList) yield ("\\" + y, x)) :::
    1.79        (for ((x, y) <- Symbol.abbrevs.toList if Completion.Word_Parsers.is_word(y)) yield (y, x))
    1.80  
    1.81 +    val symbol_abbrs =
    1.82 +      (for ((x, y) <- Symbol.abbrevs.iterator if !Completion.Word_Parsers.is_word(y))
    1.83 +        yield (y, x)).toList
    1.84 +
    1.85      val abbrs =
    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 +      for ((a, b) <- symbol_abbrs ::: Completion.default_abbrs.toList)
    1.89 +        yield (a.reverse, (a, b))
    1.90  
    1.91      new Completion(
    1.92        keywords,
    1.93 @@ -205,17 +221,19 @@
    1.94      context: Completion.Context): Option[Completion.Result] =
    1.95    {
    1.96      val abbrevs_result =
    1.97 -      if (context.symbols)
    1.98 -        Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), new Library.Reverse(text)) match {
    1.99 -          case Scan.Parsers.Success(reverse_a, _) =>
   1.100 -            val abbrevs = abbrevs_map.get_list(reverse_a)
   1.101 -            abbrevs match {
   1.102 -              case Nil => None
   1.103 -              case (a, _) :: _ => Some((a, abbrevs.map(_._2)))
   1.104 -            }
   1.105 -          case _ => None
   1.106 -        }
   1.107 -      else None
   1.108 +      Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), new Library.Reverse(text)) match {
   1.109 +        case Scan.Parsers.Success(reverse_a, _) =>
   1.110 +          val abbrevs = abbrevs_map.get_list(reverse_a)
   1.111 +          abbrevs match {
   1.112 +            case Nil => None
   1.113 +            case (a, _) :: _ =>
   1.114 +              val ok =
   1.115 +                if (a == Completion.antiquote) context.antiquotes
   1.116 +                else context.symbols || Completion.default_abbrs.isDefinedAt(a)
   1.117 +              if (ok) Some((a, abbrevs.map(_._2))) else None
   1.118 +          }
   1.119 +        case _ => None
   1.120 +      }
   1.121  
   1.122      val words_result =
   1.123        abbrevs_result orElse {
   1.124 @@ -241,7 +259,15 @@
   1.125            val immediate =
   1.126              !Completion.Word_Parsers.is_word(word) &&
   1.127              Character.codePointCount(word, 0, word.length) > 1
   1.128 -          val items = ds.map(s => Completion.Item(word, s, s, explicit || immediate))
   1.129 +          val items =
   1.130 +            ds.map(s => {
   1.131 +              val (s1, s2) =
   1.132 +                space_explode(Completion.caret, s) match {
   1.133 +                  case List(s1, s2) => (s1, s2)
   1.134 +                  case _ => (s, "")
   1.135 +                }
   1.136 +              Completion.Item(word, s, s1 + s2, - s2.length, explicit || immediate)
   1.137 +            })
   1.138            Some(Completion.Result(word, cs.length == 1, items.sorted(history.ordering)))
   1.139          }
   1.140        case None => None

     2.1 --- a/src/Pure/Isar/outer_syntax.scala	Fri Feb 21 23:42:43 2014 +0100
     2.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sat Feb 22 15:07:33 2014 +0100
     2.3 @@ -43,7 +43,7 @@
     2.4    keywords: Map[String, (String, List[String])] = Map.empty,
     2.5    lexicon: Scan.Lexicon = Scan.Lexicon.empty,
     2.6    val completion: Completion = Completion.empty,
     2.7 -  val completion_context: Completion.Context = Completion.Context.default,
     2.8 +  val completion_context: Completion.Context = Completion.Context.outer,
     2.9    val has_tokens: Boolean = true)
    2.10  {
    2.11    override def toString: String =

     3.1 --- a/src/Pure/PIDE/markup.ML	Fri Feb 21 23:42:43 2014 +0100
     3.2 +++ b/src/Pure/PIDE/markup.ML	Sat Feb 22 15:07:33 2014 +0100
     3.3 @@ -21,7 +21,8 @@
     3.4    val kindN: string
     3.5    val instanceN: string
     3.6    val symbolsN: string
     3.7 -  val languageN: string val language: string -> bool -> T
     3.8 +  val languageN: string
     3.9 +  val language: {name: string, symbols: bool, antiquotes: bool} -> T
    3.10    val language_sort: T
    3.11    val language_type: T
    3.12    val language_term: T
    3.13 @@ -249,18 +250,22 @@
    3.14  (* embedded languages *)
    3.15  
    3.16  val symbolsN = "symbols";
    3.17 +val antiquotesN = "antiquotes";
    3.18  val languageN = "language";
    3.19 -fun language name symbols = (languageN, [(nameN, name), (symbolsN, print_bool symbols)]);
    3.20  
    3.21 -val language_sort = language "sort" true;
    3.22 -val language_type = language "type" true;
    3.23 -val language_term = language "term" true;
    3.24 -val language_prop = language "prop" true;
    3.25 -val language_ML = language "ML" false;
    3.26 -val language_document = language "document" false;
    3.27 -val language_antiquotation = language "antiquotation" true;
    3.28 -val language_text = language "text" true;
    3.29 -val language_rail = language "rail" true;
    3.30 +fun language {name, symbols, antiquotes} =
    3.31 +  (languageN,
    3.32 +    [(nameN, name), (symbolsN, print_bool symbols), (antiquotesN, print_bool antiquotes)]);
    3.33 +
    3.34 +val language_sort = language {name = "sort", symbols = true, antiquotes = false};
    3.35 +val language_type = language {name = "type", symbols = true, antiquotes = false};
    3.36 +val language_term = language {name = "term", symbols = true, antiquotes = false};
    3.37 +val language_prop = language {name = "prop", symbols = true, antiquotes = false};
    3.38 +val language_ML = language {name = "ML", symbols = false, antiquotes = true};
    3.39 +val language_document = language {name = "document", symbols = false, antiquotes = true};
    3.40 +val language_antiquotation = language {name = "antiquotation", symbols = true, antiquotes = false};
    3.41 +val language_text = language {name = "text", symbols = true, antiquotes = false};
    3.42 +val language_rail = language {name = "rail", symbols = true, antiquotes = true};
    3.43  
    3.44  
    3.45  (* formal entities *)

     4.1 --- a/src/Pure/PIDE/markup.scala	Fri Feb 21 23:42:43 2014 +0100
     4.2 +++ b/src/Pure/PIDE/markup.scala	Sat Feb 22 15:07:33 2014 +0100
     4.3 @@ -87,8 +87,8 @@
     4.4  
     4.5    /* embedded languages */
     4.6  
     4.7 -  val SYMBOLS = "symbols"
     4.8 -  val Symbols = new Properties.Boolean(SYMBOLS)
     4.9 +  val Symbols = new Properties.Boolean("symbols")
    4.10 +  val Antiquotes = new Properties.Boolean("antiquotes")
    4.11  
    4.12    val LANGUAGE = "language"
    4.13    object Language
    4.14 @@ -96,11 +96,12 @@
    4.15      val ML = "ML"
    4.16      val UNKNOWN = "unknown"
    4.17  
    4.18 -    def unapply(markup: Markup): Option[(String, Boolean)] =
    4.19 +    def unapply(markup: Markup): Option[(String, Boolean, Boolean)] =
    4.20        markup match {
    4.21          case Markup(LANGUAGE, props) =>
    4.22 -          (props, props) match {
    4.23 -            case (Name(name), Symbols(symbols)) => Some((name, symbols))
    4.24 +          (props, props, props) match {
    4.25 +            case (Name(name), Symbols(symbols), Antiquotes(antiquotes)) =>
    4.26 +              Some((name, symbols, antiquotes))
    4.27              case _ => None
    4.28            }
    4.29          case _ => None

     5.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Fri Feb 21 23:42:43 2014 +0100
     5.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Sat Feb 22 15:07:33 2014 +0100
     5.3 @@ -87,6 +87,8 @@
     5.4              case Some(text) if text == item.original =>
     5.5                buffer.remove(caret - len, len)
     5.6                buffer.insert(caret - len, item.replacement)
     5.7 +              if (item.move != 0)
     5.8 +                text_area.moveCaretPosition(text_area.getCaretPosition + item.move)
     5.9              case _ =>
    5.10            }
    5.11          }
    5.12 @@ -265,7 +267,7 @@
    5.13                content.substring(0, caret - len) +
    5.14                item.replacement +
    5.15                content.substring(caret))
    5.16 -            text_field.getCaret.setDot(caret - len + item.replacement.length)
    5.17 +            text_field.getCaret.setDot(caret - len + item.replacement.length + item.move)
    5.18            case _ =>
    5.19          }
    5.20        }

     6.1 --- a/src/Tools/jEdit/src/isabelle.scala	Fri Feb 21 23:42:43 2014 +0100
     6.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Sat Feb 22 15:07:33 2014 +0100
     6.3 @@ -33,7 +33,7 @@
     6.4  
     6.5    private lazy val ml_syntax: Outer_Syntax =
     6.6      Outer_Syntax.init().no_tokens.
     6.7 -      set_completion_context(Completion.Context(Markup.Language.ML, false))
     6.8 +      set_completion_context(Completion.Context.ML_outer)
     6.9  
    6.10    private lazy val news_syntax: Outer_Syntax =
    6.11      Outer_Syntax.init().no_tokens

     7.1 --- a/src/Tools/jEdit/src/rendering.scala	Fri Feb 21 23:42:43 2014 +0100
     7.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Feb 22 15:07:33 2014 +0100
     7.3 @@ -278,11 +278,11 @@
     7.4            {
     7.5              case Text.Info(_, elem)
     7.6              if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
     7.7 -              Some(Completion.Context(Markup.Language.ML, true))
     7.8 -            case Text.Info(_, XML.Elem(Markup.Language(language, symbols), _)) =>
     7.9 -              Some(Completion.Context(language, symbols))
    7.10 -            case Text.Info(_, XML.Elem(markup, _)) =>
    7.11 -              Some(Completion.Context(Markup.Language.UNKNOWN, true))
    7.12 +              Some(Completion.Context.ML_inner)
    7.13 +            case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes), _)) =>
    7.14 +              Some(Completion.Context(language, symbols, antiquotes))
    7.15 +            case Text.Info(_, _) =>
    7.16 +              Some(Completion.Context.inner)
    7.17            })
    7.18        result match {
    7.19          case Text.Info(_, context) :: _ => Some(context)
    7.20 @@ -500,7 +500,7 @@
    7.21              Some(add(prev, r, (true, pretty_typing("::", body))))
    7.22            case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
    7.23              Some(add(prev, r, (false, pretty_typing("ML:", body))))
    7.24 -          case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _), _))) =>
    7.25 +          case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _), _))) =>
    7.26              Some(add(prev, r, (true, XML.Text("language: " + language))))
    7.27            case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
    7.28              Rendering.tooltip_descriptions.get(name).