support 'abbrevs' within theory header;
simplified 'keywords': no abbreviations here;

--- a/NEWS	Tue Aug 02 11:49:30 2016 +0200
+++ b/NEWS	Tue Aug 02 17:35:18 2016 +0200
@@ -111,6 +111,12 @@
 * Completion templates for commands involving "begin ... end" blocks,
 e.g. 'context', 'notepad'.
 
+* Additional abbreviations for syntactic completion may be specified in
+within the theory header as 'abbrevs', in addition to global
+$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs. The
+theory syntax for 'keywords' has been simplified accordingly: optional
+abbrevs need to go into the new 'abbrevs' section.
+
 
 *** Isar ***
 

--- a/etc/abbrevs	Tue Aug 02 11:49:30 2016 +0200
+++ b/etc/abbrevs	Tue Aug 02 17:35:18 2016 +0200
@@ -4,7 +4,3 @@
 "===>" = "===>"
 
 "--->" = "\<midarrow>\<rightarrow>"
-
-(*HOL-NSA*)
-"--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
-"--->" = "\<midarrow>\<rightarrow>\<^sub>N\<^sub>S"

--- a/src/Doc/Isar_Ref/Spec.thy	Tue Aug 02 11:49:30 2016 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy	Tue Aug 02 17:35:18 2016 +0200
@@ -58,14 +58,15 @@
   such a global @{command (global) "end"}.
 
   @{rail \<open>
-    @@{command theory} @{syntax name} imports? keywords? \<newline> @'begin'
+    @@{command theory} @{syntax name} imports? \<newline> keywords? abbrevs? @'begin'
     ;
     imports: @'imports' (@{syntax name} +)
     ;
     keywords: @'keywords' (keyword_decls + @'and')
     ;
-    keyword_decls: (@{syntax string} +)
-      ('::' @{syntax name} @{syntax tags})? ('==' @{syntax name})?
+    keyword_decls: (@{syntax string} +) ('::' @{syntax name} @{syntax tags})?
+    ;
+    abbrevs: @'abbrevs' ((text '=' text) +)
     ;
     @@{command thy_deps} (thy_bounds thy_bounds?)?
     ;
@@ -85,7 +86,7 @@
   based on Isabelle. Regular user theories usually refer to some more complex
   entry point, such as theory @{theory Main} in Isabelle/HOL.
 
-  The optional @{keyword_def "keywords"} specification declares outer syntax
+  The @{keyword_def "keywords"} specification declares outer syntax
   (\chref{ch:outer-syntax}) that is introduced in this theory later on (rare
   in end-user applications). Both minor keywords and major keywords of the
   Isar command language need to be specified, in order to make parsing of
@@ -97,8 +98,10 @@
   @{syntax tags} provide defaults for document preparation
   (\secref{sec:tags}).
 
-  It is possible to specify an alternative completion via \<^verbatim>\<open>==\<close>~\<open>text\<close>, while
-  the default is the corresponding keyword name.
+  The @{keyword_def "abbrevs"} specification declares additional abbreviations
+  for syntactic completion. The default for a new keyword is just its name,
+  but completion may be avoided by defining @{keyword "abbrevs"} with empty
+  text.
   
   \<^descr> @{command (global) "end"} concludes the current theory definition. Note
   that some other commands, e.g.\ local theory targets \<^theory_text>\<open>locale\<close> or \<^theory_text>\<open>class\<close>

--- a/src/HOL/Library/Simps_Case_Conv.thy	Tue Aug 02 11:49:30 2016 +0200
+++ b/src/HOL/Library/Simps_Case_Conv.thy	Tue Aug 02 17:35:18 2016 +0200
@@ -5,8 +5,9 @@
 theory Simps_Case_Conv
 imports Main
 keywords
-  "simps_of_case" :: thy_decl == "" and
-  "case_of_simps" :: thy_decl
+  "simps_of_case" "case_of_simps" :: thy_decl
+abbrevs
+  "simps_of_case" = ""
 begin
 
 ML_file "simps_case_conv.ML"

--- a/src/HOL/Nonstandard_Analysis/HLim.thy	Tue Aug 02 11:49:30 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/HLim.thy	Tue Aug 02 17:35:18 2016 +0200
@@ -6,7 +6,8 @@
 section\<open>Limits and Continuity (Nonstandard)\<close>
 
 theory HLim
-imports Star
+  imports Star
+  abbrevs "--->" = "\<midarrow>\<rightarrow>\<^sub>N\<^sub>S"
 begin
 
 text\<open>Nonstandard Definitions\<close>

--- a/src/HOL/Nonstandard_Analysis/HSEQ.thy	Tue Aug 02 11:49:30 2016 +0200
+++ b/src/HOL/Nonstandard_Analysis/HSEQ.thy	Tue Aug 02 17:35:18 2016 +0200
@@ -11,7 +11,8 @@
 section \<open>Sequences and Convergence (Nonstandard)\<close>
 
 theory HSEQ
-imports Limits NatStar
+  imports Limits NatStar
+  abbrevs "--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
 begin
 
 definition

--- a/src/Pure/General/completion.scala	Tue Aug 02 11:49:30 2016 +0200
+++ b/src/Pure/General/completion.scala	Tue Aug 02 17:35:18 2016 +0200
@@ -344,7 +344,7 @@
 }
 
 final class Completion private(
-  protected val keywords: Map[String, Boolean] = Map.empty,
+  protected val keywords: Set[String] = Set.empty,
   protected val words_lex: Scan.Lexicon = Scan.Lexicon.empty,
   protected val words_map: Multi_Map[String, String] = Multi_Map.empty,
   protected val abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
@@ -363,8 +363,7 @@
     if (this eq other) this
     else if (is_empty) other
     else {
-      val keywords1 =
-        (keywords /: other.keywords) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
+      val keywords1 = (keywords /: other.keywords) { case (ks, k) => if (ks(k)) ks else ks + k }
       val words_lex1 = words_lex ++ other.words_lex
       val words_map1 = words_map ++ other.words_map
       val abbrevs_lex1 = abbrevs_lex ++ other.abbrevs_lex
@@ -376,19 +375,12 @@
   /* keywords */
 
   private def is_symbol(name: String): Boolean = Symbol.names.isDefinedAt(name)
-  private def is_keyword(name: String): Boolean = !is_symbol(name) && keywords.isDefinedAt(name)
+  private def is_keyword(name: String): Boolean = !is_symbol(name) && keywords(name)
   private def is_keyword_template(name: String, template: Boolean): Boolean =
-    is_keyword(name) && keywords(name) == template
+    is_keyword(name) && (words_map.getOrElse(name, name) != name) == template
 
-  def + (keyword: String, template: String): Completion =
-    new Completion(
-      keywords + (keyword -> (keyword != template)),
-      words_lex + keyword,
-      words_map + (keyword -> template),
-      abbrevs_lex,
-      abbrevs_map)
-
-  def + (keyword: String): Completion = this + (keyword, keyword)
+  def add_keyword(keyword: String): Completion =
+    new Completion(keywords + keyword, words_lex, words_map, abbrevs_lex, abbrevs_map)
 
 
   /* symbols and abbrevs */
@@ -408,21 +400,23 @@
   }
 
   def add_abbrevs(abbrevs: List[(String, String)]): Completion =
-  {
-    val words =
-      for ((abbr, text) <- abbrevs if Completion.Word_Parsers.is_word(abbr))
-        yield (abbr, text)
-    val abbrs =
-      for ((abbr, text) <- abbrevs if !Completion.Word_Parsers.is_word(abbr))
-        yield (abbr.reverse, (abbr, text))
+    if (abbrevs.isEmpty) this
+    else {
+      val words =
+        for ((abbr, text) <- abbrevs if text != "" && Completion.Word_Parsers.is_word(abbr))
+          yield (abbr, text)
+      val abbrs =
+        for ((abbr, text) <- abbrevs if text != "" && !Completion.Word_Parsers.is_word(abbr))
+          yield (abbr.reverse, (abbr, text))
+      val remove = (for ((abbr, "") <- abbrevs.iterator) yield abbr).toSet
 
-    new Completion(
-      keywords,
-      words_lex ++ words.map(_._1),
-      words_map ++ words,
-      abbrevs_lex ++ abbrs.map(_._1),
-      abbrevs_map ++ abbrs)
-  }
+      new Completion(
+        keywords,
+        words_lex ++ words.map(_._1) -- remove,
+        words_map ++ words -- remove,
+        abbrevs_lex ++ abbrs.map(_._1) -- remove,
+        abbrevs_map ++ abbrs -- remove)
+    }
 
   private def load(): Completion =
     add_symbols().add_abbrevs(Completion.load_abbrevs() ::: Completion.default_abbrevs)

--- a/src/Pure/General/multi_map.scala	Tue Aug 02 11:49:30 2016 +0200
+++ b/src/Pure/General/multi_map.scala	Tue Aug 02 17:35:18 2016 +0200
@@ -8,6 +8,7 @@
 package isabelle
 
 
+import scala.collection.GenTraversableOnce
 import scala.collection.generic.{ImmutableMapFactory, CanBuildFrom}
 
 
@@ -75,6 +76,9 @@
 
   def + [B1 >: B](p: (A, B1)): Multi_Map[A, B1] = insert(p._1, p._2)
 
+  override def ++ [B1 >: B](entries: GenTraversableOnce[(A, B1)]): Multi_Map[A, B1] =
+    (this.asInstanceOf[Multi_Map[A, B1]] /: entries)(_ + _)
+
   def - (a: A): Multi_Map[A, B] =
     if (rep.isDefinedAt(a)) new Multi_Map(rep - a) else this
 }

