# HG changeset patch
# User wenzelm
# Date 1514837848 -3600
# Node ID 3869b2400e221def1f553f367b7d894294126369
# Parent  506acf60d6b1fcbabebf425329d06b9e2fcd78c7
more completion templates;

diff -r 506acf60d6b1 -r 3869b2400e22 NEWS
--- 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,
diff -r 506acf60d6b1 -r 3869b2400e22 etc/symbols
--- 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
diff -r 506acf60d6b1 -r 3869b2400e22 src/Pure/General/completion.scala
--- 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,
diff -r 506acf60d6b1 -r 3869b2400e22 src/Pure/General/symbol.scala
--- 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