# HG changeset patch
# User wenzelm
# Date 1393078053 -3600
# Node ID cc350eb1087ec7bdfbb33b6d0053ed332053ab7c
# Parent  4381a2b622ea588978dc36f189e9319ede3b06b6
refined language context: antiquotes;
support default completions, with move of caret position;
tuned signature;

diff -r 4381a2b622ea -r cc350eb1087e src/Pure/Isar/completion.scala
--- a/src/Pure/Isar/completion.scala	Fri Feb 21 23:42:43 2014 +0100
+++ b/src/Pure/Isar/completion.scala	Sat Feb 22 15:07:33 2014 +0100
@@ -1,7 +1,7 @@
 /*  Title:      Pure/Isar/completion.scala
     Author:     Makarius
 
-Completion of symbols and keywords.
+Completion of keywords and symbols, with abbreviations.
 */
 
 package isabelle
@@ -18,10 +18,13 @@
 
   object Context
   {
-    val default = Context("", true)
+    val outer = Context("", true, false)
+    val inner = Context(Markup.Language.UNKNOWN, true, false)
+    val ML_outer = Context(Markup.Language.ML, false, false)
+    val ML_inner = Context(Markup.Language.ML, true, true)
   }
 
-  sealed case class Context(language: String, symbols: Boolean)
+  sealed case class Context(language: String, symbols: Boolean, antiquotes: Boolean)
   {
     def is_outer: Boolean = language == ""
   }
@@ -31,10 +34,11 @@
 
   sealed case class Item(
     original: String,
+    name: String,
     replacement: String,
-    description: String,
+    move: Int,
     immediate: Boolean)
-  { override def toString: String = description }
+  { override def toString: String = name }
 
   sealed case class Result(original: String, unique: Boolean, items: List[Item])
 
@@ -92,8 +96,8 @@
       new Ordering[Item] {
         def compare(item1: Item, item2: Item): Int =
         {
-          frequency(item1.replacement) compare frequency(item2.replacement) match {
-            case 0 => item1.replacement compare item2.replacement
+          frequency(item1.name) compare frequency(item2.name) match {
+            case 0 => item1.name compare item2.name
             case ord => - ord
           }
         }
@@ -122,7 +126,7 @@
     }
 
     def update(item: Item, freq: Int = 1): Unit = synchronized {
-      history = history + (item.replacement -> freq)
+      history = history + (item.name -> freq)
     }
   }
 
@@ -154,6 +158,14 @@
       }
     }
   }
+
+
+  /* abbreviations */
+
+  private val caret = '\007'
+  private val antiquote = "@{"
+  private val default_abbrs =
+    Map("@{" -> "@{\007}", "`" -> "\\<open>\007\\<close>")
 }
 
 final class Completion private(
@@ -182,9 +194,13 @@
       (for ((x, y) <- Symbol.names.toList) yield ("\\" + y, x)) :::
       (for ((x, y) <- Symbol.abbrevs.toList if Completion.Word_Parsers.is_word(y)) yield (y, x))
 
-    val abbrs =
+    val symbol_abbrs =
       (for ((x, y) <- Symbol.abbrevs.iterator if !Completion.Word_Parsers.is_word(y))
-        yield (y.reverse, (y, x))).toList
+        yield (y, x)).toList
+
+    val abbrs =
+      for ((a, b) <- symbol_abbrs ::: Completion.default_abbrs.toList)
+        yield (a.reverse, (a, b))
 
     new Completion(
       keywords,
@@ -205,17 +221,19 @@
     context: Completion.Context): Option[Completion.Result] =
   {
     val abbrevs_result =
-      if (context.symbols)
-        Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), new Library.Reverse(text)) match {
-          case Scan.Parsers.Success(reverse_a, _) =>
-            val abbrevs = abbrevs_map.get_list(reverse_a)
-            abbrevs match {
-              case Nil => None
-              case (a, _) :: _ => Some((a, abbrevs.map(_._2)))
-            }
-          case _ => None
-        }
-      else None
+      Scan.Parsers.parse(Scan.Parsers.literal(abbrevs_lex), new Library.Reverse(text)) match {
+        case Scan.Parsers.Success(reverse_a, _) =>
+          val abbrevs = abbrevs_map.get_list(reverse_a)
+          abbrevs match {
+            case Nil => None
+            case (a, _) :: _ =>
+              val ok =
+                if (a == Completion.antiquote) context.antiquotes
+                else context.symbols || Completion.default_abbrs.isDefinedAt(a)
+              if (ok) Some((a, abbrevs.map(_._2))) else None
+          }
+        case _ => None
+      }
 
     val words_result =
       abbrevs_result orElse {
@@ -241,7 +259,15 @@
           val immediate =
             !Completion.Word_Parsers.is_word(word) &&
             Character.codePointCount(word, 0, word.length) > 1
-          val items = ds.map(s => Completion.Item(word, s, s, explicit || immediate))
+          val items =
+            ds.map(s => {
+              val (s1, s2) =
+                space_explode(Completion.caret, s) match {
+                  case List(s1, s2) => (s1, s2)
+                  case _ => (s, "")
+                }
+              Completion.Item(word, s, s1 + s2, - s2.length, explicit || immediate)
+            })
           Some(Completion.Result(word, cs.length == 1, items.sorted(history.ordering)))
         }
       case None => None