--- a/src/Pure/General/scan.scala	Tue Aug 02 11:49:30 2016 +0200
+++ b/src/Pure/General/scan.scala	Tue Aug 02 17:35:18 2016 +0200
@@ -8,7 +8,7 @@
 
 
 import scala.annotation.tailrec
-import scala.collection.{IndexedSeq, TraversableOnce}
+import scala.collection.{IndexedSeq, Traversable, TraversableOnce}
 import scala.collection.immutable.PagedSeq
 import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
 import scala.util.parsing.combinator.RegexParsers
@@ -393,6 +393,11 @@
       else if (is_empty) other
       else this ++ other.raw_iterator
 
+    def -- (remove: Traversable[String]): Lexicon =
+      if (remove.exists(contains(_)))
+        Lexicon.empty ++ iterator.filterNot(a => remove.exists(b => a == b))
+      else this
+
 
     /* scan */
 

--- a/src/Pure/Isar/keyword.scala	Tue Aug 02 11:49:30 2016 +0200
+++ b/src/Pure/Isar/keyword.scala	Tue Aug 02 17:35:18 2016 +0200
@@ -163,7 +163,7 @@
 
     def add_keywords(header: Thy_Header.Keywords): Keywords =
       (this /: header) {
-        case (keywords, (name, ((kind, exts), _), _)) =>
+        case (keywords, (name, ((kind, exts), _))) =>
           if (kind == "") keywords + Symbol.decode(name) + Symbol.encode(name)
           else keywords + (Symbol.decode(name), kind, exts) + (Symbol.encode(name), kind, exts)
       }

--- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 02 11:49:30 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 02 17:35:18 2016 +0200
@@ -85,24 +85,35 @@
 
   /* add keywords */
 
-  def + (name: String, kind: String = "", tags: List[String] = Nil, replace: Option[String] = None)
-    : Outer_Syntax =
+  def + (name: String, kind: String = "", tags: List[String] = Nil): Outer_Syntax =
   {
     val keywords1 = keywords + (name, kind, tags)
     val completion1 =
-      if (replace == Some("")) completion
-      else if (replace.isEmpty && Keyword.theory_block.contains(kind))
-        completion + (name, name + "\nbegin\n\u0007\nend") + (name, name)
-      else completion + (name, replace getOrElse name)
+      completion.add_keyword(name).add_abbrevs(
+        if (Keyword.theory_block.contains(kind))
+          List((name, name + "\nbegin\n\u0007\nend"), (name, name))
+        else List((name, name)))
     new Outer_Syntax(keywords1, completion1, language_context, true)
   }
 
   def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
     (this /: keywords) {
-      case (syntax, (name, ((kind, tags), _), replace)) =>
-        syntax +
-          (Symbol.decode(name), kind, tags, replace) +
-          (Symbol.encode(name), kind, tags, replace)
+      case (syntax, (name, ((kind, tags), _))) =>
+        syntax + (Symbol.decode(name), kind, tags) + (Symbol.encode(name), kind, tags)
+    }
+
+  def add_abbrevs(abbrevs: Thy_Header.Abbrevs): Outer_Syntax =
+    if (abbrevs.isEmpty) this
+    else {
+      val completion1 =
+        completion.add_abbrevs(
+          (for ((a, b) <- abbrevs) yield {
+            val a1 = Symbol.decode(a)
+            val a2 = Symbol.encode(a)
+            val b1 = Symbol.decode(b)
+            List((a1, b1), (a2, b1))
+          }).flatten)
+      new Outer_Syntax(keywords, completion1, language_context, has_tokens)
     }
 
 

