support additional abbrevs;
authorwenzelm
Tue Dec 29 17:36:18 2015 +0100 (2015-12-29)
changeset 6196020c1321378db
parent 61959 364007370bb7
child 61961 c4cc05200337
support additional abbrevs;
NEWS
etc/settings
src/Doc/JEdit/JEdit.thy
src/Pure/General/completion.scala
     1.1 --- a/NEWS	Tue Dec 29 16:23:34 2015 +0100
     1.2 +++ b/NEWS	Tue Dec 29 17:36:18 2015 +0100
     1.3 @@ -38,6 +38,9 @@
     1.4  always possible, independently of the language context. It is never
     1.5  implicit: a popup will show up unconditionally.
     1.6  
     1.7 +* Additional abbreviations for syntactic completion may be specified in
     1.8 +$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs.
     1.9 +
    1.10  * Improved scheduling for urgent print tasks (e.g. command state output,
    1.11  interactive queries) wrt. long-running background tasks.
    1.12  
     2.1 --- a/etc/settings	Tue Dec 29 16:23:34 2015 +0100
     2.2 +++ b/etc/settings	Tue Dec 29 17:36:18 2015 +0100
     2.3 @@ -121,10 +121,11 @@
     2.4  
     2.5  
     2.6  ###
     2.7 -### Rendering information
     2.8 +### Symbol rendering and abbreviations
     2.9  ###
    2.10  
    2.11  ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols"
    2.12 +ISABELLE_ABBREVS="$ISABELLE_HOME/etc/abbrevs:$ISABELLE_HOME_USER/etc/abbrevs"
    2.13  
    2.14  
    2.15  ###
     3.1 --- a/src/Doc/JEdit/JEdit.thy	Tue Dec 29 16:23:34 2015 +0100
     3.2 +++ b/src/Doc/JEdit/JEdit.thy	Tue Dec 29 17:36:18 2015 +0100
     3.3 @@ -1167,6 +1167,16 @@
     3.4    aggressively, except for single-character abbreviations like \<^verbatim>\<open>!\<close> above.
     3.5  
     3.6    \<^medskip>
     3.7 +  Additional abbreviations may be specified in @{file
     3.8 +  "$ISABELLE_HOME/etc/abbrevs"} and @{file_unchecked
     3.9 +  "$ISABELLE_HOME_USER/etc/abbrevs"}. The file content follows general Isar
    3.10 +  outer syntax @{cite "isabelle-isar-ref"}. Abbreviations are specified as
    3.11 +  ``\<open>abbrev\<close>~\<^verbatim>\<open>=\<close>~\<open>text\<close>'' pairs. The replacement \<open>text\<close> may consist of more
    3.12 +  than just one symbol; otherwise the meaning is the same as a symbol
    3.13 +  specification ``\<open>sym\<close>~\<^verbatim>\<open>abbrev:\<close>~\<open>abbrev\<close>'' within @{file_unchecked
    3.14 +  "etc/symbols"}.
    3.15 +
    3.16 +  \<^medskip>
    3.17    Symbol completion depends on the semantic language context
    3.18    (\secref{sec:completion-context}), to enable or disable that aspect for a
    3.19    particular sub-language of Isabelle. For example, symbol completion is
     4.1 --- a/src/Pure/General/completion.scala	Tue Dec 29 16:23:34 2015 +0100
     4.2 +++ b/src/Pure/General/completion.scala	Tue Dec 29 17:36:18 2015 +0100
     4.3 @@ -244,7 +244,7 @@
     4.4    /* init */
     4.5  
     4.6    val empty: Completion = new Completion()
     4.7 -  def init(): Completion = empty.add_symbols()
     4.8 +  def init(): Completion = empty.load()
     4.9  
    4.10  
    4.11    /* word parsers */
    4.12 @@ -295,6 +295,36 @@
    4.13  
    4.14    /* abbreviations */
    4.15  
    4.16 +  private object Abbrevs_Parser extends Parse.Parser
    4.17 +  {
    4.18 +    private val syntax = Outer_Syntax.empty + "="
    4.19 +
    4.20 +    private val entry: Parser[(String, String)] =
    4.21 +      text ~ ($$$("=") ~! text) ^^ { case a ~ (_ ~ b) => (a, b) }
    4.22 +
    4.23 +    def parse_file(file: Path): List[(String, String)] =
    4.24 +    {
    4.25 +      val toks = Token.explode(syntax.keywords, File.read(file))
    4.26 +      parse_all(rep(entry), Token.reader(toks, Token.Pos.file(file.implode))) match {
    4.27 +        case Success(result, _) => result
    4.28 +        case bad => error(bad.toString)
    4.29 +      }
    4.30 +    }
    4.31 +  }
    4.32 +
    4.33 +  def load_abbrevs(): List[(String, String)] =
    4.34 +  {
    4.35 +    val symbol_abbrevs =
    4.36 +      for ((sym, abbr) <- Symbol.abbrevs.toList) yield (abbr, sym)
    4.37 +    val more_abbrevs =
    4.38 +      for {
    4.39 +        path <- Path.split(Isabelle_System.getenv("ISABELLE_ABBREVS"))
    4.40 +        if path.is_file
    4.41 +        entry <- Abbrevs_Parser.parse_file(path)
    4.42 +      } yield entry
    4.43 +    symbol_abbrevs ::: more_abbrevs
    4.44 +  }
    4.45 +
    4.46    private val caret_indicator = '\u0007'
    4.47    private val antiquote = "@{"
    4.48  
    4.49 @@ -356,23 +386,24 @@
    4.50    def + (keyword: String): Completion = this + (keyword, keyword)
    4.51  
    4.52  
    4.53 -  /* symbols with abbreviations */
    4.54 +  /* load symbols and abbrevs */
    4.55  
    4.56 -  private def add_symbols(): Completion =
    4.57 +  private def load(): Completion =
    4.58    {
    4.59 +    val abbrevs = Completion.load_abbrevs()
    4.60 +
    4.61      val words =
    4.62        (for ((sym, _) <- Symbol.names.toList) yield (sym, sym)) :::
    4.63        (for ((sym, name) <- Symbol.names.toList) yield ("\\" + name, sym)) :::
    4.64 -      (for ((sym, abbr) <- Symbol.abbrevs.toList if Completion.Word_Parsers.is_word(abbr))
    4.65 -        yield (abbr, sym))
    4.66 +      (for ((abbr, text) <- abbrevs if Completion.Word_Parsers.is_word(abbr)) yield (abbr, text))
    4.67  
    4.68 -    val symbol_abbrs =
    4.69 -      (for ((sym, abbr) <- Symbol.abbrevs.iterator if !Completion.Word_Parsers.is_word(abbr))
    4.70 -        yield (abbr, sym)).toList
    4.71 +    val non_word_abbrs =
    4.72 +      (for ((abbr, text) <- abbrevs if !Completion.Word_Parsers.is_word(abbr))
    4.73 +        yield (abbr, text)).toList
    4.74  
    4.75      val abbrs =
    4.76 -      for ((abbr, sym) <- symbol_abbrs ::: Completion.default_abbrs)
    4.77 -        yield (abbr.reverse, (abbr, sym))
    4.78 +      for ((abbr, text) <- non_word_abbrs ::: Completion.default_abbrs)
    4.79 +        yield (abbr.reverse, (abbr, text))
    4.80  
    4.81      new Completion(
    4.82        keywords,