diff -r 4381a2b622ea -r cc350eb1087e src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Fri Feb 21 23:42:43 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Sat Feb 22 15:07:33 2014 +0100
@@ -43,7 +43,7 @@
   keywords: Map[String, (String, List[String])] = Map.empty,
   lexicon: Scan.Lexicon = Scan.Lexicon.empty,
   val completion: Completion = Completion.empty,
-  val completion_context: Completion.Context = Completion.Context.default,
+  val completion_context: Completion.Context = Completion.Context.outer,
   val has_tokens: Boolean = true)
 {
   override def toString: String =
diff -r 4381a2b622ea -r cc350eb1087e src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Fri Feb 21 23:42:43 2014 +0100
+++ b/src/Pure/PIDE/markup.ML	Sat Feb 22 15:07:33 2014 +0100
@@ -21,7 +21,8 @@
   val kindN: string
   val instanceN: string
   val symbolsN: string
-  val languageN: string val language: string -> bool -> T
+  val languageN: string
+  val language: {name: string, symbols: bool, antiquotes: bool} -> T
   val language_sort: T
   val language_type: T
   val language_term: T
@@ -249,18 +250,22 @@
 (* embedded languages *)
 
 val symbolsN = "symbols";
+val antiquotesN = "antiquotes";
 val languageN = "language";
-fun language name symbols = (languageN, [(nameN, name), (symbolsN, print_bool symbols)]);
+
+fun language {name, symbols, antiquotes} =
+  (languageN,
+    [(nameN, name), (symbolsN, print_bool symbols), (antiquotesN, print_bool antiquotes)]);
 
-val language_sort = language "sort" true;
-val language_type = language "type" true;
-val language_term = language "term" true;
-val language_prop = language "prop" true;
-val language_ML = language "ML" false;
-val language_document = language "document" false;
-val language_antiquotation = language "antiquotation" true;
-val language_text = language "text" true;
-val language_rail = language "rail" true;
+val language_sort = language {name = "sort", symbols = true, antiquotes = false};
+val language_type = language {name = "type", symbols = true, antiquotes = false};
+val language_term = language {name = "term", symbols = true, antiquotes = false};
+val language_prop = language {name = "prop", symbols = true, antiquotes = false};
+val language_ML = language {name = "ML", symbols = false, antiquotes = true};
+val language_document = language {name = "document", symbols = false, antiquotes = true};
+val language_antiquotation = language {name = "antiquotation", symbols = true, antiquotes = false};
+val language_text = language {name = "text", symbols = true, antiquotes = false};
+val language_rail = language {name = "rail", symbols = true, antiquotes = true};
 
 
 (* formal entities *)
diff -r 4381a2b622ea -r cc350eb1087e src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Fri Feb 21 23:42:43 2014 +0100
+++ b/src/Pure/PIDE/markup.scala	Sat Feb 22 15:07:33 2014 +0100
@@ -87,8 +87,8 @@
 
   /* embedded languages */
 
-  val SYMBOLS = "symbols"
-  val Symbols = new Properties.Boolean(SYMBOLS)
+  val Symbols = new Properties.Boolean("symbols")
+  val Antiquotes = new Properties.Boolean("antiquotes")
 
   val LANGUAGE = "language"
   object Language
@@ -96,11 +96,12 @@
     val ML = "ML"
     val UNKNOWN = "unknown"
 
-    def unapply(markup: Markup): Option[(String, Boolean)] =
+    def unapply(markup: Markup): Option[(String, Boolean, Boolean)] =
       markup match {
         case Markup(LANGUAGE, props) =>
-          (props, props) match {
-            case (Name(name), Symbols(symbols)) => Some((name, symbols))
+          (props, props, props) match {
+            case (Name(name), Symbols(symbols), Antiquotes(antiquotes)) =>
+              Some((name, symbols, antiquotes))
             case _ => None
           }
         case _ => None
diff -r 4381a2b622ea -r cc350eb1087e src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Fri Feb 21 23:42:43 2014 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Sat Feb 22 15:07:33 2014 +0100
@@ -87,6 +87,8 @@
             case Some(text) if text == item.original =>
               buffer.remove(caret - len, len)
               buffer.insert(caret - len, item.replacement)
+              if (item.move != 0)
+                text_area.moveCaretPosition(text_area.getCaretPosition + item.move)
             case _ =>
           }
         }
@@ -265,7 +267,7 @@
               content.substring(0, caret - len) +
               item.replacement +
               content.substring(caret))