--- a/src/Pure/PIDE/document.scala	Tue Aug 02 11:49:30 2016 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Aug 02 17:35:18 2016 +0200
@@ -83,6 +83,7 @@
     sealed case class Header(
       imports: List[(Name, Position.T)] = Nil,
       keywords: Thy_Header.Keywords = Nil,
+      abbrevs: Thy_Header.Abbrevs = Nil,
       errors: List[String] = Nil)
     {
       def error(msg: String): Header = copy(errors = errors ::: List(msg))

--- a/src/Pure/PIDE/protocol.scala	Tue Aug 02 11:49:30 2016 +0200
+++ b/src/Pure/PIDE/protocol.scala	Tue Aug 02 17:35:18 2016 +0200
@@ -374,13 +374,12 @@
               val master_dir = File.standard_url(name.master_dir)
               val theory = Long_Name.base_name(name.theory)
               val imports = header.imports.map({ case (a, _) => a.node })
-              val keywords = header.keywords.map({ case (a, b, _) => (a, b) })
               (Nil,
                 pair(Encode.string, pair(Encode.string, pair(list(Encode.string),
                   pair(list(pair(Encode.string,
                     pair(pair(Encode.string, list(Encode.string)), list(Encode.string)))),
                   list(Encode.string)))))(
-                (master_dir, (theory, (imports, (keywords, header.errors)))))) },
+                (master_dir, (theory, (imports, (header.keywords, header.errors)))))) },
           { case Document.Node.Perspective(a, b, c) =>
               (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
                 list(pair(id, pair(Encode.string, list(Encode.string))))(c.dest)) }))

