tuned;
authorwenzelm
Wed Jul 08 12:09:44 2015 +0200 (2015-07-08)
changeset 60692896704918a1f
parent 60691 0568c7a2b5db
child 60693 044f8bb3dd30
tuned;
src/Pure/Isar/keyword.scala
src/Pure/Isar/outer_syntax.scala
src/Pure/Isar/token.scala
     1.1 --- a/src/Pure/Isar/keyword.scala	Wed Jul 08 11:50:43 2015 +0200
     1.2 +++ b/src/Pure/Isar/keyword.scala	Wed Jul 08 12:09:44 2015 +0200
     1.3 @@ -77,6 +77,9 @@
     1.4    val qed = Set(QED, QED_SCRIPT, QED_BLOCK)
     1.5    val qed_global = Set(QED_GLOBAL)
     1.6  
     1.7 +  val proof_open = proof_goal + PRF_OPEN
     1.8 +  val proof_close = qed + PRF_CLOSE
     1.9 +
    1.10  
    1.11  
    1.12    /** keyword tables **/
     2.1 --- a/src/Pure/Isar/outer_syntax.scala	Wed Jul 08 11:50:43 2015 +0200
     2.2 +++ b/src/Pure/Isar/outer_syntax.scala	Wed Jul 08 12:09:44 2015 +0200
     2.3 @@ -164,16 +164,11 @@
     2.4        ((structure.span_depth, structure.after_span_depth) /: tokens) {
     2.5          case ((x, y), tok) =>
     2.6            if (tok.is_command) {
     2.7 -            if (tok.is_command_kind(keywords, Keyword.theory_goal))
     2.8 -              (2, 1)
     2.9 -            else if (tok.is_command_kind(keywords, Keyword.theory))
    2.10 -              (1, 0)
    2.11 -            else if (tok.is_command_kind(keywords, Keyword.proof_goal) || tok.is_begin_block)
    2.12 -              (y + 2, y + 1)
    2.13 -            else if (tok.is_command_kind(keywords, Keyword.qed) || tok.is_end_block)
    2.14 -              (y + 1, y - 1)
    2.15 -            else if (tok.is_command_kind(keywords, Keyword.qed_global))
    2.16 -              (1, 0)
    2.17 +            if (tok.is_command_kind(keywords, Keyword.theory_goal)) (2, 1)
    2.18 +            else if (tok.is_command_kind(keywords, Keyword.theory)) (1, 0)
    2.19 +            else if (tok.is_command_kind(keywords, Keyword.proof_open)) (y + 2, y + 1)
    2.20 +            else if (tok.is_command_kind(keywords, Keyword.proof_close)) (y + 1, y - 1)
    2.21 +            else if (tok.is_command_kind(keywords, Keyword.qed_global)) (1, 0)
    2.22              else (x, y)
    2.23            }
    2.24            else (x, y)
     3.1 --- a/src/Pure/Isar/token.scala	Wed Jul 08 11:50:43 2015 +0200
     3.2 +++ b/src/Pure/Isar/token.scala	Wed Jul 08 12:09:44 2015 +0200
     3.3 @@ -263,9 +263,6 @@
     3.4    def is_command_modifier: Boolean =
     3.5      is_keyword && (source == "public" || source == "private" || source == "qualified")
     3.6  
     3.7 -  def is_begin_block: Boolean = is_command && source == "{"
     3.8 -  def is_end_block: Boolean = is_command && source == "}"
     3.9 -
    3.10    def content: String =
    3.11      if (kind == Token.Kind.STRING) Scan.Parsers.quoted_content("\"", source)
    3.12      else if (kind == Token.Kind.ALT_STRING) Scan.Parsers.quoted_content("`", source)