completion templates for commands involving "begin ... end" blocks;
--- a/NEWS Wed Jul 20 11:44:11 2016 +0200
+++ b/NEWS Wed Jul 20 16:02:00 2016 +0200
@@ -103,6 +103,9 @@
* Command 'proof' provides information about proof outline with cases,
e.g. for proof methods "cases", "induct", "goal_cases".
+* Completion templates for commands involving "begin ... end" blocks,
+e.g. 'context', 'notepad'.
+
*** Isar ***
--- a/src/Pure/General/symbol.scala Wed Jul 20 11:44:11 2016 +0200
+++ b/src/Pure/General/symbol.scala Wed Jul 20 16:02:00 2016 +0200
@@ -458,8 +458,9 @@
val symbolic = recode_set((for { (sym, _) <- symbols; if raw_symbolic(sym) } yield sym): _*)
- /* comment */
+ /* misc symbols */
+ val newline_decoded = decode(newline)
val comment_decoded = decode(comment)
@@ -526,7 +527,15 @@
def is_blank(sym: Symbol): Boolean = symbols.blanks.contains(sym)
- /* comment */
+ /* misc symbols */
+
+ val newline: Symbol = "\\<newline>"
+ def newline_decoded: Symbol = symbols.newline_decoded
+
+ def print_newlines(str: String): String =
+ if (str.contains('\n'))
+ (for (s <- iterator(str)) yield { if (s == "\n") newline_decoded else s }).mkString
+ else str
val comment: Symbol = "\\<comment>"
def comment_decoded: Symbol = symbols.comment_decoded
--- a/src/Pure/Isar/outer_syntax.scala Wed Jul 20 11:44:11 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Wed Jul 20 16:02:00 2016 +0200
@@ -91,6 +91,8 @@
val keywords1 = keywords + (name, kind, tags)
val completion1 =
if (replace == Some("")) completion
+ else if (replace.isEmpty && Keyword.theory_block.contains(kind))
+ completion + (name, name + "\nbegin\n\u0007\nend") + (name, name)
else completion + (name, replace getOrElse name)
new Outer_Syntax(keywords1, completion1, language_context, true)
}
--- a/src/Tools/jEdit/src/completion_popup.scala Wed Jul 20 11:44:11 2016 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Wed Jul 20 16:02:00 2016 +0200
@@ -35,8 +35,8 @@
private val html =
item.description match {
case a :: bs =>
- "<html><b>" + HTML.output(a) + "</b>" +
- HTML.output(bs.map(" " + _).mkString) + "</html>"
+ "<html><b>" + HTML.output(Symbol.print_newlines(a)) + "</b>" +
+ HTML.output(bs.map(b => " " + Symbol.print_newlines(b)).mkString) + "</html>"
case Nil => ""
}
override def toString: String = html