--- a/src/Pure/PIDE/prover.scala	Tue Aug 02 11:49:30 2016 +0200
+++ b/src/Pure/PIDE/prover.scala	Tue Aug 02 17:35:18 2016 +0200
@@ -19,6 +19,7 @@
   {
     def ++ (other: Syntax): Syntax
     def add_keywords(keywords: Thy_Header.Keywords): Syntax
+    def add_abbrevs(abbrevs: Thy_Header.Abbrevs): Syntax
     def parse_spans(input: CharSequence): List[Command_Span.Span]
     def load_command(name: String): Option[List[String]]
     def load_commands_in(text: String): Boolean

--- a/src/Pure/PIDE/resources.scala	Tue Aug 02 11:49:30 2016 +0200
+++ b/src/Pure/PIDE/resources.scala	Tue Aug 02 17:35:18 2016 +0200
@@ -103,7 +103,7 @@
 
         val imports =
           header.imports.map({ case (s, pos) => (import_name(qualifier, node_name, s), pos) })
-        Document.Node.Header(imports, header.keywords)
+        Document.Node.Header(imports, header.keywords, header.abbrevs)
       }
       catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
     }

--- a/src/Pure/Pure.thy	Tue Aug 02 11:49:30 2016 +0200
+++ b/src/Pure/Pure.thy	Tue Aug 02 17:35:18 2016 +0200
@@ -6,7 +6,7 @@
 
 theory Pure
 keywords
-    "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
+    "!!" "!" "+" "--" ":" ";" "<" "<=" "==" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
     "\<subseteq>" "]" "attach" "binder" "for" "if" "in" "infix" "infixl" "infixr" "is"
     "open" "output" "overloaded" "pervasive" "premises" "structure" "unchecked" "when"
   and "private" "qualified" :: before_command
@@ -14,7 +14,7 @@
     "obtains" "shows" "where" "|" :: quasi_command
   and "text" "txt" :: document_body
   and "text_raw" :: document_raw
-  and "default_sort" :: thy_decl == ""
+  and "default_sort" :: thy_decl
   and "typedecl" "type_synonym" "nonterminal" "judgment"
     "consts" "syntax" "no_syntax" "translations" "no_translations"
     "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
@@ -25,7 +25,7 @@
   and "SML_import" "SML_export" :: thy_decl % "ML"
   and "ML_prf" :: prf_decl % "proof"  (* FIXME % "ML" ?? *)
   and "ML_val" "ML_command" :: diag % "ML"
-  and "simproc_setup" :: thy_decl % "ML" == ""
+  and "simproc_setup" :: thy_decl % "ML"
   and "setup" "local_setup" "attribute_setup" "method_setup"
     "declaration" "syntax_declaration"
     "parse_ast_translation" "parse_translation" "print_translation"
@@ -47,9 +47,9 @@
   and "schematic_goal" :: thy_goal
   and "notepad" :: thy_decl_block
   and "have" :: prf_goal % "proof"
-  and "hence" :: prf_goal % "proof" == "then have"
+  and "hence" :: prf_goal % "proof"
   and "show" :: prf_asm_goal % "proof"
-  and "thus" :: prf_asm_goal % "proof" == "then show"
+  and "thus" :: prf_asm_goal % "proof"
   and "then" "from" "with" :: prf_chain % "proof"
   and "note" :: prf_decl % "proof"
   and "supply" :: prf_script % "proof"
@@ -68,7 +68,7 @@
   and "done" :: "qed_script" % "proof"
   and "oops" :: qed_global % "proof"
   and "defer" "prefer" "apply" :: prf_script % "proof"
-  and "apply_end" :: prf_script % "proof" == ""
+  and "apply_end" :: prf_script % "proof"
   and "subgoal" :: prf_script_goal % "proof"
   and "proof" :: prf_block % "proof"
   and "also" "moreover" :: prf_decl % "proof"
@@ -86,11 +86,19 @@
   and "display_drafts" "print_state" :: diag
   and "welcome" :: diag
   and "end" :: thy_end % "theory"
-  and "realizers" :: thy_decl == ""
-  and "realizability" :: thy_decl == ""
+  and "realizers" :: thy_decl
+  and "realizability" :: thy_decl
   and "extract_type" "extract" :: thy_decl
   and "find_theorems" "find_consts" :: diag
   and "named_theorems" :: thy_decl
