tuned;
authorwenzelm
Wed Jul 13 19:36:47 2016 +0200 (2016-07-13)
changeset 63479464ef556bd21
parent 63478 37a3fc20154d
child 63480 05908c773ca7
tuned;
src/Pure/Isar/keyword.scala
src/Pure/Isar/outer_syntax.scala
src/Tools/jEdit/src/text_structure.scala
     1.1 --- a/src/Pure/Isar/keyword.scala	Wed Jul 13 19:10:35 2016 +0200
     1.2 +++ b/src/Pure/Isar/keyword.scala	Wed Jul 13 19:36:47 2016 +0200
     1.3 @@ -66,6 +66,8 @@
     1.4  
     1.5    val theory_body = Set(THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
     1.6  
     1.7 +  val prf_script = Set(PRF_SCRIPT)
     1.8 +
     1.9    val proof =
    1.10      Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, NEXT_BLOCK, PRF_OPEN,
    1.11        PRF_CLOSE, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL,
     2.1 --- a/src/Pure/Isar/outer_syntax.scala	Wed Jul 13 19:10:35 2016 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.scala	Wed Jul 13 19:36:47 2016 +0200
     2.3 @@ -174,9 +174,9 @@
     2.4              if (keywords.is_command(tok, Keyword.theory_goal)) (2, 1)
     2.5              else if (keywords.is_command(tok, Keyword.theory)) (1, 0)
     2.6              else if (keywords.is_command(tok, Keyword.proof_open)) (y + 2, y + 1)
     2.7 -            else if (keywords.is_command(tok, Keyword.PRF_BLOCK == _)) (y + 2, y + 1)
     2.8 -            else if (keywords.is_command(tok, Keyword.QED_BLOCK == _)) (y - 1, y - 2)
     2.9 -            else if (keywords.is_command(tok, Keyword.PRF_CLOSE == _)) (y, y - 1)
    2.10 +            else if (keywords.is_command(tok, Set(Keyword.PRF_BLOCK))) (y + 2, y + 1)
    2.11 +            else if (keywords.is_command(tok, Set(Keyword.QED_BLOCK))) (y - 1, y - 2)
    2.12 +            else if (keywords.is_command(tok, Set(Keyword.PRF_CLOSE))) (y, y - 1)
    2.13              else if (keywords.is_command(tok, Keyword.proof_close)) (y + 1, y - 1)
    2.14              else if (keywords.is_command(tok, Keyword.qed_global)) (1, 0)
    2.15              else (x, y)
     3.1 --- a/src/Tools/jEdit/src/text_structure.scala	Wed Jul 13 19:10:35 2016 +0200
     3.2 +++ b/src/Tools/jEdit/src/text_structure.scala	Wed Jul 13 19:36:47 2016 +0200
     3.3 @@ -122,7 +122,7 @@
     3.4              nav.reverse_iterator(current_line - 1).scanLeft((0, false))(
     3.5                { case ((ind, _), Text.Info(range, tok)) =>
     3.6                    val ind1 = ind + indent_indent(tok)
     3.7 -                  if (tok.is_begin_or_command && !keywords.is_command(tok, Keyword.PRF_SCRIPT == _)) {
     3.8 +                  if (tok.is_begin_or_command && !keywords.is_command(tok, Keyword.prf_script)) {
     3.9                      val line = buffer.getLineOfOffset(range.start)
    3.10                      line_head(line) match {
    3.11                        case Some(info) if info.info == tok =>
    3.12 @@ -140,7 +140,7 @@
    3.13                  if (tok.is_begin ||
    3.14                      keywords.is_before_command(tok) ||
    3.15                      keywords.is_command(tok, Keyword.theory)) 0
    3.16 -                else if (keywords.is_command(tok, Keyword.PRF_SCRIPT == _))
    3.17 +                else if (keywords.is_command(tok, Keyword.prf_script))
    3.18                    (indent_structure + script_indent(range)) max indent_size
    3.19                  else if (keywords.is_command(tok, Keyword.proof))
    3.20                    (indent_structure - indent_offset(tok)) max indent_size