# HG changeset patch # User wenzelm # Date 1469023320 -7200 # Node ID 0f39f59317c15f198fb8dc767cf87de9de65fc9e # Parent 59eff6e56d816e98db711c21be16fc597236a5f7 completion templates for commands involving "begin ... end" blocks; diff -r 59eff6e56d81 -r 0f39f59317c1 NEWS --- 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 *** diff -r 59eff6e56d81 -r 0f39f59317c1 src/Pure/General/symbol.scala --- 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 = "\\" + 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 = "\\" def comment_decoded: Symbol = symbols.comment_decoded diff -r 59eff6e56d81 -r 0f39f59317c1 src/Pure/Isar/outer_syntax.scala --- 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) } diff -r 59eff6e56d81 -r 0f39f59317c1 src/Tools/jEdit/src/completion_popup.scala --- 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.output(a) + "" + - HTML.output(bs.map(" " + _).mkString) + "" + "" + HTML.output(Symbol.print_newlines(a)) + "" + + HTML.output(bs.map(b => " " + Symbol.print_newlines(b)).mkString) + "" case Nil => "" } override def toString: String = html