+abbrevs
+  "default_sort" = ""
+  "simproc_setup" = ""
+  "hence" = "then have"
+  "thus" = "then show"
+  "apply_end" = ""
+  "realizers" = ""
+  "realizability" = ""
 begin
 
 section \<open>Isar commands\<close>

--- a/src/Pure/Thy/thy_header.ML	Tue Aug 02 11:49:30 2016 +0200
+++ b/src/Pure/Thy/thy_header.ML	Tue Aug 02 17:35:18 2016 +0200
@@ -58,6 +58,7 @@
 val theoryN = "theory";
 val importsN = "imports";
 val keywordsN = "keywords";
+val abbrevsN = "abbrevs";
 val beginN = "begin";
 
 val bootstrap_keywords =
@@ -68,11 +69,12 @@
      ((")", @{here}), Keyword.no_spec),
      ((",", @{here}), Keyword.no_spec),
      (("::", @{here}), Keyword.no_spec),
-     (("==", @{here}), Keyword.no_spec),
+     (("=", @{here}), Keyword.no_spec),
      (("and", @{here}), Keyword.no_spec),
      ((beginN, @{here}), Keyword.quasi_command_spec),
      ((importsN, @{here}), Keyword.quasi_command_spec),
      ((keywordsN, @{here}), Keyword.quasi_command_spec),
+     ((abbrevsN, @{here}), Keyword.quasi_command_spec),
      ((chapterN, @{here}), ((Keyword.document_heading, []), [])),
      ((sectionN, @{here}), ((Keyword.document_heading, []), [])),
      ((subsectionN, @{here}), ((Keyword.document_heading, []), [])),
@@ -128,14 +130,12 @@
   Parse.group (fn () => "outer syntax keyword specification")
     (Parse.name -- opt_files -- Parse.tags);
 
-val keyword_compl =
-  Parse.group (fn () => "outer syntax keyword completion") Parse.name;
-
 val keyword_decl =
   Scan.repeat1 (Parse.position Parse.string) --
-  Scan.optional (Parse.$$$ "::" |-- Parse.!!! keyword_spec) Keyword.no_spec --
-  Scan.option (Parse.$$$ "==" |-- Parse.!!! keyword_compl)
-  >> (fn ((names, spec), _) => map (rpair spec) names);
+  Scan.optional (Parse.$$$ "::" |-- Parse.!!! keyword_spec) Keyword.no_spec
+  >> (fn (names, spec) => map (rpair spec) names);
+
+val abbrevs = Scan.repeat1 (Parse.text -- (Parse.$$$ "=" |-- Parse.!!! Parse.text));
 
 val keyword_decls = Parse.and_list1 keyword_decl >> flat;
 
@@ -145,7 +145,8 @@
   Parse.position Parse.theory_name :|-- (fn (name, pos) =>
     imports name --
     Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --|
-    Parse.$$$ beginN >> (fn (imports, keywords) => make (name, pos) imports keywords));
+    (Scan.optional (Parse.$$$ abbrevsN |-- Parse.!!! abbrevs) [] -- Parse.$$$ beginN)
+    >> (fn (imports, keywords) => make (name, pos) imports keywords));
 
 end;
 

