more completion templates;
authorwenzelm
Mon Jan 01 21:17:28 2018 +0100 (18 months ago)
changeset 673113869b2400e22
parent 67310 506acf60d6b1
child 67312 0d25e02759b7
more completion templates;
NEWS
etc/symbols
src/Pure/General/completion.scala
src/Pure/General/symbol.scala
     1.1 --- a/NEWS	Mon Jan 01 16:36:52 2018 +0100
     1.2 +++ b/NEWS	Mon Jan 01 21:17:28 2018 +0100
     1.3 @@ -77,6 +77,9 @@
     1.4  "isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1
     1.5  arguments into this format.
     1.6  
     1.7 +* Completion provides templates for named symbols with arguments,
     1.8 +e.g. "\<comment> \<open>ARGUMENT\<close>" or "\<^emph>\<open>ARGUMENT\<close>".
     1.9 +
    1.10  * Bibtex database files (.bib) are semantically checked.
    1.11  
    1.12  * Action "isabelle.preview" is able to present more file formats,
     2.1 --- a/etc/symbols	Mon Jan 01 16:36:52 2018 +0100
     2.2 +++ b/etc/symbols	Mon Jan 01 21:17:28 2018 +0100
     2.3 @@ -358,7 +358,7 @@
     2.4  \<some>                 code: 0x0003f5
     2.5  \<hole>                 code: 0x002311
     2.6  \<newline>              code: 0x0023ce
     2.7 -\<comment>              code: 0x002015  group: document  font: IsabelleText
     2.8 +\<comment>              code: 0x002015  group: document  argument: space_cartouche  font: IsabelleText
     2.9  \<open>                 code: 0x002039  group: punctuation  font: IsabelleText  abbrev: <<
    2.10  \<close>                code: 0x00203a  group: punctuation  font: IsabelleText  abbrev: >>
    2.11  \<^here>                code: 0x002302  font: IsabelleText
    2.12 @@ -370,19 +370,56 @@
    2.13  \<^item>                code: 0x0025aa  group: document  font: IsabelleText
    2.14  \<^enum>                code: 0x0025b8  group: document  font: IsabelleText
    2.15  \<^descr>               code: 0x0027a7  group: document  font: IsabelleText
    2.16 -\<^footnote>            code: 0x00204b  group: document  font: IsabelleText
    2.17 -\<^verbatim>            code: 0x0025a9  group: document  font: IsabelleText
    2.18 -\<^theory_text>         code: 0x002b1a  group: document  font: IsabelleText
    2.19 -\<^emph>                code: 0x002217  group: document  font: IsabelleText
    2.20 -\<^bold>                code: 0x002759  group: control  group: document  font: IsabelleText
    2.21 +\<^footnote>            code: 0x00204b  group: document  argument: cartouche  font: IsabelleText
    2.22 +\<^verbatim>            code: 0x0025a9  group: document  argument: cartouche  font: IsabelleText
    2.23 +\<^theory_text>         code: 0x002b1a  group: document  argument: cartouche  font: IsabelleText
    2.24 +\<^emph>                code: 0x002217  group: document  argument: cartouche  font: IsabelleText
    2.25 +\<^bold>                code: 0x002759  group: control  argument: cartouche  group: document  font: IsabelleText
    2.26  \<^sub>                 code: 0x0021e9  group: control  font: IsabelleText
    2.27  \<^sup>                 code: 0x0021e7  group: control  font: IsabelleText
    2.28  \<^bsub>                code: 0x0021d8  group: control_block  font: IsabelleText  abbrev: =_(
    2.29  \<^esub>                code: 0x0021d9  group: control_block  font: IsabelleText  abbrev: =_)
    2.30  \<^bsup>                code: 0x0021d7  group: control_block  font: IsabelleText  abbrev: =^(
    2.31  \<^esup>                code: 0x0021d6  group: control_block  font: IsabelleText  abbrev: =^)
    2.32 -\<^file>                code: 0x01F5CF  group: icon  font: IsabelleText
    2.33 -\<^dir>                 code: 0x01F5C0  group: icon  font: IsabelleText
    2.34 -\<^url>                 code: 0x01F310  group: icon  font: IsabelleText
    2.35 -\<^doc>                 code: 0x01F4D3  group: icon  font: IsabelleText
    2.36 -\<^action>              code: 0x00261b  group: icon  font: IsabelleText
    2.37 +\<^file>                code: 0x01F5CF  group: icon  argument: cartouche  font: IsabelleText
    2.38 +\<^dir>                 code: 0x01F5C0  group: icon  argument: cartouche  font: IsabelleText
    2.39 +\<^url>                 code: 0x01F310  group: icon  argument: cartouche  font: IsabelleText
    2.40 +\<^doc>                 code: 0x01F4D3  group: icon  argument: cartouche  font: IsabelleText
    2.41 +\<^action>              code: 0x00261b  group: icon  argument: cartouche  font: IsabelleText
    2.42 +\<^assert>
    2.43 +\<^binding>             argument: cartouche
    2.44 +\<^class>               argument: cartouche
    2.45 +\<^class_syntax>        argument: cartouche
    2.46 +\<^command_keyword>     argument: cartouche
    2.47 +\<^const_abbrev>        argument: cartouche
    2.48 +\<^const_name>          argument: cartouche
    2.49 +\<^const_syntax>        argument: cartouche
    2.50 +\<^context>
    2.51 +\<^cprop>               argument: cartouche
    2.52 +\<^cterm>               argument: cartouche
    2.53 +\<^ctyp>                argument: cartouche
    2.54 +\<^keyword>             argument: cartouche
    2.55 +\<^locale>              argument: cartouche
    2.56 +\<^make_string>
    2.57 +\<^method>              argument: cartouche
    2.58 +\<^named_theorems>      argument: cartouche
    2.59 +\<^nonterminal>         argument: cartouche
    2.60 +\<^path>                argument: cartouche
    2.61 +\<^plugin>              argument: cartouche
    2.62 +\<^print>
    2.63 +\<^prop>                argument: cartouche
    2.64 +\<^simproc>             argument: cartouche
    2.65 +\<^sort>                argument: cartouche
    2.66 +\<^syntax_const>        argument: cartouche
    2.67 +\<^system_option>       argument: cartouche
    2.68 +\<^term>                argument: cartouche
    2.69 +\<^theory>              argument: cartouche
    2.70 +\<^theory_context>      argument: cartouche
    2.71 +\<^typ>                 argument: cartouche
    2.72 +\<^type_abbrev>         argument: cartouche
    2.73 +\<^type_name>           argument: cartouche
    2.74 +\<^type_syntax>         argument: cartouche
    2.75 +\<^code>                argument: cartouche
    2.76 +\<^computation>         argument: cartouche
    2.77 +\<^computation_conv>    argument: cartouche
    2.78 +\<^computation_check>   argument: cartouche
     3.1 --- a/src/Pure/General/completion.scala	Mon Jan 01 16:36:52 2018 +0100
     3.2 +++ b/src/Pure/General/completion.scala	Mon Jan 01 21:17:28 2018 +0100
     3.3 @@ -367,8 +367,15 @@
     3.4    def add_symbols: Completion =
     3.5    {
     3.6      val words =
     3.7 -      (for ((sym, _) <- Symbol.names.toList) yield (sym, sym)) :::
     3.8 -      (for ((sym, name) <- Symbol.names.toList) yield ("\\" + name, sym))
     3.9 +      Symbol.names.toList.flatMap({ case (sym, (name, argument)) =>
    3.10 +        val word = "\\" + name
    3.11 +        val seps =
    3.12 +          if (argument == Symbol.ARGUMENT_CARTOUCHE) List("")
    3.13 +          else if (argument == Symbol.ARGUMENT_SPACE_CARTOUCHE) List(" ")
    3.14 +          else Nil
    3.15 +        List(sym -> sym, word -> sym) :::
    3.16 +          seps.map(sep => word -> (sym + sep + "\\<open>\u0007\\<close>"))
    3.17 +      })
    3.18  
    3.19      new Completion(
    3.20        keywords,
     4.1 --- a/src/Pure/General/symbol.scala	Mon Jan 01 16:36:52 2018 +0100
     4.2 +++ b/src/Pure/General/symbol.scala	Mon Jan 01 21:17:28 2018 +0100
     4.3 @@ -300,6 +300,9 @@
     4.4  
     4.5    /** symbol interpretation **/
     4.6  
     4.7 +  val ARGUMENT_CARTOUCHE = "cartouche"
     4.8 +  val ARGUMENT_SPACE_CARTOUCHE = "space_cartouche"
     4.9 +
    4.10    private lazy val symbols =
    4.11    {
    4.12      val contents =
    4.13 @@ -350,10 +353,18 @@
    4.14  
    4.15      val properties: Map[Symbol, Properties.T] = Map(symbols: _*)
    4.16  
    4.17 -    val names: Map[Symbol, String] =
    4.18 +    val names: Map[Symbol, (String, String)] =
    4.19      {
    4.20 -      val name = new Regex("""\\<\^?([A-Za-z][A-Za-z0-9_']*)>""")
    4.21 -      Map((for ((sym @ name(a), _) <- symbols) yield sym -> a): _*)
    4.22 +      val Name = new Regex("""\\<\^?([A-Za-z][A-Za-z0-9_']*)>""")
    4.23 +      val Argument = new Properties.String("argument")
    4.24 +      def argument(sym: Symbol, props: Properties.T): String =
    4.25 +        props match {
    4.26 +          case Argument(arg) =>
    4.27 +            if (arg == ARGUMENT_CARTOUCHE || arg == ARGUMENT_SPACE_CARTOUCHE) arg
    4.28 +            else error("Bad argument: " + quote(arg) + " for symbol " + quote(sym))
    4.29 +          case _ => ""
    4.30 +        }
    4.31 +      Map((for ((sym @ Name(a), props) <- symbols) yield sym -> (a, argument(sym, props))): _*)
    4.32      }
    4.33  
    4.34      val groups: List[(String, List[Symbol])] =
    4.35 @@ -376,12 +387,12 @@
    4.36        val Code = new Properties.String("code")
    4.37        for {
    4.38          (sym, props) <- symbols
    4.39 -        code =
    4.40 +        code <-
    4.41            props match {
    4.42              case Code(s) =>
    4.43 -              try { Integer.decode(s).intValue }
    4.44 +              try { Some(Integer.decode(s).intValue) }
    4.45                catch { case _: NumberFormatException => error("Bad code for symbol " + sym) }
    4.46 -            case _ => error("Missing code for symbol " + sym)
    4.47 +            case _ => None
    4.48            }
    4.49        } yield {
    4.50          if (code < 128) error("Illegal ASCII code for symbol " + sym)
    4.51 @@ -499,7 +510,7 @@
    4.52    /* tables */
    4.53  
    4.54    def properties: Map[Symbol, Properties.T] = symbols.properties
    4.55 -  def names: Map[Symbol, String] = symbols.names
    4.56 +  def names: Map[Symbol, (String, String)] = symbols.names
    4.57    def groups: List[(String, List[Symbol])] = symbols.groups
    4.58    def abbrevs: Multi_Map[Symbol, String] = symbols.abbrevs
    4.59    def codes: List[(Symbol, Int)] = symbols.codes