--- a/NEWS Tue Dec 29 16:23:34 2015 +0100
+++ b/NEWS Tue Dec 29 17:36:18 2015 +0100
@@ -38,6 +38,9 @@
always possible, independently of the language context. It is never
implicit: a popup will show up unconditionally.
+* Additional abbreviations for syntactic completion may be specified in
+$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs.
+
* Improved scheduling for urgent print tasks (e.g. command state output,
interactive queries) wrt. long-running background tasks.
--- a/etc/settings Tue Dec 29 16:23:34 2015 +0100
+++ b/etc/settings Tue Dec 29 17:36:18 2015 +0100
@@ -121,10 +121,11 @@
###
-### Rendering information
+### Symbol rendering and abbreviations
###
ISABELLE_SYMBOLS="$ISABELLE_HOME/etc/symbols:$ISABELLE_HOME_USER/etc/symbols"
+ISABELLE_ABBREVS="$ISABELLE_HOME/etc/abbrevs:$ISABELLE_HOME_USER/etc/abbrevs"
###
--- a/src/Doc/JEdit/JEdit.thy Tue Dec 29 16:23:34 2015 +0100
+++ b/src/Doc/JEdit/JEdit.thy Tue Dec 29 17:36:18 2015 +0100
@@ -1167,6 +1167,16 @@
aggressively, except for single-character abbreviations like \<^verbatim>\<open>!\<close> above.
\<^medskip>
+ Additional abbreviations may be specified in @{file
+ "$ISABELLE_HOME/etc/abbrevs"} and @{file_unchecked
+ "$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 @{file_unchecked
+ "etc/symbols"}.
+
+ \<^medskip>
Symbol completion depends on the semantic language context
(\secref{sec:completion-context}), to enable or disable that aspect for a
particular sub-language of Isabelle. For example, symbol completion is
--- a/src/Pure/General/completion.scala Tue Dec 29 16:23:34 2015 +0100
+++ b/src/Pure/General/completion.scala Tue Dec 29 17:36:18 2015 +0100
@@ -244,7 +244,7 @@
/* init */
val empty: Completion = new Completion()
- def init(): Completion = empty.add_symbols()
+ def init(): Completion = empty.load()
/* word parsers */
@@ -295,6 +295,36 @@
/* 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
+ symbol_abbrevs ::: more_abbrevs
+ }
+
private val caret_indicator = '\u0007'
private val antiquote = "@{"
@@ -356,23 +386,24 @@
def + (keyword: String): Completion = this + (keyword, keyword)
- /* symbols with abbreviations */
+ /* load symbols and abbrevs */
- private def add_symbols(): Completion =
+ private def load(): Completion =
{
+ val abbrevs = Completion.load_abbrevs()
+
val words =
(for ((sym, _) <- Symbol.names.toList) yield (sym, sym)) :::
(for ((sym, name) <- Symbol.names.toList) yield ("\\" + name, sym)) :::
- (for ((sym, abbr) <- Symbol.abbrevs.toList if Completion.Word_Parsers.is_word(abbr))
- yield (abbr, sym))
+ (for ((abbr, text) <- abbrevs if Completion.Word_Parsers.is_word(abbr)) yield (abbr, text))
- val symbol_abbrs =
- (for ((sym, abbr) <- Symbol.abbrevs.iterator if !Completion.Word_Parsers.is_word(abbr))
- yield (abbr, sym)).toList
+ val non_word_abbrs =
+ (for ((abbr, text) <- abbrevs if !Completion.Word_Parsers.is_word(abbr))
+ yield (abbr, text)).toList
val abbrs =
- for ((abbr, sym) <- symbol_abbrs ::: Completion.default_abbrs)
- yield (abbr.reverse, (abbr, sym))
+ for ((abbr, text) <- non_word_abbrs ::: Completion.default_abbrs)
+ yield (abbr.reverse, (abbr, text))
new Completion(
keywords,