-            text_field.getCaret.setDot(caret - len + item.replacement.length)
+            text_field.getCaret.setDot(caret - len + item.replacement.length + item.move)
           case _ =>
         }
       }
diff -r 4381a2b622ea -r cc350eb1087e src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Fri Feb 21 23:42:43 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Sat Feb 22 15:07:33 2014 +0100
@@ -33,7 +33,7 @@
 
   private lazy val ml_syntax: Outer_Syntax =
     Outer_Syntax.init().no_tokens.
-      set_completion_context(Completion.Context(Markup.Language.ML, false))
+      set_completion_context(Completion.Context.ML_outer)
 
   private lazy val news_syntax: Outer_Syntax =
     Outer_Syntax.init().no_tokens
diff -r 4381a2b622ea -r cc350eb1087e src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Fri Feb 21 23:42:43 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Sat Feb 22 15:07:33 2014 +0100
@@ -278,11 +278,11 @@
           {
             case Text.Info(_, elem)
             if elem.name == Markup.ML_STRING || elem.name == Markup.ML_COMMENT =>
-              Some(Completion.Context(Markup.Language.ML, true))
-            case Text.Info(_, XML.Elem(Markup.Language(language, symbols), _)) =>
-              Some(Completion.Context(language, symbols))
-            case Text.Info(_, XML.Elem(markup, _)) =>
-              Some(Completion.Context(Markup.Language.UNKNOWN, true))
+              Some(Completion.Context.ML_inner)
+            case Text.Info(_, XML.Elem(Markup.Language(language, symbols, antiquotes), _)) =>
+              Some(Completion.Context(language, symbols, antiquotes))
+            case Text.Info(_, _) =>
+              Some(Completion.Context.inner)
           })
       result match {
         case Text.Info(_, context) :: _ => Some(context)
@@ -500,7 +500,7 @@
             Some(add(prev, r, (true, pretty_typing("::", body))))
           case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
             Some(add(prev, r, (false, pretty_typing("ML:", body))))
-          case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _), _))) =>
+          case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _), _))) =>
             Some(add(prev, r, (true, XML.Text("language: " + language))))
           case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
             Rendering.tooltip_descriptions.get(name).