discontinued global etc/abbrevs;
authorwenzelm
Wed Sep 14 14:37:38 2016 +0200 (2016-09-14)
changeset 63871f745c6e683b7
parent 63870 6db1aac936db
child 63872 7dd5297d87fa
discontinued global etc/abbrevs;
NEWS
etc/abbrevs
etc/settings
src/Doc/JEdit/JEdit.thy
src/Pure/General/completion.scala
src/Pure/Pure.thy
     1.1 --- a/NEWS	Wed Sep 14 14:17:32 2016 +0200
     1.2 +++ b/NEWS	Wed Sep 14 14:37:38 2016 +0200
     1.3 @@ -146,10 +146,13 @@
     1.4  e.g. 'context', 'notepad'.
     1.5  
     1.6  * Additional abbreviations for syntactic completion may be specified
     1.7 -within the theory header as 'abbrevs', in addition to global
     1.8 -$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs as
     1.9 -before. The theory syntax for 'keywords' has been simplified
    1.10 -accordingly: optional abbrevs need to go into the new 'abbrevs' section.
    1.11 +within the theory header as 'abbrevs'. The theory syntax for 'keywords'
    1.12 +has been simplified accordingly: optional abbrevs need to go into the
    1.13 +new 'abbrevs' section.
    1.14 +
    1.15 +* Global abbreviations via $ISABELLE_HOME/etc/abbrevs and
    1.16 +$ISABELLE_HOME_USER/etc/abbrevs are no longer supported. Minor
    1.17 +INCOMPATIBILITY, use 'abbrevs' within theory header instead.
    1.18  
    1.19  * ML and document antiquotations for file-systems paths are more uniform
    1.20  and diverse:
     2.1 --- a/etc/abbrevs	Wed Sep 14 14:17:32 2016 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,6 +0,0 @@
     2.4 -(* additional abbreviations for syntactic completion *)
     2.5 -
     2.6 -(*prevent replacement of very long arrows*)
     2.7 -"===>" = "===>"
     2.8 -
     2.9 -"--->" = "\<midarrow>\<rightarrow>"
     3.1 --- a/etc/settings	Wed Sep 14 14:17:32 2016 +0200
     3.2 +++ b/etc/settings	Wed Sep 14 14:37:38 2016 +0200
     3.3 @@ -121,11 +121,10 @@
     3.4  
     3.5  
     3.6  ###
     3.7 -### Symbol rendering and abbreviations
     3.8 +### Symbol rendering
     3.9  ###
    3.10  
    3.11  ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols"
    3.12 -ISABELLE_ABBREVS="$ISABELLE_HOME/etc/abbrevs:$ISABELLE_HOME_USER/etc/abbrevs"
    3.13  
    3.14  
    3.15  ###
     4.1 --- a/src/Doc/JEdit/JEdit.thy	Wed Sep 14 14:17:32 2016 +0200
     4.2 +++ b/src/Doc/JEdit/JEdit.thy	Wed Sep 14 14:37:38 2016 +0200
     4.3 @@ -1266,15 +1266,6 @@
     4.4    Backslash sequences also help when input is broken, and thus escapes its
     4.5    normal semantic context: e.g.\ antiquotations or string literals in ML,
     4.6    which do not allow arbitrary backslash sequences.
     4.7 -
     4.8 -  \<^medskip>
     4.9 -  Additional abbreviations may be specified in \<^file>\<open>$ISABELLE_HOME/etc/abbrevs\<close>
    4.10 -  and @{path "$ISABELLE_HOME_USER/etc/abbrevs"}. The file content follows
    4.11 -  general Isar outer syntax @{cite "isabelle-isar-ref"}. Abbreviations are
    4.12 -  specified as ``\<open>abbrev\<close>~\<^verbatim>\<open>=\<close>~\<open>text\<close>'' pairs. The replacement \<open>text\<close> may
    4.13 -  consist of more than just one symbol; otherwise the meaning is the same as a
    4.14 -  symbol specification ``\<open>sym\<close>~\<^verbatim>\<open>abbrev:\<close>~\<open>abbrev\<close>'' within @{path
    4.15 -  "etc/symbols"}.
    4.16  \<close>
    4.17  
    4.18  
     5.1 --- a/src/Pure/General/completion.scala	Wed Sep 14 14:17:32 2016 +0200
     5.2 +++ b/src/Pure/General/completion.scala	Wed Sep 14 14:37:38 2016 +0200
     5.3 @@ -246,7 +246,8 @@
     5.4    /* init */
     5.5  
     5.6    val empty: Completion = new Completion()
     5.7 -  def init(): Completion = empty.load()
     5.8 +  def init(): Completion =
     5.9 +    empty.add_symbols.add_abbrevs(Completion.symbol_abbrevs ::: Completion.default_abbrevs)
    5.10  
    5.11  
    5.12    /* word parsers */
    5.13 @@ -295,47 +296,22 @@
    5.14    }
    5.15  
    5.16  
    5.17 -  /* abbreviations */
    5.18 -
    5.19 -  private object Abbrevs_Parser extends Parse.Parser
    5.20 -  {
    5.21 -    private val syntax = Outer_Syntax.empty + "="
    5.22 -
    5.23 -    private val entry: Parser[(String, String)] =
    5.24 -      text ~ ($$$("=") ~! text) ^^ { case a ~ (_ ~ b) => (a, b) }
    5.25 -
    5.26 -    def parse_file(file: Path): List[(String, String)] =
    5.27 -    {
    5.28 -      val toks = Token.explode(syntax.keywords, File.read(file))
    5.29 -      parse_all(rep(entry), Token.reader(toks, Token.Pos.file(file.implode))) match {
    5.30 -        case Success(result, _) => result
    5.31 -        case bad => error(bad.toString)
    5.32 -      }
    5.33 -    }
    5.34 -  }
    5.35 -
    5.36 -  def load_abbrevs(): List[(String, String)] =
    5.37 -  {
    5.38 -    val symbol_abbrevs =
    5.39 -      for ((sym, abbr) <- Symbol.abbrevs.toList) yield (abbr, sym)
    5.40 -    val more_abbrevs =
    5.41 -      for {
    5.42 -        path <- Path.split(Isabelle_System.getenv("ISABELLE_ABBREVS"))
    5.43 -        if path.is_file
    5.44 -        entry <- Abbrevs_Parser.parse_file(path)
    5.45 -      } yield entry
    5.46 -    val remove_abbrevs = (for { (a, b) <- more_abbrevs if b == "" } yield a).toSet
    5.47 -
    5.48 -    (symbol_abbrevs ::: more_abbrevs).filterNot({ case (a, _) => remove_abbrevs.contains(a) })
    5.49 -  }
    5.50 +  /* templates */
    5.51  
    5.52    val caret_indicator = '\u0007'
    5.53 +
    5.54    def split_template(s: String): (String, String) =
    5.55      space_explode(caret_indicator, s) match {
    5.56        case List(s1, s2) => (s1, s2)
    5.57        case _ => (s, "")
    5.58      }
    5.59  
    5.60 +
    5.61 +  /* abbreviations */
    5.62 +
    5.63 +  private def symbol_abbrevs: Thy_Header.Abbrevs =
    5.64 +    for ((sym, abbr) <- Symbol.abbrevs.toList) yield (abbr, sym)
    5.65 +
    5.66    private val antiquote = "@{"
    5.67  
    5.68    private val default_abbrevs =
    5.69 @@ -393,7 +369,7 @@
    5.70  
    5.71    /* symbols and abbrevs */
    5.72  
    5.73 -  def add_symbols(): Completion =
    5.74 +  def add_symbols: Completion =
    5.75    {
    5.76      val words =
    5.77        (for ((sym, _) <- Symbol.names.toList) yield (sym, sym)) :::
    5.78 @@ -429,9 +405,6 @@
    5.79      new Completion(keywords, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
    5.80    }
    5.81  
    5.82 -  private def load(): Completion =
    5.83 -    add_symbols().add_abbrevs(Completion.load_abbrevs() ::: Completion.default_abbrevs)
    5.84 -
    5.85  
    5.86    /* complete */
    5.87  
     6.1 --- a/src/Pure/Pure.thy	Wed Sep 14 14:17:32 2016 +0200
     6.2 +++ b/src/Pure/Pure.thy	Wed Sep 14 14:37:38 2016 +0200
     6.3 @@ -92,6 +92,8 @@
     6.4    and "find_theorems" "find_consts" :: diag
     6.5    and "named_theorems" :: thy_decl
     6.6  abbrevs
     6.7 +  "===>" = "===>"  (*prevent replacement of very long arrows*)
     6.8 +  "--->" = "\<midarrow>\<rightarrow>"
     6.9    "default_sort" = ""
    6.10    "simproc_setup" = ""
    6.11    "hence" = ""