--- a/NEWS Wed Sep 14 16:24:51 2016 +0200
+++ b/NEWS Wed Sep 14 22:07:11 2016 +0200
@@ -79,6 +79,11 @@
*** Prover IDE -- Isabelle/Scala/jEdit ***
+* Dockable window "Symbols" also provides access to 'abbrevs' from the
+outer syntax of the current theory buffer. This provides clickable
+syntax templates, including entries with empty abbrevs name (which are
+inaccessible via keyboard completion).
+
* Cartouche abbreviations work both for " and ` to accomodate typical
situations where old ASCII notation may be updated.
@@ -146,10 +151,13 @@
e.g. 'context', 'notepad'.
* Additional abbreviations for syntactic completion may be specified
-within the theory header as 'abbrevs', in addition to global
-$ISABELLE_HOME/etc/abbrevs and $ISABELLE_HOME_USER/etc/abbrevs as
-before. The theory syntax for 'keywords' has been simplified
-accordingly: optional abbrevs need to go into the new 'abbrevs' section.
+within the theory header as 'abbrevs'. The theory syntax for 'keywords'
+has been simplified accordingly: optional abbrevs need to go into the
+new 'abbrevs' section.
+
+* Global abbreviations via $ISABELLE_HOME/etc/abbrevs and
+$ISABELLE_HOME_USER/etc/abbrevs are no longer supported. Minor
+INCOMPATIBILITY, use 'abbrevs' within theory header instead.
* ML and document antiquotations for file-systems paths are more uniform
and diverse:
--- a/etc/abbrevs Wed Sep 14 16:24:51 2016 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-(* additional abbreviations for syntactic completion *)
-
-(*prevent replacement of very long arrows*)
-"===>" = "===>"
-
-"--->" = "\<midarrow>\<rightarrow>"
--- a/etc/settings Wed Sep 14 16:24:51 2016 +0200
+++ b/etc/settings Wed Sep 14 22:07:11 2016 +0200
@@ -121,11 +121,10 @@
###
-### Symbol rendering and abbreviations
+### Symbol rendering
###
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 Wed Sep 14 16:24:51 2016 +0200
+++ b/src/Doc/JEdit/JEdit.thy Wed Sep 14 22:07:11 2016 +0200
@@ -1266,15 +1266,6 @@
Backslash sequences also help when input is broken, and thus escapes its
normal semantic context: e.g.\ antiquotations or string literals in ML,
which do not allow arbitrary backslash sequences.
-
- \<^medskip>
- Additional abbreviations may be specified in \<^file>\<open>$ISABELLE_HOME/etc/abbrevs\<close>
- and @{path "$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 @{path
- "etc/symbols"}.
\<close>
--- a/src/Pure/GUI/gui.scala Wed Sep 14 16:24:51 2016 +0200
+++ b/src/Pure/GUI/gui.scala Wed Sep 14 22:07:11 2016 +0200
@@ -211,6 +211,21 @@
case _ => None
}
+ def traverse_components(component: Component, apply: Component => Unit)
+ {
+ def traverse(comp: Component)
+ {
+ apply(comp)
+ comp match {
+ case cont: Container =>
+ for (i <- 0 until cont.getComponentCount)
+ traverse(cont.getComponent(i))
+ case _ =>
+ }
+ }
+ traverse(component)
+ }
+
/* font operations */
--- a/src/Pure/General/completion.scala Wed Sep 14 16:24:51 2016 +0200
+++ b/src/Pure/General/completion.scala Wed Sep 14 22:07:11 2016 +0200
@@ -246,7 +246,8 @@
/* init */
val empty: Completion = new Completion()
- def init(): Completion = empty.load()
+ def init(): Completion =
+ empty.add_symbols.add_abbrevs(Completion.symbol_abbrevs ::: Completion.default_abbrevs)
/* word parsers */
@@ -295,41 +296,22 @@
}
+ /* templates */
+
+ val caret_indicator = '\u0007'
+
+ def split_template(s: String): (String, String) =
+ space_explode(caret_indicator, s) match {
+ case List(s1, s2) => (s1, s2)
+ case _ => (s, "")
+ }
+
+
/* 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)
- }
- }
- }
+ private def symbol_abbrevs: Thy_Header.Abbrevs =
+ for ((sym, abbr) <- Symbol.abbrevs.toList) yield (abbr, sym)
- 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
- val remove_abbrevs = (for { (a, b) <- more_abbrevs if b == "" } yield a).toSet
-
- (symbol_abbrevs ::: more_abbrevs).filterNot({ case (a, _) => remove_abbrevs.contains(a) })
- }
-
- private val caret_indicator = '\u0007'
private val antiquote = "@{"
private val default_abbrevs =
@@ -387,7 +369,7 @@
/* symbols and abbrevs */
- def add_symbols(): Completion =
+ def add_symbols: Completion =
{
val words =
(for ((sym, _) <- Symbol.names.toList) yield (sym, sym)) :::
@@ -405,26 +387,24 @@
(this /: abbrevs)(_.add_abbrev(_))
private def add_abbrev(abbrev: (String, String)): Completion =
- {
- val (abbr, text) = abbrev
- val rev_abbr = abbr.reverse
- val is_word = Completion.Word_Parsers.is_word(abbr)
-
- val (words_lex1, words_map1) =
- if (!is_word) (words_lex, words_map)
- else if (text != "") (words_lex + abbr, words_map + abbrev)
- else (words_lex -- List(abbr), words_map - abbr)
+ abbrev match {
+ case ("", _) => this
+ case (abbr, text) =>
+ val rev_abbr = abbr.reverse
+ val is_word = Completion.Word_Parsers.is_word(abbr)
- val (abbrevs_lex1, abbrevs_map1) =
- if (is_word) (abbrevs_lex, abbrevs_map)
- else if (text != "") (abbrevs_lex + rev_abbr, abbrevs_map + (rev_abbr -> abbrev))
- else (abbrevs_lex -- List(rev_abbr), abbrevs_map - rev_abbr)
+ val (words_lex1, words_map1) =
+ if (!is_word) (words_lex, words_map)
+ else if (text != "") (words_lex + abbr, words_map + abbrev)
+ else (words_lex -- List(abbr), words_map - abbr)
- new Completion(keywords, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
- }
+ val (abbrevs_lex1, abbrevs_map1) =
+ if (is_word) (abbrevs_lex, abbrevs_map)
+ else if (text != "") (abbrevs_lex + rev_abbr, abbrevs_map + (rev_abbr -> abbrev))
+ else (abbrevs_lex -- List(rev_abbr), abbrevs_map - rev_abbr)
- private def load(): Completion =
- add_symbols().add_abbrevs(Completion.load_abbrevs() ::: Completion.default_abbrevs)
+ new Completion(keywords, words_lex1, words_map1, abbrevs_lex1, abbrevs_map1)
+ }
/* complete */
@@ -505,11 +485,7 @@
(complete_word, name0) <- completions
name1 = decode(name0)
if name1 != original
- (s1, s2) =
- space_explode(Completion.caret_indicator, name1) match {
- case List(s1, s2) => (s1, s2)
- case _ => (name1, "")
- }
+ (s1, s2) = Completion.split_template(name1)
move = - s2.length
description =
if (is_symbol(name0)) {
--- a/src/Pure/General/path.scala Wed Sep 14 16:24:51 2016 +0200
+++ b/src/Pure/General/path.scala Wed Sep 14 22:07:11 2016 +0200
@@ -96,7 +96,7 @@
else (List(root_elem(es.head)), es.tail)
val elems = raw_elems.filterNot(s => s.isEmpty || s == ".").map(explode_elem)
- new Path(norm_elems(elems.reverse ::: roots))
+ new Path(norm_elems(elems reverse_::: roots))
}
def is_wellformed(str: String): Boolean =
--- a/src/Pure/Isar/outer_syntax.scala Wed Sep 14 16:24:51 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Wed Sep 14 22:07:11 2016 +0200
@@ -46,6 +46,7 @@
final class Outer_Syntax private(
val keywords: Keyword.Keywords = Keyword.Keywords.empty,
val completion: Completion = Completion.empty,
+ val rev_abbrevs: Thy_Header.Abbrevs = Nil,
val language_context: Completion.Language_Context = Completion.Language_Context.outer,
val has_tokens: Boolean = true)
{
@@ -54,7 +55,7 @@
override def toString: String = keywords.toString
- /* add keywords */
+ /* keywords */
def + (name: String, kind: String = "", tags: List[String] = Nil): Outer_Syntax =
{
@@ -65,7 +66,7 @@
(if (Keyword.theory_block.contains(kind)) List((name, name + "\nbegin\n\u0007\nend"))
else Nil) :::
(if (Completion.Word_Parsers.is_word(name)) List((name, name)) else Nil))
- new Outer_Syntax(keywords1, completion1, language_context, true)
+ new Outer_Syntax(keywords1, completion1, rev_abbrevs, language_context, true)
}
def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
@@ -74,18 +75,24 @@
syntax + (Symbol.decode(name), kind, tags) + (Symbol.encode(name), kind, tags)
}
- def add_abbrevs(abbrevs: Thy_Header.Abbrevs): Outer_Syntax =
- if (abbrevs.isEmpty) this
+
+ /* abbrevs */
+
+ def abbrevs: Thy_Header.Abbrevs = rev_abbrevs.reverse
+
+ def add_abbrevs(new_abbrevs: Thy_Header.Abbrevs): Outer_Syntax =
+ if (new_abbrevs.isEmpty) this
else {
val completion1 =
completion.add_abbrevs(
- (for ((a, b) <- abbrevs) yield {
+ (for ((a, b) <- new_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)
+ val rev_abbrevs1 = Library.distinct(new_abbrevs) reverse_::: rev_abbrevs
+ new Outer_Syntax(keywords, completion1, rev_abbrevs1, language_context, has_tokens)
}
@@ -94,10 +101,11 @@
def ++ (other: Outer_Syntax): Outer_Syntax =
if (this eq other) this
else {
- val keywords1 = keywords ++ other.asInstanceOf[Outer_Syntax].keywords
- val completion1 = completion ++ other.asInstanceOf[Outer_Syntax].completion
+ val keywords1 = keywords ++ other.keywords
+ val completion1 = completion ++ other.completion
+ val rev_abbrevs1 = Library.merge(rev_abbrevs, other.rev_abbrevs)
if ((keywords eq keywords1) && (completion eq completion1)) this
- else new Outer_Syntax(keywords1, completion1, language_context, has_tokens)
+ else new Outer_Syntax(keywords1, completion1, rev_abbrevs1, language_context, has_tokens)
}
@@ -110,13 +118,14 @@
/* language context */
def set_language_context(context: Completion.Language_Context): Outer_Syntax =
- new Outer_Syntax(keywords, completion, context, has_tokens)
+ new Outer_Syntax(keywords, completion, rev_abbrevs, context, has_tokens)
def no_tokens: Outer_Syntax =
{
require(keywords.is_empty)
new Outer_Syntax(
completion = completion,
+ rev_abbrevs = rev_abbrevs,
language_context = language_context,
has_tokens = false)
}
--- a/src/Pure/Pure.thy Wed Sep 14 16:24:51 2016 +0200
+++ b/src/Pure/Pure.thy Wed Sep 14 22:07:11 2016 +0200
@@ -92,6 +92,8 @@
and "find_theorems" "find_consts" :: diag
and "named_theorems" :: thy_decl
abbrevs
+ "===>" = "===>" (*prevent replacement of very long arrows*)
+ "--->" = "\<midarrow>\<rightarrow>"
"default_sort" = ""
"simproc_setup" = ""
"hence" = ""
--- a/src/Pure/Thy/thy_syntax.scala Wed Sep 14 16:24:51 2016 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Wed Sep 14 22:07:11 2016 +0200
@@ -198,7 +198,7 @@
val removed = old_cmds.iterator.filter(!new_cmds.contains(_)).toList
val inserted = new_cmds.iterator.filter(!old_cmds.contains(_)).toList
- removed.reverse.map(cmd => (old_cmds.prev(cmd), None)) :::
+ removed.map(cmd => (old_cmds.prev(cmd), None)) reverse_:::
inserted.map(cmd => (new_cmds.prev(cmd), Some(cmd)))
}
--- a/src/Pure/Tools/build.scala Wed Sep 14 16:24:51 2016 +0200
+++ b/src/Pure/Tools/build.scala Wed Sep 14 22:07:11 2016 +0200
@@ -170,7 +170,7 @@
val loaded_theories = thy_deps.loaded_theories
val keywords = thy_deps.keywords
- val syntax = thy_deps.syntax.asInstanceOf[Outer_Syntax]
+ val syntax = thy_deps.syntax
val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
val loaded_files =
--- a/src/Pure/library.scala Wed Sep 14 16:24:51 2016 +0200
+++ b/src/Pure/library.scala Wed Sep 14 22:07:11 2016 +0200
@@ -198,6 +198,11 @@
def remove[A, B](x: B)(xs: List[A]): List[A] = if (member(xs)(x)) xs.filterNot(_ == x) else xs
def update[A](x: A)(xs: List[A]): List[A] = x :: remove(x)(xs)
+ def merge[A](xs: List[A], ys: List[A]): List[A] =
+ if (xs.eq(ys)) xs
+ else if (xs.isEmpty) ys
+ else ys.foldRight(xs)(Library.insert(_)(_))
+
def distinct[A](xs: List[A]): List[A] =
{
val result = new mutable.ListBuffer[A]
--- a/src/Tools/jEdit/src/isabelle.scala Wed Sep 14 16:24:51 2016 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Wed Sep 14 22:07:11 2016 +0200
@@ -50,7 +50,7 @@
def mode_syntax(mode: String): Option[Outer_Syntax] =
mode match {
- case "isabelle" => Some(PIDE.resources.base_syntax.asInstanceOf[Outer_Syntax])
+ case "isabelle" => Some(PIDE.resources.base_syntax)
case "isabelle-options" => Some(Options.options_syntax)
case "isabelle-root" => Some(Sessions.root_syntax)
case "isabelle-ml" => Some(ml_syntax)
@@ -61,11 +61,13 @@
}
def buffer_syntax(buffer: JEditBuffer): Option[Outer_Syntax] =
- (JEdit_Lib.buffer_mode(buffer), PIDE.document_model(buffer)) match {
- case ("isabelle", Some(model)) =>
- Some(PIDE.session.recent_syntax(model.node_name).asInstanceOf[Outer_Syntax])
- case (mode, _) => mode_syntax(mode)
- }
+ if (buffer == null) None
+ else
+ (JEdit_Lib.buffer_mode(buffer), PIDE.document_model(buffer)) match {
+ case ("isabelle", Some(model)) =>
+ Some(PIDE.session.recent_syntax(model.node_name))
+ case (mode, _) => mode_syntax(mode)
+ }
/* token markers */
--- a/src/Tools/jEdit/src/symbols_dockable.scala Wed Sep 14 16:24:51 2016 +0200
+++ b/src/Tools/jEdit/src/symbols_dockable.scala Wed Sep 14 22:07:11 2016 +0200
@@ -10,22 +10,89 @@
import isabelle._
import scala.swing.event.{SelectionChanged, ValueChanged}
-import scala.swing.{Action, Button, TabbedPane, TextField, BorderPanel, Label, ScrollPane}
+import scala.swing.{Component, Action, Button, TabbedPane, TextField, BorderPanel,
+ Label, ScrollPane}
-import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.{EditBus, EBComponent, EBMessage, View}
class Symbols_Dockable(view: View, position: String) extends Dockable(view, position)
{
+ private def font_size: Int =
+ Font_Info.main_size(PIDE.options.real("jedit_font_scale")).round
+
+
+ /* abbreviations */
+
+ private val abbrevs_panel = new Abbrevs_Panel
+
+ private val abbrevs_refresh_delay =
+ GUI_Thread.delay_last(PIDE.options.seconds("editor_update_delay")) { abbrevs_panel.refresh }
+
+ private class Abbrev_Component(txt: String, abbrs: List[String]) extends Button
+ {
+ def update_font { font = GUI.font(size = font_size) }
+ update_font
+
+ text = "<html>" + HTML.output(Symbol.decode(txt)) + "</html>"
+ action =
+ Action(text) {
+ val text_area = view.getTextArea
+ val (s1, s2) =
+ Completion.split_template(Isabelle_Encoding.maybe_decode(text_area.getBuffer, txt))
+ text_area.setSelectedText(s1 + s2)
+ text_area.moveCaretPosition(text_area.getCaretPosition - s2.length)
+ text_area.requestFocus
+ }
+ tooltip = GUI.tooltip_lines(cat_lines(txt :: abbrs.map(a => "abbrev: " + a)))
+ }
+
+ private class Abbrevs_Panel extends Wrap_Panel
+ {
+ private var abbrevs: Thy_Header.Abbrevs = Nil
+
+ def refresh: Unit = GUI_Thread.require {
+ val abbrevs1 = Isabelle.buffer_syntax(view.getBuffer).getOrElse(Outer_Syntax.empty).abbrevs
+
+ if (abbrevs != abbrevs1) {
+ abbrevs = abbrevs1
+
+ val entries: List[(String, List[String])] =
+ Multi_Map(
+ (for {
+ (abbr, txt0) <- abbrevs
+ val txt = Symbol.encode(txt0)
+ if !Symbol.iterator(txt).
+ forall(s => s.length == 1 && s(0) != Completion.caret_indicator)
+ } yield (txt, abbr)): _*).iterator_list.toList
+
+ contents.clear
+ for ((txt, abbrs) <- entries.sortBy(_._1))
+ contents += new Abbrev_Component(txt, abbrs.filterNot(_ == "").sorted)
+
+ revalidate
+ repaint
+ }
+ }
+
+ refresh
+ }
+
+
+ /* symbols */
+
private class Symbol_Component(val symbol: String, is_control: Boolean) extends Button
{
- private val font_size = Font_Info.main_size(PIDE.options.real("jedit_font_scale")).round
+ def update_font
+ {
+ font =
+ Symbol.fonts.get(symbol) match {
+ case None => GUI.font(size = font_size)
+ case Some(font_family) => GUI.font(family = font_family, size = font_size)
+ }
+ }
+ update_font
- font =
- Symbol.fonts.get(symbol) match {
- case None => GUI.font(size = font_size)
- case Some(font_family) => GUI.font(family = font_family, size = font_size)
- }
action =
Action(Symbol.decode(symbol)) {
val text_area = view.getTextArea
@@ -50,7 +117,12 @@
tooltip = "Reset control symbols within text"
}
+
+ /* tabs */
+
private val group_tabs: TabbedPane = new TabbedPane {
+ pages += new TabbedPane.Page("abbrevs", abbrevs_panel)
+
pages ++=
Symbol.groups.map({ case (group, symbols) =>
new TabbedPane.Page(group,
@@ -67,7 +139,7 @@
val results_panel = new Wrap_Panel
layout(search_field) = BorderPanel.Position.North
layout(new ScrollPane(results_panel)) = BorderPanel.Position.Center
-
+
val search_space =
(for (sym <- Symbol.names.keysIterator) yield (sym, Word.lowercase(sym))).toList
val search_delay =
@@ -99,4 +171,46 @@
page.title = Word.implode(Word.explode('_', page.title).map(Word.perhaps_capitalize(_)))
}
set_content(group_tabs)
+
+
+
+ /* main */
+
+ private val edit_bus_handler: EBComponent =
+ new EBComponent { def handleMessage(msg: EBMessage) { abbrevs_refresh_delay.invoke() } }
+
+ private val main =
+ Session.Consumer[Any](getClass.getName) {
+ case _: Session.Global_Options =>
+ GUI_Thread.later {
+ val comp = group_tabs.peer
+ GUI.traverse_components(comp,
+ {
+ case c0: javax.swing.JComponent =>
+ Component.wrap(c0) match {
+ case c: Abbrev_Component => c.update_font
+ case c: Symbol_Component => c.update_font
+ case _ =>
+ }
+ case _ =>
+ })
+ comp.revalidate
+ comp.repaint()
+ }
+ case _: Session.Commands_Changed => abbrevs_refresh_delay.invoke()
+ }
+
+ override def init()
+ {
+ EditBus.addToBus(edit_bus_handler)
+ PIDE.session.global_options += main
+ PIDE.session.commands_changed += main
+ }
+
+ override def exit()
+ {
+ EditBus.removeFromBus(edit_bus_handler)
+ PIDE.session.global_options -= main
+ PIDE.session.commands_changed -= main
+ }
}