--- a/NEWS Mon Jan 01 16:36:52 2018 +0100
+++ b/NEWS Mon Jan 01 21:17:28 2018 +0100
@@ -77,6 +77,9 @@
"isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1
arguments into this format.
+* Completion provides templates for named symbols with arguments,
+e.g. "\<comment> \<open>ARGUMENT\<close>" or "\<^emph>\<open>ARGUMENT\<close>".
+
* Bibtex database files (.bib) are semantically checked.
* Action "isabelle.preview" is able to present more file formats,
--- a/etc/symbols Mon Jan 01 16:36:52 2018 +0100
+++ b/etc/symbols Mon Jan 01 21:17:28 2018 +0100
@@ -358,7 +358,7 @@
\<some> code: 0x0003f5
\<hole> code: 0x002311
\<newline> code: 0x0023ce
-\<comment> code: 0x002015 group: document font: IsabelleText
+\<comment> code: 0x002015 group: document argument: space_cartouche font: IsabelleText
\<open> code: 0x002039 group: punctuation font: IsabelleText abbrev: <<
\<close> code: 0x00203a group: punctuation font: IsabelleText abbrev: >>
\<^here> code: 0x002302 font: IsabelleText
@@ -370,19 +370,56 @@
\<^item> code: 0x0025aa group: document font: IsabelleText
\<^enum> code: 0x0025b8 group: document font: IsabelleText
\<^descr> code: 0x0027a7 group: document font: IsabelleText
-\<^footnote> code: 0x00204b group: document font: IsabelleText
-\<^verbatim> code: 0x0025a9 group: document font: IsabelleText
-\<^theory_text> code: 0x002b1a group: document font: IsabelleText
-\<^emph> code: 0x002217 group: document font: IsabelleText
-\<^bold> code: 0x002759 group: control group: document font: IsabelleText
+\<^footnote> code: 0x00204b group: document argument: cartouche font: IsabelleText
+\<^verbatim> code: 0x0025a9 group: document argument: cartouche font: IsabelleText
+\<^theory_text> code: 0x002b1a group: document argument: cartouche font: IsabelleText
+\<^emph> code: 0x002217 group: document argument: cartouche font: IsabelleText
+\<^bold> code: 0x002759 group: control argument: cartouche group: document font: IsabelleText
\<^sub> code: 0x0021e9 group: control font: IsabelleText
\<^sup> code: 0x0021e7 group: control font: IsabelleText
\<^bsub> code: 0x0021d8 group: control_block font: IsabelleText abbrev: =_(
\<^esub> code: 0x0021d9 group: control_block font: IsabelleText abbrev: =_)
\<^bsup> code: 0x0021d7 group: control_block font: IsabelleText abbrev: =^(
\<^esup> code: 0x0021d6 group: control_block font: IsabelleText abbrev: =^)
-\<^file> code: 0x01F5CF group: icon font: IsabelleText
-\<^dir> code: 0x01F5C0 group: icon font: IsabelleText
-\<^url> code: 0x01F310 group: icon font: IsabelleText
-\<^doc> code: 0x01F4D3 group: icon font: IsabelleText
-\<^action> code: 0x00261b group: icon font: IsabelleText
+\<^file> code: 0x01F5CF group: icon argument: cartouche font: IsabelleText
+\<^dir> code: 0x01F5C0 group: icon argument: cartouche font: IsabelleText
+\<^url> code: 0x01F310 group: icon argument: cartouche font: IsabelleText
+\<^doc> code: 0x01F4D3 group: icon argument: cartouche font: IsabelleText
+\<^action> code: 0x00261b group: icon argument: cartouche font: IsabelleText
+\<^assert>
+\<^binding> argument: cartouche
+\<^class> argument: cartouche
+\<^class_syntax> argument: cartouche
+\<^command_keyword> argument: cartouche
+\<^const_abbrev> argument: cartouche
+\<^const_name> argument: cartouche
+\<^const_syntax> argument: cartouche
+\<^context>
+\<^cprop> argument: cartouche
+\<^cterm> argument: cartouche
+\<^ctyp> argument: cartouche
+\<^keyword> argument: cartouche
+\<^locale> argument: cartouche
+\<^make_string>
+\<^method> argument: cartouche
+\<^named_theorems> argument: cartouche
+\<^nonterminal> argument: cartouche
+\<^path> argument: cartouche
+\<^plugin> argument: cartouche
+\<^print>
+\<^prop> argument: cartouche
+\<^simproc> argument: cartouche
+\<^sort> argument: cartouche
+\<^syntax_const> argument: cartouche
+\<^system_option> argument: cartouche
+\<^term> argument: cartouche
+\<^theory> argument: cartouche
+\<^theory_context> argument: cartouche
+\<^typ> argument: cartouche
+\<^type_abbrev> argument: cartouche
+\<^type_name> argument: cartouche
+\<^type_syntax> argument: cartouche
+\<^code> argument: cartouche
+\<^computation> argument: cartouche
+\<^computation_conv> argument: cartouche
+\<^computation_check> argument: cartouche
--- a/src/Pure/General/completion.scala Mon Jan 01 16:36:52 2018 +0100
+++ b/src/Pure/General/completion.scala Mon Jan 01 21:17:28 2018 +0100
@@ -367,8 +367,15 @@
def add_symbols: Completion =
{
val words =
- (for ((sym, _) <- Symbol.names.toList) yield (sym, sym)) :::
- (for ((sym, name) <- Symbol.names.toList) yield ("\\" + name, sym))
+ Symbol.names.toList.flatMap({ case (sym, (name, argument)) =>
+ val word = "\\" + name
+ val seps =
+ if (argument == Symbol.ARGUMENT_CARTOUCHE) List("")
+ else if (argument == Symbol.ARGUMENT_SPACE_CARTOUCHE) List(" ")
+ else Nil
+ List(sym -> sym, word -> sym) :::
+ seps.map(sep => word -> (sym + sep + "\\<open>\u0007\\<close>"))
+ })
new Completion(
keywords,
--- a/src/Pure/General/symbol.scala Mon Jan 01 16:36:52 2018 +0100
+++ b/src/Pure/General/symbol.scala Mon Jan 01 21:17:28 2018 +0100
@@ -300,6 +300,9 @@
/** symbol interpretation **/
+ val ARGUMENT_CARTOUCHE = "cartouche"
+ val ARGUMENT_SPACE_CARTOUCHE = "space_cartouche"
+
private lazy val symbols =
{
val contents =
@@ -350,10 +353,18 @@
val properties: Map[Symbol, Properties.T] = Map(symbols: _*)
- val names: Map[Symbol, String] =
+ val names: Map[Symbol, (String, String)] =
{
- val name = new Regex("""\\<\^?([A-Za-z][A-Za-z0-9_']*)>""")
- Map((for ((sym @ name(a), _) <- symbols) yield sym -> a): _*)
+ val Name = new Regex("""\\<\^?([A-Za-z][A-Za-z0-9_']*)>""")
+ val Argument = new Properties.String("argument")
+ def argument(sym: Symbol, props: Properties.T): String =
+ props match {
+ case Argument(arg) =>
+ if (arg == ARGUMENT_CARTOUCHE || arg == ARGUMENT_SPACE_CARTOUCHE) arg
+ else error("Bad argument: " + quote(arg) + " for symbol " + quote(sym))
+ case _ => ""
+ }
+ Map((for ((sym @ Name(a), props) <- symbols) yield sym -> (a, argument(sym, props))): _*)
}
val groups: List[(String, List[Symbol])] =
@@ -376,12 +387,12 @@
val Code = new Properties.String("code")
for {
(sym, props) <- symbols
- code =
+ code <-
props match {
case Code(s) =>
- try { Integer.decode(s).intValue }
+ try { Some(Integer.decode(s).intValue) }
catch { case _: NumberFormatException => error("Bad code for symbol " + sym) }
- case _ => error("Missing code for symbol " + sym)
+ case _ => None
}
} yield {
if (code < 128) error("Illegal ASCII code for symbol " + sym)
@@ -499,7 +510,7 @@
/* tables */
def properties: Map[Symbol, Properties.T] = symbols.properties
- def names: Map[Symbol, String] = symbols.names
+ def names: Map[Symbol, (String, String)] = symbols.names
def groups: List[(String, List[Symbol])] = symbols.groups
def abbrevs: Multi_Map[Symbol, String] = symbols.abbrevs
def codes: List[(Symbol, Int)] = symbols.codes