# HG changeset patch
# User wenzelm
# Date 1468431407 -7200
# Node ID 464ef556bd218d69819c7f210226e31b077ffcdc
# Parent  37a3fc20154d5ae17664241c2be41e8668298167
tuned;

diff -r 37a3fc20154d -r 464ef556bd21 src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Wed Jul 13 19:10:35 2016 +0200
+++ b/src/Pure/Isar/keyword.scala	Wed Jul 13 19:36:47 2016 +0200
@@ -66,6 +66,8 @@
 
   val theory_body = Set(THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
 
+  val prf_script = Set(PRF_SCRIPT)
+
   val proof =
     Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, NEXT_BLOCK, PRF_OPEN,
       PRF_CLOSE, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL,
diff -r 37a3fc20154d -r 464ef556bd21 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Wed Jul 13 19:10:35 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Wed Jul 13 19:36:47 2016 +0200
@@ -174,9 +174,9 @@
             if (keywords.is_command(tok, Keyword.theory_goal)) (2, 1)
             else if (keywords.is_command(tok, Keyword.theory)) (1, 0)
             else if (keywords.is_command(tok, Keyword.proof_open)) (y + 2, y + 1)
-            else if (keywords.is_command(tok, Keyword.PRF_BLOCK == _)) (y + 2, y + 1)
-            else if (keywords.is_command(tok, Keyword.QED_BLOCK == _)) (y - 1, y - 2)
-            else if (keywords.is_command(tok, Keyword.PRF_CLOSE == _)) (y, y - 1)
+            else if (keywords.is_command(tok, Set(Keyword.PRF_BLOCK))) (y + 2, y + 1)
+            else if (keywords.is_command(tok, Set(Keyword.QED_BLOCK))) (y - 1, y - 2)
+            else if (keywords.is_command(tok, Set(Keyword.PRF_CLOSE))) (y, y - 1)
             else if (keywords.is_command(tok, Keyword.proof_close)) (y + 1, y - 1)
             else if (keywords.is_command(tok, Keyword.qed_global)) (1, 0)
             else (x, y)
diff -r 37a3fc20154d -r 464ef556bd21 src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Wed Jul 13 19:10:35 2016 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala	Wed Jul 13 19:36:47 2016 +0200
@@ -122,7 +122,7 @@
             nav.reverse_iterator(current_line - 1).scanLeft((0, false))(
               { case ((ind, _), Text.Info(range, tok)) =>
                   val ind1 = ind + indent_indent(tok)
-                  if (tok.is_begin_or_command && !keywords.is_command(tok, Keyword.PRF_SCRIPT == _)) {
+                  if (tok.is_begin_or_command && !keywords.is_command(tok, Keyword.prf_script)) {
                     val line = buffer.getLineOfOffset(range.start)
                     line_head(line) match {
                       case Some(info) if info.info == tok =>
@@ -140,7 +140,7 @@
                 if (tok.is_begin ||
                     keywords.is_before_command(tok) ||
                     keywords.is_command(tok, Keyword.theory)) 0
-                else if (keywords.is_command(tok, Keyword.PRF_SCRIPT == _))
+                else if (keywords.is_command(tok, Keyword.prf_script))
                   (indent_structure + script_indent(range)) max indent_size
                 else if (keywords.is_command(tok, Keyword.proof))
                   (indent_structure - indent_offset(tok)) max indent_size