# HG changeset patch
# User wenzelm
# Date 1451406978 -3600
# Node ID 20c1321378db75ba33e5f8f0ea17208a45d36afb
# Parent  364007370bb75896ef51605a5ab807f76a0dd3a5
support additional abbrevs;

diff -r 364007370bb7 -r 20c1321378db NEWS
--- a/NEWS	Tue Dec 29 16:23:34 2015 +0100
+++ b/NEWS	Tue Dec 29 17:36:18 2015 +0100
@@ -38,6 +38,9 @@
 always possible, independently of the language context. It is never
 implicit: a popup will show up unconditionally.
 
+* Additional abbreviations for syntactic completion may be specified in
+$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs.
+
 * Improved scheduling for urgent print tasks (e.g. command state output,
 interactive queries) wrt. long-running background tasks.
 
diff -r 364007370bb7 -r 20c1321378db etc/settings
--- a/etc/settings	Tue Dec 29 16:23:34 2015 +0100
+++ b/etc/settings	Tue Dec 29 17:36:18 2015 +0100
@@ -121,10 +121,11 @@
 
 
 ###
-### Rendering information
+### Symbol rendering and abbreviations
 ###
 
 ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols"
+ISABELLE_ABBREVS="$ISABELLE_HOME/etc/abbrevs:$ISABELLE_HOME_USER/etc/abbrevs"
 
 
 ###
diff -r 364007370bb7 -r 20c1321378db src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Tue Dec 29 16:23:34 2015 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Tue Dec 29 17:36:18 2015 +0100
@@ -1167,6 +1167,16 @@
   aggressively, except for single-character abbreviations like \<^verbatim>\<open>!\<close> above.
 
   \<^medskip>
+  Additional abbreviations may be specified in @{file
+  "$ISABELLE_HOME/etc/abbrevs"} and @{file_unchecked
+  "$ISABELLE_HOME_USER/etc/abbrevs"}. The file content follows general Isar
+  outer syntax @{cite "isabelle-isar-ref"}. Abbreviations are specified as
+  ``\<open>abbrev\<close>~\<^verbatim>\<open>=\<close>~\<open>text\<close>'' pairs. The replacement \<open>text\<close> may consist of more
+  than just one symbol; otherwise the meaning is the same as a symbol
+  specification ``\<open>sym\<close>~\<^verbatim>\<open>abbrev:\<close>~\<open>abbrev\<close>'' within @{file_unchecked
+  "etc/symbols"}.
+
+  \<^medskip>
   Symbol completion depends on the semantic language context
   (\secref{sec:completion-context}), to enable or disable that aspect for a
   particular sub-language of Isabelle. For example, symbol completion is
diff -r 364007370bb7 -r 20c1321378db src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Tue Dec 29 16:23:34 2015 +0100
+++ b/src/Pure/General/completion.scala	Tue Dec 29 17:36:18 2015 +0100
@@ -244,7 +244,7 @@
   /* init */
 
   val empty: Completion = new Completion()
-  def init(): Completion = empty.add_symbols()
+  def init(): Completion = empty.load()
 
 
   /* word parsers */
@@ -295,6 +295,36 @@
 
   /* abbreviations */
 
+  private object Abbrevs_Parser extends Parse.Parser
+  {
+    private val syntax = Outer_Syntax.empty + "="
+
+    private val entry: Parser[(String, String)] =
+      text ~ ($$$("=") ~! text) ^^ { case a ~ (_ ~ b) => (a, b) }
+
+    def parse_file(file: Path): List[(String, String)] =
+    {
+      val toks = Token.explode(syntax.keywords, File.read(file))
+      parse_all(rep(entry), Token.reader(toks, Token.Pos.file(file.implode))) match {
+        case Success(result, _) => result
+        case bad => error(bad.toString)
+      }
+    }
+  }
+
+  def load_abbrevs(): List[(String, String)] =
+  {
+    val symbol_abbrevs =
+      for ((sym, abbr) <- Symbol.abbrevs.toList) yield (abbr, sym)
+    val more_abbrevs =
+      for {
+        path <- Path.split(Isabelle_System.getenv("ISABELLE_ABBREVS"))
+        if path.is_file
+        entry <- Abbrevs_Parser.parse_file(path)
+      } yield entry
+    symbol_abbrevs ::: more_abbrevs
+  }
+
   private val caret_indicator = '\u0007'
   private val antiquote = "@{"
 
@@ -356,23 +386,24 @@
   def + (keyword: String): Completion = this + (keyword, keyword)
 
 
-  /* symbols with abbreviations */
+  /* load symbols and abbrevs */
 
-  private def add_symbols(): Completion =
+  private def load(): Completion =
   {
+    val abbrevs = Completion.load_abbrevs()
+
     val words =
       (for ((sym, _) <- Symbol.names.toList) yield (sym, sym)) :::
       (for ((sym, name) <- Symbol.names.toList) yield ("\\" + name, sym)) :::
-      (for ((sym, abbr) <- Symbol.abbrevs.toList if Completion.Word_Parsers.is_word(abbr))
-        yield (abbr, sym))
+      (for ((abbr, text) <- abbrevs if Completion.Word_Parsers.is_word(abbr)) yield (abbr, text))
 
-    val symbol_abbrs =
-      (for ((sym, abbr) <- Symbol.abbrevs.iterator if !Completion.Word_Parsers.is_word(abbr))
-        yield (abbr, sym)).toList
+    val non_word_abbrs =
+      (for ((abbr, text) <- abbrevs if !Completion.Word_Parsers.is_word(abbr))
+        yield (abbr, text)).toList
 
     val abbrs =
-      for ((abbr, sym) <- symbol_abbrs ::: Completion.default_abbrs)
-        yield (abbr.reverse, (abbr, sym))
+      for ((abbr, text) <- non_word_abbrs ::: Completion.default_abbrs)
+        yield (abbr.reverse, (abbr, text))
 
     new Completion(
       keywords,