# HG changeset patch
# User wenzelm
# Date 1473856658 -7200
# Node ID f745c6e683b7956f58d88b91cd3f860511f19530
# Parent  6db1aac936db19bfdad64857ad54d6e0c463504e
discontinued global etc/abbrevs;

diff -r 6db1aac936db -r f745c6e683b7 NEWS
--- a/NEWS	Wed Sep 14 14:17:32 2016 +0200
+++ b/NEWS	Wed Sep 14 14:37:38 2016 +0200
@@ -146,10 +146,13 @@
 e.g. 'context', 'notepad'.
 
 * Additional abbreviations for syntactic completion may be specified
-within the theory header as 'abbrevs', in addition to global
-$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs as
-before. The theory syntax for 'keywords' has been simplified
-accordingly: optional abbrevs need to go into the new 'abbrevs' section.
+within the theory header as 'abbrevs'. The theory syntax for 'keywords'
+has been simplified accordingly: optional abbrevs need to go into the
+new 'abbrevs' section.
+
+* Global abbreviations via $ISABELLE_HOME/etc/abbrevs and
+$ISABELLE_HOME_USER/etc/abbrevs are no longer supported. Minor
+INCOMPATIBILITY, use 'abbrevs' within theory header instead.
 
 * ML and document antiquotations for file-systems paths are more uniform
 and diverse:
diff -r 6db1aac936db -r f745c6e683b7 etc/abbrevs
--- a/etc/abbrevs	Wed Sep 14 14:17:32 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-(* additional abbreviations for syntactic completion *)
-
-(*prevent replacement of very long arrows*)
-"===>" = "===>"
-
-"--->" = "\<midarrow>\<rightarrow>"
diff -r 6db1aac936db -r f745c6e683b7 etc/settings
--- a/etc/settings	Wed Sep 14 14:17:32 2016 +0200
+++ b/etc/settings	Wed Sep 14 14:37:38 2016 +0200
@@ -121,11 +121,10 @@
 
 
 ###
-### Symbol rendering and abbreviations
+### Symbol rendering
 ###
 
 ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols"
-ISABELLE_ABBREVS="$ISABELLE_HOME/etc/abbrevs:$ISABELLE_HOME_USER/etc/abbrevs"
 
 
 ###
diff -r 6db1aac936db -r f745c6e683b7 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Wed Sep 14 14:17:32 2016 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Wed Sep 14 14:37:38 2016 +0200
@@ -1266,15 +1266,6 @@
   Backslash sequences also help when input is broken, and thus escapes its
   normal semantic context: e.g.\ antiquotations or string literals in ML,
   which do not allow arbitrary backslash sequences.
-
-  \<^medskip>
-  Additional abbreviations may be specified in \<^file>\<open>$ISABELLE_HOME/etc/abbrevs\<close>
-  and @{path "$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 @{path
-  "etc/symbols"}.
 \<close>
 
 
diff -r 6db1aac936db -r f745c6e683b7 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Wed Sep 14 14:17:32 2016 +0200
+++ b/src/Pure/General/completion.scala	Wed Sep 14 14:37:38 2016 +0200
@@ -246,7 +246,8 @@
   /* init */
 
   val empty: Completion = new Completion()
-  def init(): Completion = empty.load()
+  def init(): Completion =
+    empty.add_symbols.add_abbrevs(Completion.symbol_abbrevs ::: Completion.default_abbrevs)
 
 
   /* word parsers */
@@ -295,47 +296,22 @@
   }
 
 
-  /* 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
-    val remove_abbrevs = (for { (a, b) <- more_abbrevs if b == "" } yield a).toSet
-
-    (symbol_abbrevs ::: more_abbrevs).filterNot({ case (a, _) => remove_abbrevs.contains(a) })
-  }
+  /* templates */
 
   val caret_indicator = '\u0007'
+
   def split_template(s: String): (String, String) =
     space_explode(caret_indicator, s) match {
       case List(s1, s2) => (s1, s2)
       case _ => (s, "")
     }
 
+
+  /* abbreviations */
+
+  private def symbol_abbrevs: Thy_Header.Abbrevs =
+    for ((sym, abbr) <- Symbol.abbrevs.toList) yield (abbr, sym)
+
   private val antiquote = "@{"
 
   private val default_abbrevs =
@@ -393,7 +369,7 @@
 
   /* symbols and abbrevs */
 
-  def add_symbols(): Completion =
+  def add_symbols: Completion =
   {
     val words =
       (for ((sym, _) <- Symbol.names.toList) yield (sym, sym)) :::
@@ -429,9 +405,6 @@
     new Completion(keywords, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
   }
 
-  private def load(): Completion =
-    add_symbols().add_abbrevs(Completion.load_abbrevs() ::: Completion.default_abbrevs)
-
 
   /* complete */
 
diff -r 6db1aac936db -r f745c6e683b7 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Wed Sep 14 14:17:32 2016 +0200
+++ b/src/Pure/Pure.thy	Wed Sep 14 14:37:38 2016 +0200
@@ -92,6 +92,8 @@
   and "find_theorems" "find_consts" :: diag
   and "named_theorems" :: thy_decl
 abbrevs
+  "===>" = "===>"  (*prevent replacement of very long arrows*)
+  "--->" = "\<midarrow>\<rightarrow>"
   "default_sort" = ""
   "simproc_setup" = ""
   "hence" = ""