support 'abbrevs' within theory header;
authorwenzelm
Tue Aug 02 17:35:18 2016 +0200 (2016-08-02)
changeset 6357973939a9b70a3
parent 63578 e8990d0e3965
child 63580 7f06347a5013
support 'abbrevs' within theory header;
simplified 'keywords': no abbreviations here;
NEWS
etc/abbrevs
src/Doc/Isar_Ref/Spec.thy
src/HOL/Library/Simps_Case_Conv.thy
src/HOL/Nonstandard_Analysis/HLim.thy
src/HOL/Nonstandard_Analysis/HSEQ.thy
src/Pure/General/completion.scala
src/Pure/General/multi_map.scala
src/Pure/General/scan.scala
src/Pure/Isar/keyword.scala
src/Pure/Isar/outer_syntax.scala
src/Pure/PIDE/document.scala
src/Pure/PIDE/protocol.scala
src/Pure/PIDE/prover.scala
src/Pure/PIDE/resources.scala
src/Pure/Pure.thy
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_header.scala
src/Pure/Thy/thy_info.scala
src/Pure/Thy/thy_syntax.scala
     1.1 --- a/NEWS	Tue Aug 02 11:49:30 2016 +0200
     1.2 +++ b/NEWS	Tue Aug 02 17:35:18 2016 +0200
     1.3 @@ -111,6 +111,12 @@
     1.4  * Completion templates for commands involving "begin ... end" blocks,
     1.5  e.g. 'context', 'notepad'.
     1.6  
     1.7 +* Additional abbreviations for syntactic completion may be specified in
     1.8 +within the theory header as 'abbrevs', in addition to global
     1.9 +$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs. The
    1.10 +theory syntax for 'keywords' has been simplified accordingly: optional
    1.11 +abbrevs need to go into the new 'abbrevs' section.
    1.12 +
    1.13  
    1.14  *** Isar ***
    1.15  
     2.1 --- a/etc/abbrevs	Tue Aug 02 11:49:30 2016 +0200
     2.2 +++ b/etc/abbrevs	Tue Aug 02 17:35:18 2016 +0200
     2.3 @@ -4,7 +4,3 @@
     2.4  "===>" = "===>"
     2.5  
     2.6  "--->" = "\<midarrow>\<rightarrow>"
     2.7 -
     2.8 -(*HOL-NSA*)
     2.9 -"--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
    2.10 -"--->" = "\<midarrow>\<rightarrow>\<^sub>N\<^sub>S"
     3.1 --- a/src/Doc/Isar_Ref/Spec.thy	Tue Aug 02 11:49:30 2016 +0200
     3.2 +++ b/src/Doc/Isar_Ref/Spec.thy	Tue Aug 02 17:35:18 2016 +0200
     3.3 @@ -58,14 +58,15 @@
     3.4    such a global @{command (global) "end"}.
     3.5  
     3.6    @{rail \<open>
     3.7 -    @@{command theory} @{syntax name} imports? keywords? \<newline> @'begin'
     3.8 +    @@{command theory} @{syntax name} imports? \<newline> keywords? abbrevs? @'begin'
     3.9      ;
    3.10      imports: @'imports' (@{syntax name} +)
    3.11      ;
    3.12      keywords: @'keywords' (keyword_decls + @'and')
    3.13      ;
    3.14 -    keyword_decls: (@{syntax string} +)
    3.15 -      ('::' @{syntax name} @{syntax tags})? ('==' @{syntax name})?
    3.16 +    keyword_decls: (@{syntax string} +) ('::' @{syntax name} @{syntax tags})?
    3.17 +    ;
    3.18 +    abbrevs: @'abbrevs' ((text '=' text) +)
    3.19      ;
    3.20      @@{command thy_deps} (thy_bounds thy_bounds?)?
    3.21      ;
    3.22 @@ -85,7 +86,7 @@
    3.23    based on Isabelle. Regular user theories usually refer to some more complex
    3.24    entry point, such as theory @{theory Main} in Isabelle/HOL.
    3.25  
    3.26 -  The optional @{keyword_def "keywords"} specification declares outer syntax
    3.27 +  The @{keyword_def "keywords"} specification declares outer syntax
    3.28    (\chref{ch:outer-syntax}) that is introduced in this theory later on (rare
    3.29    in end-user applications). Both minor keywords and major keywords of the
    3.30    Isar command language need to be specified, in order to make parsing of
    3.31 @@ -97,8 +98,10 @@
    3.32    @{syntax tags} provide defaults for document preparation
    3.33    (\secref{sec:tags}).
    3.34  
    3.35 -  It is possible to specify an alternative completion via \<^verbatim>\<open>==\<close>~\<open>text\<close>, while
    3.36 -  the default is the corresponding keyword name.
    3.37 +  The @{keyword_def "abbrevs"} specification declares additional abbreviations
    3.38 +  for syntactic completion. The default for a new keyword is just its name,
    3.39 +  but completion may be avoided by defining @{keyword "abbrevs"} with empty
    3.40 +  text.
    3.41    
    3.42    \<^descr> @{command (global) "end"} concludes the current theory definition. Note
    3.43    that some other commands, e.g.\ local theory targets \<^theory_text>\<open>locale\<close> or \<^theory_text>\<open>class\<close>
     4.1 --- a/src/HOL/Library/Simps_Case_Conv.thy	Tue Aug 02 11:49:30 2016 +0200
     4.2 +++ b/src/HOL/Library/Simps_Case_Conv.thy	Tue Aug 02 17:35:18 2016 +0200
     4.3 @@ -5,8 +5,9 @@
     4.4  theory Simps_Case_Conv
     4.5  imports Main
     4.6  keywords
     4.7 -  "simps_of_case" :: thy_decl == "" and
     4.8 -  "case_of_simps" :: thy_decl
     4.9 +  "simps_of_case" "case_of_simps" :: thy_decl
    4.10 +abbrevs
    4.11 +  "simps_of_case" = ""
    4.12  begin
    4.13  
    4.14  ML_file "simps_case_conv.ML"
     5.1 --- a/src/HOL/Nonstandard_Analysis/HLim.thy	Tue Aug 02 11:49:30 2016 +0200
     5.2 +++ b/src/HOL/Nonstandard_Analysis/HLim.thy	Tue Aug 02 17:35:18 2016 +0200
     5.3 @@ -6,7 +6,8 @@
     5.4  section\<open>Limits and Continuity (Nonstandard)\<close>
     5.5  
     5.6  theory HLim
     5.7 -imports Star
     5.8 +  imports Star
     5.9 +  abbrevs "--->" = "\<midarrow>\<rightarrow>\<^sub>N\<^sub>S"
    5.10  begin
    5.11  
    5.12  text\<open>Nonstandard Definitions\<close>
     6.1 --- a/src/HOL/Nonstandard_Analysis/HSEQ.thy	Tue Aug 02 11:49:30 2016 +0200
     6.2 +++ b/src/HOL/Nonstandard_Analysis/HSEQ.thy	Tue Aug 02 17:35:18 2016 +0200
     6.3 @@ -11,7 +11,8 @@
     6.4  section \<open>Sequences and Convergence (Nonstandard)\<close>
     6.5  
     6.6  theory HSEQ
     6.7 -imports Limits NatStar
     6.8 +  imports Limits NatStar
     6.9 +  abbrevs "--->" = "\<longlonglongrightarrow>\<^sub>N\<^sub>S"
    6.10  begin
    6.11  
    6.12  definition
     7.1 --- a/src/Pure/General/completion.scala	Tue Aug 02 11:49:30 2016 +0200
     7.2 +++ b/src/Pure/General/completion.scala	Tue Aug 02 17:35:18 2016 +0200
     7.3 @@ -344,7 +344,7 @@
     7.4  }
     7.5  
     7.6  final class Completion private(
     7.7 -  protected val keywords: Map[String, Boolean] = Map.empty,
     7.8 +  protected val keywords: Set[String] = Set.empty,
     7.9    protected val words_lex: Scan.Lexicon = Scan.Lexicon.empty,
    7.10    protected val words_map: Multi_Map[String, String] = Multi_Map.empty,
    7.11    protected val abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
    7.12 @@ -363,8 +363,7 @@
    7.13      if (this eq other) this
    7.14      else if (is_empty) other
    7.15      else {
    7.16 -      val keywords1 =
    7.17 -        (keywords /: other.keywords) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
    7.18 +      val keywords1 = (keywords /: other.keywords) { case (ks, k) => if (ks(k)) ks else ks + k }
    7.19        val words_lex1 = words_lex ++ other.words_lex
    7.20        val words_map1 = words_map ++ other.words_map
    7.21        val abbrevs_lex1 = abbrevs_lex ++ other.abbrevs_lex
    7.22 @@ -376,19 +375,12 @@
    7.23    /* keywords */
    7.24  
    7.25    private def is_symbol(name: String): Boolean = Symbol.names.isDefinedAt(name)
    7.26 -  private def is_keyword(name: String): Boolean = !is_symbol(name) && keywords.isDefinedAt(name)
    7.27 +  private def is_keyword(name: String): Boolean = !is_symbol(name) && keywords(name)
    7.28    private def is_keyword_template(name: String, template: Boolean): Boolean =
    7.29 -    is_keyword(name) && keywords(name) == template
    7.30 +    is_keyword(name) && (words_map.getOrElse(name, name) != name) == template
    7.31  
    7.32 -  def + (keyword: String, template: String): Completion =
    7.33 -    new Completion(
    7.34 -      keywords + (keyword -> (keyword != template)),
    7.35 -      words_lex + keyword,
    7.36 -      words_map + (keyword -> template),
    7.37 -      abbrevs_lex,
    7.38 -      abbrevs_map)
    7.39 -
    7.40 -  def + (keyword: String): Completion = this + (keyword, keyword)
    7.41 +  def add_keyword(keyword: String): Completion =
    7.42 +    new Completion(keywords + keyword, words_lex, words_map, abbrevs_lex, abbrevs_map)
    7.43  
    7.44  
    7.45    /* symbols and abbrevs */
    7.46 @@ -408,21 +400,23 @@
    7.47    }
    7.48  
    7.49    def add_abbrevs(abbrevs: List[(String, String)]): Completion =
    7.50 -  {
    7.51 -    val words =
    7.52 -      for ((abbr, text) <- abbrevs if Completion.Word_Parsers.is_word(abbr))
    7.53 -        yield (abbr, text)
    7.54 -    val abbrs =
    7.55 -      for ((abbr, text) <- abbrevs if !Completion.Word_Parsers.is_word(abbr))
    7.56 -        yield (abbr.reverse, (abbr, text))
    7.57 +    if (abbrevs.isEmpty) this
    7.58 +    else {
    7.59 +      val words =
    7.60 +        for ((abbr, text) <- abbrevs if text != "" && Completion.Word_Parsers.is_word(abbr))
    7.61 +          yield (abbr, text)
    7.62 +      val abbrs =
    7.63 +        for ((abbr, text) <- abbrevs if text != "" && !Completion.Word_Parsers.is_word(abbr))
    7.64 +          yield (abbr.reverse, (abbr, text))
    7.65 +      val remove = (for ((abbr, "") <- abbrevs.iterator) yield abbr).toSet
    7.66  
    7.67 -    new Completion(
    7.68 -      keywords,
    7.69 -      words_lex ++ words.map(_._1),
    7.70 -      words_map ++ words,
    7.71 -      abbrevs_lex ++ abbrs.map(_._1),
    7.72 -      abbrevs_map ++ abbrs)
    7.73 -  }
    7.74 +      new Completion(
    7.75 +        keywords,
    7.76 +        words_lex ++ words.map(_._1) -- remove,
    7.77 +        words_map ++ words -- remove,
    7.78 +        abbrevs_lex ++ abbrs.map(_._1) -- remove,
    7.79 +        abbrevs_map ++ abbrs -- remove)
    7.80 +    }
    7.81  
    7.82    private def load(): Completion =
    7.83      add_symbols().add_abbrevs(Completion.load_abbrevs() ::: Completion.default_abbrevs)
     8.1 --- a/src/Pure/General/multi_map.scala	Tue Aug 02 11:49:30 2016 +0200
     8.2 +++ b/src/Pure/General/multi_map.scala	Tue Aug 02 17:35:18 2016 +0200
     8.3 @@ -8,6 +8,7 @@
     8.4  package isabelle
     8.5  
     8.6  
     8.7 +import scala.collection.GenTraversableOnce
     8.8  import scala.collection.generic.{ImmutableMapFactory, CanBuildFrom}
     8.9  
    8.10  
    8.11 @@ -75,6 +76,9 @@
    8.12  
    8.13    def + [B1 >: B](p: (A, B1)): Multi_Map[A, B1] = insert(p._1, p._2)
    8.14  
    8.15 +  override def ++ [B1 >: B](entries: GenTraversableOnce[(A, B1)]): Multi_Map[A, B1] =
    8.16 +    (this.asInstanceOf[Multi_Map[A, B1]] /: entries)(_ + _)
    8.17 +
    8.18    def - (a: A): Multi_Map[A, B] =
    8.19      if (rep.isDefinedAt(a)) new Multi_Map(rep - a) else this
    8.20  }
     9.1 --- a/src/Pure/General/scan.scala	Tue Aug 02 11:49:30 2016 +0200
     9.2 +++ b/src/Pure/General/scan.scala	Tue Aug 02 17:35:18 2016 +0200
     9.3 @@ -8,7 +8,7 @@
     9.4  
     9.5  
     9.6  import scala.annotation.tailrec
     9.7 -import scala.collection.{IndexedSeq, TraversableOnce}
     9.8 +import scala.collection.{IndexedSeq, Traversable, TraversableOnce}
     9.9  import scala.collection.immutable.PagedSeq
    9.10  import scala.util.parsing.input.{OffsetPosition, Position => InputPosition, Reader}
    9.11  import scala.util.parsing.combinator.RegexParsers
    9.12 @@ -393,6 +393,11 @@
    9.13        else if (is_empty) other
    9.14        else this ++ other.raw_iterator
    9.15  
    9.16 +    def -- (remove: Traversable[String]): Lexicon =
    9.17 +      if (remove.exists(contains(_)))
    9.18 +        Lexicon.empty ++ iterator.filterNot(a => remove.exists(b => a == b))
    9.19 +      else this
    9.20 +
    9.21  
    9.22      /* scan */
    9.23  
    10.1 --- a/src/Pure/Isar/keyword.scala	Tue Aug 02 11:49:30 2016 +0200
    10.2 +++ b/src/Pure/Isar/keyword.scala	Tue Aug 02 17:35:18 2016 +0200
    10.3 @@ -163,7 +163,7 @@
    10.4  
    10.5      def add_keywords(header: Thy_Header.Keywords): Keywords =
    10.6        (this /: header) {
    10.7 -        case (keywords, (name, ((kind, exts), _), _)) =>
    10.8 +        case (keywords, (name, ((kind, exts), _))) =>
    10.9            if (kind == "") keywords + Symbol.decode(name) + Symbol.encode(name)
   10.10            else keywords + (Symbol.decode(name), kind, exts) + (Symbol.encode(name), kind, exts)
   10.11        }
    11.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 02 11:49:30 2016 +0200
    11.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 02 17:35:18 2016 +0200
    11.3 @@ -85,24 +85,35 @@
    11.4  
    11.5    /* add keywords */
    11.6  
    11.7 -  def + (name: String, kind: String = "", tags: List[String] = Nil, replace: Option[String] = None)
    11.8 -    : Outer_Syntax =
    11.9 +  def + (name: String, kind: String = "", tags: List[String] = Nil): Outer_Syntax =
   11.10    {
   11.11      val keywords1 = keywords + (name, kind, tags)
   11.12      val completion1 =
   11.13 -      if (replace == Some("")) completion
   11.14 -      else if (replace.isEmpty && Keyword.theory_block.contains(kind))
   11.15 -        completion + (name, name + "\nbegin\n\u0007\nend") + (name, name)
   11.16 -      else completion + (name, replace getOrElse name)
   11.17 +      completion.add_keyword(name).add_abbrevs(
   11.18 +        if (Keyword.theory_block.contains(kind))
   11.19 +          List((name, name + "\nbegin\n\u0007\nend"), (name, name))
   11.20 +        else List((name, name)))
   11.21      new Outer_Syntax(keywords1, completion1, language_context, true)
   11.22    }
   11.23  
   11.24    def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
   11.25      (this /: keywords) {
   11.26 -      case (syntax, (name, ((kind, tags), _), replace)) =>
   11.27 -        syntax +
   11.28 -          (Symbol.decode(name), kind, tags, replace) +
   11.29 -          (Symbol.encode(name), kind, tags, replace)
   11.30 +      case (syntax, (name, ((kind, tags), _))) =>
   11.31 +        syntax + (Symbol.decode(name), kind, tags) + (Symbol.encode(name), kind, tags)
   11.32 +    }
   11.33 +
   11.34 +  def add_abbrevs(abbrevs: Thy_Header.Abbrevs): Outer_Syntax =
   11.35 +    if (abbrevs.isEmpty) this
   11.36 +    else {
   11.37 +      val completion1 =
   11.38 +        completion.add_abbrevs(
   11.39 +          (for ((a, b) <- abbrevs) yield {
   11.40 +            val a1 = Symbol.decode(a)
   11.41 +            val a2 = Symbol.encode(a)
   11.42 +            val b1 = Symbol.decode(b)
   11.43 +            List((a1, b1), (a2, b1))
   11.44 +          }).flatten)
   11.45 +      new Outer_Syntax(keywords, completion1, language_context, has_tokens)
   11.46      }
   11.47  
   11.48  
    12.1 --- a/src/Pure/PIDE/document.scala	Tue Aug 02 11:49:30 2016 +0200
    12.2 +++ b/src/Pure/PIDE/document.scala	Tue Aug 02 17:35:18 2016 +0200
    12.3 @@ -83,6 +83,7 @@
    12.4      sealed case class Header(
    12.5        imports: List[(Name, Position.T)] = Nil,
    12.6        keywords: Thy_Header.Keywords = Nil,
    12.7 +      abbrevs: Thy_Header.Abbrevs = Nil,
    12.8        errors: List[String] = Nil)
    12.9      {
   12.10        def error(msg: String): Header = copy(errors = errors ::: List(msg))
    13.1 --- a/src/Pure/PIDE/protocol.scala	Tue Aug 02 11:49:30 2016 +0200
    13.2 +++ b/src/Pure/PIDE/protocol.scala	Tue Aug 02 17:35:18 2016 +0200
    13.3 @@ -374,13 +374,12 @@
    13.4                val master_dir = File.standard_url(name.master_dir)
    13.5                val theory = Long_Name.base_name(name.theory)
    13.6                val imports = header.imports.map({ case (a, _) => a.node })
    13.7 -              val keywords = header.keywords.map({ case (a, b, _) => (a, b) })
    13.8                (Nil,
    13.9                  pair(Encode.string, pair(Encode.string, pair(list(Encode.string),
   13.10                    pair(list(pair(Encode.string,
   13.11                      pair(pair(Encode.string, list(Encode.string)), list(Encode.string)))),
   13.12                    list(Encode.string)))))(
   13.13 -                (master_dir, (theory, (imports, (keywords, header.errors)))))) },
   13.14 +                (master_dir, (theory, (imports, (header.keywords, header.errors)))))) },
   13.15            { case Document.Node.Perspective(a, b, c) =>
   13.16                (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
   13.17                  list(pair(id, pair(Encode.string, list(Encode.string))))(c.dest)) }))
    14.1 --- a/src/Pure/PIDE/prover.scala	Tue Aug 02 11:49:30 2016 +0200
    14.2 +++ b/src/Pure/PIDE/prover.scala	Tue Aug 02 17:35:18 2016 +0200
    14.3 @@ -19,6 +19,7 @@
    14.4    {
    14.5      def ++ (other: Syntax): Syntax
    14.6      def add_keywords(keywords: Thy_Header.Keywords): Syntax
    14.7 +    def add_abbrevs(abbrevs: Thy_Header.Abbrevs): Syntax
    14.8      def parse_spans(input: CharSequence): List[Command_Span.Span]
    14.9      def load_command(name: String): Option[List[String]]
   14.10      def load_commands_in(text: String): Boolean
    15.1 --- a/src/Pure/PIDE/resources.scala	Tue Aug 02 11:49:30 2016 +0200
    15.2 +++ b/src/Pure/PIDE/resources.scala	Tue Aug 02 17:35:18 2016 +0200
    15.3 @@ -103,7 +103,7 @@
    15.4  
    15.5          val imports =
    15.6            header.imports.map({ case (s, pos) => (import_name(qualifier, node_name, s), pos) })
    15.7 -        Document.Node.Header(imports, header.keywords)
    15.8 +        Document.Node.Header(imports, header.keywords, header.abbrevs)
    15.9        }
   15.10        catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
   15.11      }
    16.1 --- a/src/Pure/Pure.thy	Tue Aug 02 11:49:30 2016 +0200
    16.2 +++ b/src/Pure/Pure.thy	Tue Aug 02 17:35:18 2016 +0200
    16.3 @@ -6,7 +6,7 @@
    16.4  
    16.5  theory Pure
    16.6  keywords
    16.7 -    "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
    16.8 +    "!!" "!" "+" "--" ":" ";" "<" "<=" "==" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
    16.9      "\<subseteq>" "]" "attach" "binder" "for" "if" "in" "infix" "infixl" "infixr" "is"
   16.10      "open" "output" "overloaded" "pervasive" "premises" "structure" "unchecked" "when"
   16.11    and "private" "qualified" :: before_command
   16.12 @@ -14,7 +14,7 @@
   16.13      "obtains" "shows" "where" "|" :: quasi_command
   16.14    and "text" "txt" :: document_body
   16.15    and "text_raw" :: document_raw
   16.16 -  and "default_sort" :: thy_decl == ""
   16.17 +  and "default_sort" :: thy_decl
   16.18    and "typedecl" "type_synonym" "nonterminal" "judgment"
   16.19      "consts" "syntax" "no_syntax" "translations" "no_translations"
   16.20      "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
   16.21 @@ -25,7 +25,7 @@
   16.22    and "SML_import" "SML_export" :: thy_decl % "ML"
   16.23    and "ML_prf" :: prf_decl % "proof"  (* FIXME % "ML" ?? *)
   16.24    and "ML_val" "ML_command" :: diag % "ML"
   16.25 -  and "simproc_setup" :: thy_decl % "ML" == ""
   16.26 +  and "simproc_setup" :: thy_decl % "ML"
   16.27    and "setup" "local_setup" "attribute_setup" "method_setup"
   16.28      "declaration" "syntax_declaration"
   16.29      "parse_ast_translation" "parse_translation" "print_translation"
   16.30 @@ -47,9 +47,9 @@
   16.31    and "schematic_goal" :: thy_goal
   16.32    and "notepad" :: thy_decl_block
   16.33    and "have" :: prf_goal % "proof"
   16.34 -  and "hence" :: prf_goal % "proof" == "then have"
   16.35 +  and "hence" :: prf_goal % "proof"
   16.36    and "show" :: prf_asm_goal % "proof"
   16.37 -  and "thus" :: prf_asm_goal % "proof" == "then show"
   16.38 +  and "thus" :: prf_asm_goal % "proof"
   16.39    and "then" "from" "with" :: prf_chain % "proof"
   16.40    and "note" :: prf_decl % "proof"
   16.41    and "supply" :: prf_script % "proof"
   16.42 @@ -68,7 +68,7 @@
   16.43    and "done" :: "qed_script" % "proof"
   16.44    and "oops" :: qed_global % "proof"
   16.45    and "defer" "prefer" "apply" :: prf_script % "proof"
   16.46 -  and "apply_end" :: prf_script % "proof" == ""
   16.47 +  and "apply_end" :: prf_script % "proof"
   16.48    and "subgoal" :: prf_script_goal % "proof"
   16.49    and "proof" :: prf_block % "proof"
   16.50    and "also" "moreover" :: prf_decl % "proof"
   16.51 @@ -86,11 +86,19 @@
   16.52    and "display_drafts" "print_state" :: diag
   16.53    and "welcome" :: diag
   16.54    and "end" :: thy_end % "theory"
   16.55 -  and "realizers" :: thy_decl == ""
   16.56 -  and "realizability" :: thy_decl == ""
   16.57 +  and "realizers" :: thy_decl
   16.58 +  and "realizability" :: thy_decl
   16.59    and "extract_type" "extract" :: thy_decl
   16.60    and "find_theorems" "find_consts" :: diag
   16.61    and "named_theorems" :: thy_decl
   16.62 +abbrevs
   16.63 +  "default_sort" = ""
   16.64 +  "simproc_setup" = ""
   16.65 +  "hence" = "then have"
   16.66 +  "thus" = "then show"
   16.67 +  "apply_end" = ""
   16.68 +  "realizers" = ""
   16.69 +  "realizability" = ""
   16.70  begin
   16.71  
   16.72  section \<open>Isar commands\<close>
    17.1 --- a/src/Pure/Thy/thy_header.ML	Tue Aug 02 11:49:30 2016 +0200
    17.2 +++ b/src/Pure/Thy/thy_header.ML	Tue Aug 02 17:35:18 2016 +0200
    17.3 @@ -58,6 +58,7 @@
    17.4  val theoryN = "theory";
    17.5  val importsN = "imports";
    17.6  val keywordsN = "keywords";
    17.7 +val abbrevsN = "abbrevs";
    17.8  val beginN = "begin";
    17.9  
   17.10  val bootstrap_keywords =
   17.11 @@ -68,11 +69,12 @@
   17.12       ((")", @{here}), Keyword.no_spec),
   17.13       ((",", @{here}), Keyword.no_spec),
   17.14       (("::", @{here}), Keyword.no_spec),
   17.15 -     (("==", @{here}), Keyword.no_spec),
   17.16 +     (("=", @{here}), Keyword.no_spec),
   17.17       (("and", @{here}), Keyword.no_spec),
   17.18       ((beginN, @{here}), Keyword.quasi_command_spec),
   17.19       ((importsN, @{here}), Keyword.quasi_command_spec),
   17.20       ((keywordsN, @{here}), Keyword.quasi_command_spec),
   17.21 +     ((abbrevsN, @{here}), Keyword.quasi_command_spec),
   17.22       ((chapterN, @{here}), ((Keyword.document_heading, []), [])),
   17.23       ((sectionN, @{here}), ((Keyword.document_heading, []), [])),
   17.24       ((subsectionN, @{here}), ((Keyword.document_heading, []), [])),
   17.25 @@ -128,14 +130,12 @@
   17.26    Parse.group (fn () => "outer syntax keyword specification")
   17.27      (Parse.name -- opt_files -- Parse.tags);
   17.28  
   17.29 -val keyword_compl =
   17.30 -  Parse.group (fn () => "outer syntax keyword completion") Parse.name;
   17.31 -
   17.32  val keyword_decl =
   17.33    Scan.repeat1 (Parse.position Parse.string) --
   17.34 -  Scan.optional (Parse.$$$ "::" |-- Parse.!!! keyword_spec) Keyword.no_spec --
   17.35 -  Scan.option (Parse.$$$ "==" |-- Parse.!!! keyword_compl)
   17.36 -  >> (fn ((names, spec), _) => map (rpair spec) names);
   17.37 +  Scan.optional (Parse.$$$ "::" |-- Parse.!!! keyword_spec) Keyword.no_spec
   17.38 +  >> (fn (names, spec) => map (rpair spec) names);
   17.39 +
   17.40 +val abbrevs = Scan.repeat1 (Parse.text -- (Parse.$$$ "=" |-- Parse.!!! Parse.text));
   17.41  
   17.42  val keyword_decls = Parse.and_list1 keyword_decl >> flat;
   17.43  
   17.44 @@ -145,7 +145,8 @@
   17.45    Parse.position Parse.theory_name :|-- (fn (name, pos) =>
   17.46      imports name --
   17.47      Scan.optional (Parse.$$$ keywordsN |-- Parse.!!! keyword_decls) [] --|
   17.48 -    Parse.$$$ beginN >> (fn (imports, keywords) => make (name, pos) imports keywords));
   17.49 +    (Scan.optional (Parse.$$$ abbrevsN |-- Parse.!!! abbrevs) [] -- Parse.$$$ beginN)
   17.50 +    >> (fn (imports, keywords) => make (name, pos) imports keywords));
   17.51  
   17.52  end;
   17.53  
    18.1 --- a/src/Pure/Thy/thy_header.scala	Tue Aug 02 11:49:30 2016 +0200
    18.2 +++ b/src/Pure/Thy/thy_header.scala	Tue Aug 02 17:35:18 2016 +0200
    18.3 @@ -17,7 +17,8 @@
    18.4  {
    18.5    /* bootstrap keywords */
    18.6  
    18.7 -  type Keywords = List[(String, Keyword.Spec, Option[String])]
    18.8 +  type Keywords = List[(String, Keyword.Spec)]
    18.9 +  type Abbrevs = List[(String, String)]
   18.10  
   18.11    val CHAPTER = "chapter"
   18.12    val SECTION = "section"
   18.13 @@ -32,32 +33,34 @@
   18.14    val THEORY = "theory"
   18.15    val IMPORTS = "imports"
   18.16    val KEYWORDS = "keywords"
   18.17 +  val ABBREVS = "abbrevs"
   18.18    val AND = "and"
   18.19    val BEGIN = "begin"
   18.20  
   18.21    private val bootstrap_header: Keywords =
   18.22      List(
   18.23 -      ("%", Keyword.no_spec, None),
   18.24 -      ("(", Keyword.no_spec, None),
   18.25 -      (")", Keyword.no_spec, None),
   18.26 -      (",", Keyword.no_spec, None),
   18.27 -      ("::", Keyword.no_spec, None),
   18.28 -      ("==", Keyword.no_spec, None),
   18.29 -      (AND, Keyword.no_spec, None),
   18.30 -      (BEGIN, Keyword.quasi_command_spec, None),
   18.31 -      (IMPORTS, Keyword.quasi_command_spec, None),
   18.32 -      (KEYWORDS, Keyword.quasi_command_spec, None),
   18.33 -      (CHAPTER, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
   18.34 -      (SECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
   18.35 -      (SUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
   18.36 -      (SUBSUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
   18.37 -      (PARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
   18.38 -      (SUBPARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
   18.39 -      (TEXT, (((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
   18.40 -      (TXT, (((Keyword.DOCUMENT_BODY, Nil), Nil)), None),
   18.41 -      (TEXT_RAW, (((Keyword.DOCUMENT_RAW, Nil), Nil)), None),
   18.42 -      (THEORY, ((Keyword.THY_BEGIN, Nil), List("theory")), None),
   18.43 -      ("ML", ((Keyword.THY_DECL, Nil), List("ML")), None))
   18.44 +      ("%", Keyword.no_spec),
   18.45 +      ("(", Keyword.no_spec),
   18.46 +      (")", Keyword.no_spec),
   18.47 +      (",", Keyword.no_spec),
   18.48 +      ("::", Keyword.no_spec),
   18.49 +      ("=", Keyword.no_spec),
   18.50 +      (AND, Keyword.no_spec),
   18.51 +      (BEGIN, Keyword.quasi_command_spec),
   18.52 +      (IMPORTS, Keyword.quasi_command_spec),
   18.53 +      (KEYWORDS, Keyword.quasi_command_spec),
   18.54 +      (ABBREVS, Keyword.quasi_command_spec),
   18.55 +      (CHAPTER, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
   18.56 +      (SECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
   18.57 +      (SUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
   18.58 +      (SUBSUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
   18.59 +      (PARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
   18.60 +      (SUBPARAGRAPH, (((Keyword.DOCUMENT_HEADING, Nil), Nil))),
   18.61 +      (TEXT, (((Keyword.DOCUMENT_BODY, Nil), Nil))),
   18.62 +      (TXT, (((Keyword.DOCUMENT_BODY, Nil), Nil))),
   18.63 +      (TEXT_RAW, (((Keyword.DOCUMENT_RAW, Nil), Nil))),
   18.64 +      (THEORY, ((Keyword.THY_BEGIN, Nil), List("theory"))),
   18.65 +      ("ML", ((Keyword.THY_DECL, Nil), List("ML"))))
   18.66  
   18.67    private val bootstrap_keywords =
   18.68      Keyword.Keywords.empty.add_keywords(bootstrap_header)
   18.69 @@ -106,22 +109,26 @@
   18.70  
   18.71      val keyword_decl =
   18.72        rep1(string) ~
   18.73 -      opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ~
   18.74 -      opt($$$("==") ~! name ^^ { case _ ~ x => x }) ^^
   18.75 -      { case xs ~ y ~ z => xs.map((_, y.getOrElse(Keyword.no_spec), z)) }
   18.76 +      opt($$$("::") ~! keyword_spec ^^ { case _ ~ x => x }) ^^
   18.77 +      { case xs ~ y => xs.map((_, y.getOrElse(Keyword.no_spec))) }
   18.78  
   18.79      val keyword_decls =
   18.80        keyword_decl ~ rep($$$(AND) ~! keyword_decl ^^ { case _ ~ x => x }) ^^
   18.81        { case xs ~ yss => (xs :: yss).flatten }
   18.82  
   18.83 +    val abbrevs =
   18.84 +      rep1(text ~ ($$$("=") ~! text) ^^ { case a ~ (_ ~ b) => (a, b) })
   18.85 +
   18.86      val args =
   18.87        position(theory_name) ~
   18.88        (opt($$$(IMPORTS) ~! rep1(position(theory_name))) ^^
   18.89          { case None => Nil case Some(_ ~ xs) => xs }) ~
   18.90        (opt($$$(KEYWORDS) ~! keyword_decls) ^^
   18.91          { case None => Nil case Some(_ ~ xs) => xs }) ~
   18.92 +      (opt($$$(ABBREVS) ~! abbrevs) ^^
   18.93 +        { case None => Nil case Some(_ ~ xs) => xs }) ~
   18.94        $$$(BEGIN) ^^
   18.95 -      { case x ~ ys ~ zs ~ _ => Thy_Header(x, ys, zs) }
   18.96 +      { case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) }
   18.97  
   18.98      val heading =
   18.99        (command(CHAPTER) |
  18.100 @@ -171,13 +178,15 @@
  18.101  sealed case class Thy_Header(
  18.102    name: (String, Position.T),
  18.103    imports: List[(String, Position.T)],
  18.104 -  keywords: Thy_Header.Keywords)
  18.105 +  keywords: Thy_Header.Keywords,
  18.106 +  abbrevs: Thy_Header.Abbrevs)
  18.107  {
  18.108    def decode_symbols: Thy_Header =
  18.109    {
  18.110      val f = Symbol.decode _
  18.111 -    Thy_Header((f(name._1), name._2), imports.map({ case (a, b) => (f(a), b) }),
  18.112 -      keywords.map({ case (a, ((x, y), z), c) =>
  18.113 -        (f(a), ((f(x), y.map(f)), z.map(f)), c.map(f)) }))
  18.114 +    Thy_Header((f(name._1), name._2),
  18.115 +      imports.map({ case (a, b) => (f(a), b) }),
  18.116 +      keywords.map({ case (a, ((b, c), d)) => (f(a), ((f(b), c.map(f)), d.map(f))) }),
  18.117 +      abbrevs.map({ case (a, b) => (f(a), f(b)) }))
  18.118    }
  18.119  }
    19.1 --- a/src/Pure/Thy/thy_info.scala	Tue Aug 02 11:49:30 2016 +0200
    19.2 +++ b/src/Pure/Thy/thy_info.scala	Tue Aug 02 17:35:18 2016 +0200
    19.3 @@ -38,24 +38,26 @@
    19.4  
    19.5    object Dependencies
    19.6    {
    19.7 -    val empty = new Dependencies(Nil, Nil, Set.empty, Multi_Map.empty, Multi_Map.empty)
    19.8 +    val empty = new Dependencies(Nil, Nil, Nil, Set.empty, Multi_Map.empty, Multi_Map.empty)
    19.9    }
   19.10  
   19.11    final class Dependencies private(
   19.12      rev_deps: List[Thy_Info.Dep],
   19.13      val keywords: Thy_Header.Keywords,
   19.14 +    val abbrevs: Thy_Header.Abbrevs,
   19.15      val seen: Set[Document.Node.Name],
   19.16      val seen_names: Multi_Map[String, Document.Node.Name],
   19.17      val seen_positions: Multi_Map[String, Position.T])
   19.18    {
   19.19      def :: (dep: Thy_Info.Dep): Dependencies =
   19.20 -      new Dependencies(dep :: rev_deps, dep.header.keywords ::: keywords,
   19.21 +      new Dependencies(
   19.22 +        dep :: rev_deps, dep.header.keywords ::: keywords, dep.header.abbrevs ::: abbrevs,
   19.23          seen, seen_names, seen_positions)
   19.24  
   19.25      def + (thy: (Document.Node.Name, Position.T)): Dependencies =
   19.26      {
   19.27        val (name, pos) = thy
   19.28 -      new Dependencies(rev_deps, keywords,
   19.29 +      new Dependencies(rev_deps, keywords, abbrevs,
   19.30          seen + name,
   19.31          seen_names + (name.theory -> name),
   19.32          seen_positions + (name.theory -> pos))
   19.33 @@ -80,7 +82,8 @@
   19.34        header_errors ::: import_errors
   19.35      }
   19.36  
   19.37 -    lazy val syntax: Prover.Syntax = resources.base_syntax.add_keywords(keywords)
   19.38 +    lazy val syntax: Prover.Syntax =
   19.39 +      resources.base_syntax.add_keywords(keywords).add_abbrevs(abbrevs)
   19.40  
   19.41      def loaded_theories: Set[String] =
   19.42        (resources.loaded_theories /: rev_deps) { case (loaded, dep) => loaded + dep.name.theory }
    20.1 --- a/src/Pure/Thy/thy_syntax.scala	Tue Aug 02 11:49:30 2016 +0200
    20.2 +++ b/src/Pure/Thy/thy_syntax.scala	Tue Aug 02 17:35:18 2016 +0200
    20.3 @@ -84,6 +84,7 @@
    20.4            val node1 = node.update_header(header)
    20.5            if (node.header.imports.map(_._1) != node1.header.imports.map(_._1) ||
    20.6                node.header.keywords != node1.header.keywords ||
    20.7 +              node.header.abbrevs != node1.header.abbrevs ||
    20.8                node.header.errors != node1.header.errors) syntax_changed0 += name
    20.9            nodes += (name -> node1)
   20.10            doc_edits += (name -> Document.Node.Deps(header))
   20.11 @@ -100,7 +101,8 @@
   20.12          else {
   20.13            val header = node.header
   20.14            val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax)
   20.15 -          Some((resources.base_syntax /: imports_syntax)(_ ++ _).add_keywords(header.keywords))
   20.16 +          Some((resources.base_syntax /: imports_syntax)(_ ++ _)
   20.17 +            .add_keywords(header.keywords).add_abbrevs(header.abbrevs))
   20.18          }
   20.19        nodes += (name -> node.update_syntax(syntax))
   20.20      }