--- a/src/Pure/Thy/thy_header.scala	Tue Aug 02 11:49:30 2016 +0200
+++ b/src/Pure/Thy/thy_header.scala	Tue Aug 02 17:35:18 2016 +0200
@@ -17,7 +17,8 @@
 {
   /* bootstrap keywords */
 
-  type Keywords = List[(String, Keyword.Spec, Option[String])]
+  type Keywords = List[(String, Keyword.Spec)]
+  type Abbrevs = List[(String, String)]
 
   val CHAPTER = "chapter"
   val SECTION = "section"
@@ -32,32 +33,34 @@
   val THEORY = "theory"
   val IMPORTS = "imports"
   val KEYWORDS = "keywords"
+  val ABBREVS = "abbrevs"
   val AND = "and"
   val BEGIN = "begin"
 
   private val bootstrap_header: Keywords =
     List(
-      ("%", Keyword.no_spec, None),
-      ("(", Keyword.no_spec, None),
-      (")", Keyword.no_spec, None),
-      (",", Keyword.no_spec, None),
-      ("::", Keyword.no_spec, None),
-      ("==", Keyword.no_spec, None),
-      (AND, Keyword.no_spec, None),
-      (BEGIN, Keyword.quasi_command_spec, None),
-      (IMPORTS, Keyword.quasi_command_spec, None),
-      (KEYWORDS, Keyword.quasi_command_spec, None),
-      (CHAPTER, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
-      (SECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
-      (SUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
-      (SUBSUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
-      (PARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
-      (SUBPARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
-      (TEXT, (((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
-      (TXT, (((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
-      (TEXT_RAW, (((Keyword.DOCUMENT_RAW, Nil), Nil)), None),
-      (THEORY, ((Keyword.THY_BEGIN, Nil), List("theory")), None),
-      ("ML", ((Keyword.THY_DECL, Nil), List("ML")), None))
+      ("%", Keyword.no_spec),
+      ("(", Keyword.no_spec),
+      (")", Keyword.no_spec),
+      (",", Keyword.no_spec),
+      ("::", Keyword.no_spec),
+      ("=", Keyword.no_spec),
+      (AND, Keyword.no_spec),
+      (BEGIN, Keyword.quasi_command_spec),
+      (IMPORTS, Keyword.quasi_command_spec),
+      (KEYWORDS, Keyword.quasi_command_spec),
+      (ABBREVS, Keyword.quasi_command_spec),
+      (CHAPTER, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
+      (SECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
+      (SUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
+      (SUBSUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
+      (PARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
+      (SUBPARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
+      (TEXT, (((Keyword.DOCUMENT_BODY, Nil), Nil))),
+      (TXT, (((Keyword.DOCUMENT_BODY, Nil), Nil))),
+      (TEXT_RAW, (((Keyword.DOCUMENT_RAW, Nil), Nil))),
+      (THEORY, ((Keyword.THY_BEGIN, Nil), List("theory"))),
+      ("ML", ((Keyword.THY_DECL, Nil), List("ML"))))
 
   private val bootstrap_keywords =
     Keyword.Keywords.empty.add_keywords(bootstrap_header)
@@ -106,22 +109,26 @@
 
     val keyword_decl =
       rep1(string) ~
-      opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~
-      opt($$$("==") ~! name ^^ { case _ ~ x => x }) ^^
-      { case xs ~ y ~ z => xs.map((_, y.getOrElse(Keyword.no_spec), z)) }
+      opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ^^
+      { case xs ~ y => xs.map((_, y.getOrElse(Keyword.no_spec))) }
 
     val keyword_decls =
       keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
       { case xs ~ yss => (xs :: yss).flatten }
 
+    val abbrevs =
+      rep1(text ~ ($$$("=") ~! text) ^^ { case a ~ (_ ~ b) => (a, b) })
+
     val args =
       position(theory_name) ~
       (opt($$$(IMPORTS) ~! rep1(position(theory_name))) ^^
         { case None => Nil case Some(_ ~ xs) => xs }) ~
       (opt($$$(KEYWORDS) ~! keyword_decls) ^^
         { case None => Nil case Some(_ ~ xs) => xs }) ~
+      (opt($$$(ABBREVS) ~! abbrevs) ^^
+        { case None => Nil case Some(_ ~ xs) => xs }) ~
       $$$(BEGIN) ^^
-      { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
+      { case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) }
 
     val heading =
       (command(CHAPTER) |
@@ -171,13 +178,15 @@
 sealed case class Thy_Header(
   name: (String, Position.T),
   imports: List[(String, Position.T)],
-  keywords: Thy_Header.Keywords)
+  keywords: Thy_Header.Keywords,
+  abbrevs: Thy_Header.Abbrevs)
 {
   def decode_symbols: Thy_Header =
   {
     val f = Symbol.decode _
-    Thy_Header((f(name._1), name._2), imports.map({ case (a, b) => (f(a), b) }),
-      keywords.map({ case (a, ((x, y), z), c) =>
-        (f(a), ((f(x), y.map(f)), z.map(f)), c.map(f)) }))
+    Thy_Header((f(name._1), name._2),
+      imports.map({ case (a, b) => (f(a), b) }),
+      keywords.map({ case (a, ((b, c), d)) => (f(a), ((f(b), c.map(f)), d.map(f))) }),
+      abbrevs.map({ case (a, b) => (f(a), f(b)) }))
   }
 }

--- a/src/Pure/Thy/thy_info.scala	Tue Aug 02 11:49:30 2016 +0200
+++ b/src/Pure/Thy/thy_info.scala	Tue Aug 02 17:35:18 2016 +0200
@@ -38,24 +38,26 @@
 
   object Dependencies
   {
-    val empty = new Dependencies(Nil, Nil, Set.empty, Multi_Map.empty, Multi_Map.empty)
+    val empty = new Dependencies(Nil, Nil, Nil, Set.empty, Multi_Map.empty, Multi_Map.empty)
   }
 
   final class Dependencies private(
     rev_deps: List[Thy_Info.Dep],
     val keywords: Thy_Header.Keywords,
+    val abbrevs: Thy_Header.Abbrevs,
     val seen: Set[Document.Node.Name],
     val seen_names: Multi_Map[String, Document.Node.Name],
     val seen_positions: Multi_Map[String, Position.T])
   {
     def :: (dep: Thy_Info.Dep): Dependencies =
-      new Dependencies(dep :: rev_deps, dep.header.keywords ::: keywords,
+      new Dependencies(
+        dep :: rev_deps, dep.header.keywords ::: keywords, dep.header.abbrevs ::: abbrevs,
         seen, seen_names, seen_positions)
 
     def + (thy: (Document.Node.Name, Position.T)): Dependencies =
     {
       val (name, pos) = thy
-      new Dependencies(rev_deps, keywords,
+      new Dependencies(rev_deps, keywords, abbrevs,
         seen + name,
         seen_names + (name.theory -> name),
         seen_positions + (name.theory -> pos))
@@ -80,7 +82,8 @@
       header_errors ::: import_errors
     }
 
-    lazy val syntax: Prover.Syntax = resources.base_syntax.add_keywords(keywords)
+    lazy val syntax: Prover.Syntax =
+      resources.base_syntax.add_keywords(keywords).add_abbrevs(abbrevs)
 
     def loaded_theories: Set[String] =
       (resources.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }

--- a/src/Pure/Thy/thy_syntax.scala	Tue Aug 02 11:49:30 2016 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Tue Aug 02 17:35:18 2016 +0200
@@ -84,6 +84,7 @@
           val node1 = node.update_header(header)
           if (node.header.imports.map(_._1) != node1.header.imports.map(_._1) ||
               node.header.keywords != node1.header.keywords ||
+              node.header.abbrevs != node1.header.abbrevs ||
               node.header.errors != node1.header.errors) syntax_changed0 += name
           nodes += (name -> node1)
           doc_edits += (name -> Document.Node.Deps(header))
@@ -100,7 +101,8 @@
         else {
           val header = node.header
           val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax)
-          Some((resources.base_syntax /: imports_syntax)(_ ++ _).add_keywords(header.keywords))
+          Some((resources.base_syntax /: imports_syntax)(_ ++ _)
+            .add_keywords(header.keywords).add_abbrevs(header.abbrevs))
         }
       nodes += (name -> node.update_syntax(syntax))
     }