# HG changeset patch
# User wenzelm
# Date 1468253904 -7200
# Node ID 19162a9ef7e361d83cf12c5101d1cabd9ba0f775
# Parent  5761bb8592dcc64ac1cf43035ed8ded3eae2fde1
tunes signature;

diff -r 5761bb8592dc -r 19162a9ef7e3 src/Pure/Isar/parse.scala
--- a/src/Pure/Isar/parse.scala	Mon Jul 11 17:53:02 2016 +0200
+++ b/src/Pure/Isar/parse.scala	Mon Jul 11 18:18:24 2016 +0200
@@ -59,12 +59,8 @@
     def atom(s: String, pred: Elem => Boolean): Parser[String] =
       token(s, pred) ^^ (_.content)
 
-    def command(name: String): Parser[String] =
-      atom("command " + quote(name), tok => tok.is_command && tok.source == name)
-
-    def $$$(name: String): Parser[String] =
-      atom("keyword " + quote(name), tok => tok.is_keyword && tok.source == name)
-
+    def command(name: String): Parser[String] = atom("command " + quote(name), _.is_command(name))
+    def $$$(name: String): Parser[String] = atom("keyword " + quote(name), _.is_keyword(name))
     def string: Parser[String] = atom("string", _.is_string)
     def nat: Parser[Int] = atom("natural number", _.is_nat) ^^ (s => Integer.parseInt(s))
     def name: Parser[String] = atom("name", _.is_name)
diff -r 5761bb8592dc -r 19162a9ef7e3 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Mon Jul 11 17:53:02 2016 +0200
+++ b/src/Pure/Isar/token.scala	Mon Jul 11 18:18:24 2016 +0200
@@ -225,7 +225,9 @@
 sealed case class Token(kind: Token.Kind.Value, source: String)
 {
   def is_command: Boolean = kind == Token.Kind.COMMAND
+  def is_command(name: String): Boolean = kind == Token.Kind.COMMAND && source == name
   def is_keyword: Boolean = kind == Token.Kind.KEYWORD
+  def is_keyword(name: String): Boolean = kind == Token.Kind.KEYWORD && source == name
   def is_delimiter: Boolean = is_keyword && !Symbol.is_ascii_identifier(source)
   def is_ident: Boolean = kind == Token.Kind.IDENT
   def is_sym_ident: Boolean = kind == Token.Kind.SYM_IDENT
@@ -254,8 +256,8 @@
     source.startsWith(Symbol.open) ||
     source.startsWith(Symbol.open_decoded))
 
-  def is_begin: Boolean = is_keyword && source == "begin"
-  def is_end: Boolean = is_command && source == "end"
+  def is_begin: Boolean = is_keyword("begin")
+  def is_end: Boolean = is_command("end")
 
   def content: String =
     if (kind == Token.Kind.STRING) Scan.Parsers.quoted_content("\"", source)
diff -r 5761bb8592dc -r 19162a9ef7e3 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Jul 11 17:53:02 2016 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Jul 11 18:18:24 2016 +0200
@@ -96,8 +96,7 @@
           Token_Markup.line_token_iterator(
             Thy_Header.bootstrap_syntax, buffer, 0, buffer.getLineCount).collectFirst(
               {
-                case Text.Info(range, tok)
-                if tok.is_command && tok.source == Thy_Header.THEORY => range.start
+                case Text.Info(range, tok) if tok.is_command(Thy_Header.THEORY) => range.start
               })
             match {
               case Some(offset) =>
diff -r 5761bb8592dc -r 19162a9ef7e3 src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Mon Jul 11 17:53:02 2016 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala	Mon Jul 11 18:18:24 2016 +0200
@@ -81,8 +81,7 @@
             else 0
 
           def indent_offset(tok: Token): Int =
-            if (keywords.is_command(tok, Keyword.proof_enclose)) indent_size
-            else if (tok.is_begin) indent_size
+            if (keywords.is_command(tok, Keyword.proof_enclose) || tok.is_begin) indent_size
             else 0
 
           def indent_extra: Int =