completion templates for commands involving "begin ... end" blocks;
authorwenzelm
Wed Jul 20 16:02:00 2016 +0200 (2016-07-20)
changeset 635280f39f59317c1
parent 63527 59eff6e56d81
child 63529 58980a8b2faf
completion templates for commands involving "begin ... end" blocks;
NEWS
src/Pure/General/symbol.scala
src/Pure/Isar/outer_syntax.scala
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/NEWS	Wed Jul 20 11:44:11 2016 +0200
     1.2 +++ b/NEWS	Wed Jul 20 16:02:00 2016 +0200
     1.3 @@ -103,6 +103,9 @@
     1.4  * Command 'proof' provides information about proof outline with cases,
     1.5  e.g. for proof methods "cases", "induct", "goal_cases".
     1.6  
     1.7 +* Completion templates for commands involving "begin ... end" blocks,
     1.8 +e.g. 'context', 'notepad'.
     1.9 +
    1.10  
    1.11  *** Isar ***
    1.12  
     2.1 --- a/src/Pure/General/symbol.scala	Wed Jul 20 11:44:11 2016 +0200
     2.2 +++ b/src/Pure/General/symbol.scala	Wed Jul 20 16:02:00 2016 +0200
     2.3 @@ -458,8 +458,9 @@
     2.4      val symbolic = recode_set((for { (sym, _) <- symbols; if raw_symbolic(sym) } yield sym): _*)
     2.5  
     2.6  
     2.7 -    /* comment */
     2.8 +    /* misc symbols */
     2.9  
    2.10 +    val newline_decoded = decode(newline)
    2.11      val comment_decoded = decode(comment)
    2.12  
    2.13  
    2.14 @@ -526,7 +527,15 @@
    2.15    def is_blank(sym: Symbol): Boolean = symbols.blanks.contains(sym)
    2.16  
    2.17  
    2.18 -  /* comment */
    2.19 +  /* misc symbols */
    2.20 +
    2.21 +  val newline: Symbol = "\\<newline>"
    2.22 +  def newline_decoded: Symbol = symbols.newline_decoded
    2.23 +
    2.24 +  def print_newlines(str: String): String =
    2.25 +    if (str.contains('\n'))
    2.26 +      (for (s <- iterator(str)) yield { if (s == "\n") newline_decoded else s }).mkString
    2.27 +    else str
    2.28  
    2.29    val comment: Symbol = "\\<comment>"
    2.30    def comment_decoded: Symbol = symbols.comment_decoded
     3.1 --- a/src/Pure/Isar/outer_syntax.scala	Wed Jul 20 11:44:11 2016 +0200
     3.2 +++ b/src/Pure/Isar/outer_syntax.scala	Wed Jul 20 16:02:00 2016 +0200
     3.3 @@ -91,6 +91,8 @@
     3.4      val keywords1 = keywords + (name, kind, tags)
     3.5      val completion1 =
     3.6        if (replace == Some("")) completion
     3.7 +      else if (replace.isEmpty && Keyword.theory_block.contains(kind))
     3.8 +        completion + (name, name + "\nbegin\n\u0007\nend") + (name, name)
     3.9        else completion + (name, replace getOrElse name)
    3.10      new Outer_Syntax(keywords1, completion1, language_context, true)
    3.11    }
     4.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Wed Jul 20 11:44:11 2016 +0200
     4.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Jul 20 16:02:00 2016 +0200
     4.3 @@ -35,8 +35,8 @@
     4.4      private val html =
     4.5        item.description match {
     4.6          case a :: bs =>
     4.7 -          "<html><b>" + HTML.output(a) + "</b>" +
     4.8 -            HTML.output(bs.map(" " + _).mkString) + "</html>"
     4.9 +          "<html><b>" + HTML.output(Symbol.print_newlines(a)) + "</b>" +
    4.10 +            HTML.output(bs.map(b => " " + Symbol.print_newlines(b)).mkString) + "</html>"
    4.11          case Nil => ""
    4.12        }
    4.13      override def toString: String = html