tuned signature;
authorwenzelm
Tue Dec 09 21:14:11 2014 +0100 (2014-12-09)
changeset 59122c1dbcde94cd2
parent 59121 8ea2748241da
child 59123 e68e44836d04
tuned signature;
src/Pure/Isar/keyword.scala
src/Pure/Isar/outer_syntax.scala
src/Pure/Isar/token.scala
src/Tools/jEdit/src/structure_matching.scala
     1.1 --- a/src/Pure/Isar/keyword.scala	Tue Dec 09 20:00:45 2014 +0100
     1.2 +++ b/src/Pure/Isar/keyword.scala	Tue Dec 09 21:14:11 2014 +0100
     1.3 @@ -139,10 +139,6 @@
     1.4  
     1.5      def command_kind(name: String): Option[String] = commands.get(name).map(_._1)
     1.6  
     1.7 -    def is_command_kind(token: Token, pred: String => Boolean): Boolean =
     1.8 -      token.is_command &&
     1.9 -        (command_kind(token.source) match { case Some(k) => pred(k) case None => false })
    1.10 -
    1.11  
    1.12      /* load commands */
    1.13  
     2.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Dec 09 20:00:45 2014 +0100
     2.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Dec 09 21:14:11 2014 +0100
     2.3 @@ -156,7 +156,7 @@
     2.4      val command1 = tokens.exists(_.is_command)
     2.5  
     2.6      val depth1 =
     2.7 -      if (tokens.exists(tok => keywords.is_command_kind(tok, Keyword.theory))) 0
     2.8 +      if (tokens.exists(tok => tok.is_command_kind(keywords, Keyword.theory))) 0
     2.9        else if (command1) struct.after_span_depth
    2.10        else struct.span_depth
    2.11  
    2.12 @@ -164,15 +164,15 @@
    2.13        ((struct.span_depth, struct.after_span_depth) /: tokens) {
    2.14          case ((x, y), tok) =>
    2.15            if (tok.is_command) {
    2.16 -            if (keywords.is_command_kind(tok, Keyword.theory_goal))
    2.17 +            if (tok.is_command_kind(keywords, Keyword.theory_goal))
    2.18                (2, 1)
    2.19 -            else if (keywords.is_command_kind(tok, Keyword.theory))
    2.20 +            else if (tok.is_command_kind(keywords, Keyword.theory))
    2.21                (1, 0)
    2.22 -            else if (keywords.is_command_kind(tok, Keyword.proof_goal) || tok.is_begin_block)
    2.23 +            else if (tok.is_command_kind(keywords, Keyword.proof_goal) || tok.is_begin_block)
    2.24                (y + 2, y + 1)
    2.25 -            else if (keywords.is_command_kind(tok, Keyword.qed) || tok.is_end_block)
    2.26 +            else if (tok.is_command_kind(keywords, Keyword.qed) || tok.is_end_block)
    2.27                (y + 1, y - 1)
    2.28 -            else if (keywords.is_command_kind(tok, Keyword.qed_global))
    2.29 +            else if (tok.is_command_kind(keywords, Keyword.qed_global))
    2.30                (1, 0)
    2.31              else (x, y)
    2.32            }
     3.1 --- a/src/Pure/Isar/token.scala	Tue Dec 09 20:00:45 2014 +0100
     3.2 +++ b/src/Pure/Isar/token.scala	Tue Dec 09 21:14:11 2014 +0100
     3.3 @@ -194,6 +194,9 @@
     3.4  sealed case class Token(val kind: Token.Kind.Value, val source: String)
     3.5  {
     3.6    def is_command: Boolean = kind == Token.Kind.COMMAND
     3.7 +  def is_command_kind(keywords: Keyword.Keywords, pred: String => Boolean): Boolean =
     3.8 +    is_command &&
     3.9 +      (keywords.command_kind(source) match { case Some(k) => pred(k) case None => false })
    3.10    def is_keyword: Boolean = kind == Token.Kind.KEYWORD
    3.11    def is_delimiter: Boolean = is_keyword && !Symbol.is_ascii_identifier(source)
    3.12    def is_ident: Boolean = kind == Token.Kind.IDENT
     4.1 --- a/src/Tools/jEdit/src/structure_matching.scala	Tue Dec 09 20:00:45 2014 +0100
     4.2 +++ b/src/Tools/jEdit/src/structure_matching.scala	Tue Dec 09 21:14:11 2014 +0100
     4.3 @@ -45,7 +45,7 @@
     4.4            val limit = PIDE.options.value.int("jedit_structure_limit") max 0
     4.5  
     4.6            def is_command_kind(token: Token, pred: String => Boolean): Boolean =
     4.7 -            syntax.keywords.is_command_kind(token, pred)
     4.8 +            token.is_command_kind(syntax.keywords, pred)
     4.9  
    4.10            def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
    4.11              Token_Markup.line_token_iterator(syntax, buffer, line, line + lim).