# HG changeset patch # User wenzelm # Date 1415203032 -3600 # Node ID 1435cc20b022d6573bb80bf738c1f6237df849aa # Parent 0a793c580685bc03bef0cad634ff7a13e414959c explicit type Keyword.Keywords; diff -r 0a793c580685 -r 1435cc20b022 src/Pure/Isar/keyword.ML --- a/src/Pure/Isar/keyword.ML Wed Nov 05 15:32:11 2014 +0100 +++ b/src/Pure/Isar/keyword.ML Wed Nov 05 16:57:12 2014 +0100 @@ -1,7 +1,7 @@ (* Title: Pure/Isar/keyword.ML Author: Makarius -Isar command keyword classification and global keyword tables. +Isar keyword classification. *) signature KEYWORD = diff -r 0a793c580685 -r 1435cc20b022 src/Pure/Isar/keyword.scala --- a/src/Pure/Isar/keyword.scala Wed Nov 05 15:32:11 2014 +0100 +++ b/src/Pure/Isar/keyword.scala Wed Nov 05 16:57:12 2014 +0100 @@ -1,7 +1,7 @@ /* Title: Pure/Isar/keyword.scala Author: Makarius -Isar command keyword classification and keyword tables. +Isar keyword classification. */ package isabelle @@ -9,6 +9,8 @@ object Keyword { + /** keyword classification **/ + /* kinds */ val MINOR = "minor" @@ -60,5 +62,70 @@ val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT) val qed = Set(QED, QED_SCRIPT, QED_BLOCK) val qed_global = Set(QED_GLOBAL) + + + type Spec = ((String, List[String]), List[String]) + + + + /** keyword tables **/ + + object Keywords + { + def empty: Keywords = new Keywords() + + def apply(names: List[String]): Keywords = + (empty /: names)({ case (keywords, a) => keywords + (a, (MINOR, Nil)) }) + } + + class Keywords private( + keywords: Map[String, (String, List[String])] = Map.empty, + val minor: Scan.Lexicon = Scan.Lexicon.empty, + val major: Scan.Lexicon = Scan.Lexicon.empty) + { + /* content */ + + override def toString: String = + (for ((name, (kind, files)) <- keywords) yield { + if (kind == MINOR) quote(name) + else + quote(name) + " :: " + quote(kind) + + (if (files.isEmpty) "" else " (" + commas_quote(files) + ")") + }).toList.sorted.mkString("keywords\n ", " and\n ", "") + + def is_empty: Boolean = keywords.isEmpty + + def + (name: String, kind: (String, List[String])): Keywords = + { + val keywords1 = keywords + (name -> kind) + val (minor1, major1) = + if (kind._1 == MINOR) (minor + name, major) else (minor, major + name) + new Keywords(keywords1, minor1, major1) + } + + + /* kind */ + + def kind(name: String): Option[String] = keywords.get(name).map(_._1) + + def command_kind(token: Token, pred: String => Boolean): Boolean = + token.is_command && + (kind(token.source) match { case Some(k) => k != MINOR && pred(k) case None => false }) + + + /* load commands */ + + def load_command(name: String): Option[List[String]] = + keywords.get(name) match { + case Some((THY_LOAD, exts)) => Some(exts) + case _ => None + } + + private lazy val load_commands: List[(String, List[String])] = + (for ((name, (THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList + + def load_commands_in(text: String): Boolean = + load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) }) + } } diff -r 0a793c580685 -r 1435cc20b022 src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Wed Nov 05 15:32:11 2014 +0100 +++ b/src/Pure/Isar/outer_syntax.scala Wed Nov 05 16:57:12 2014 +0100 @@ -74,66 +74,25 @@ } final class Outer_Syntax private( - keywords: Map[String, (String, List[String])] = Map.empty, - minor: Scan.Lexicon = Scan.Lexicon.empty, - major: Scan.Lexicon = Scan.Lexicon.empty, + val keywords: Keyword.Keywords = Keyword.Keywords.empty, val completion: Completion = Completion.empty, val language_context: Completion.Language_Context = Completion.Language_Context.outer, val has_tokens: Boolean = true) extends Prover.Syntax { /** syntax content **/ - override def toString: String = - (for ((name, (kind, files)) <- keywords) yield { - if (kind == Keyword.MINOR) quote(name) - else - quote(name) + " :: " + quote(kind) + - (if (files.isEmpty) "" else " (" + commas_quote(files) + ")") - }).toList.sorted.mkString("keywords\n ", " and\n ", "") - - - /* keyword kind */ - - def keyword_kind_files(name: String): Option[(String, List[String])] = keywords.get(name) - def keyword_kind(name: String): Option[String] = keyword_kind_files(name).map(_._1) - - def is_command(name: String): Boolean = - keyword_kind(name) match { - case Some(kind) => kind != Keyword.MINOR - case None => false - } - - def command_kind(token: Token, pred: String => Boolean): Boolean = - token.is_command && is_command(token.source) && - pred(keyword_kind(token.source).get) - - - /* load commands */ - - def load_command(name: String): Option[List[String]] = - keywords.get(name) match { - case Some((Keyword.THY_LOAD, exts)) => Some(exts) - case _ => None - } - - val load_commands: List[(String, List[String])] = - (for ((name, (Keyword.THY_LOAD, files)) <- keywords.iterator) yield (name, files)).toList - - def load_commands_in(text: String): Boolean = - load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) }) + override def toString: String = keywords.toString /* add keywords */ def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax = { - val keywords1 = keywords + (name -> kind) - val (minor1, major1) = - if (kind._1 == Keyword.MINOR) (minor + name, major) else (minor, major + name) + val keywords1 = keywords + (name, kind) val completion1 = if (replace == Some("")) completion else completion + (name, replace getOrElse name) - new Outer_Syntax(keywords1, minor1, major1, completion1, language_context, true) + new Outer_Syntax(keywords1, completion1, language_context, true) } def + (name: String, kind: (String, List[String])): Outer_Syntax = @@ -157,14 +116,20 @@ } + /* load commands */ + + def load_command(name: String): Option[List[String]] = keywords.load_command(name) + def load_commands_in(text: String): Boolean = keywords.load_commands_in(text) + + /* language context */ def set_language_context(context: Completion.Language_Context): Outer_Syntax = - new Outer_Syntax(keywords, minor, major, completion, context, has_tokens) + new Outer_Syntax(keywords, completion, context, has_tokens) def no_tokens: Outer_Syntax = { - require(keywords.isEmpty && minor.isEmpty && major.isEmpty) + require(keywords.is_empty) new Outer_Syntax( completion = completion, language_context = language_context, @@ -184,7 +149,7 @@ val command1 = tokens.exists(_.is_command) val depth1 = - if (tokens.exists(tok => command_kind(tok, Keyword.theory))) 0 + if (tokens.exists(tok => keywords.command_kind(tok, Keyword.theory))) 0 else if (command1) struct.after_span_depth else struct.span_depth @@ -192,11 +157,16 @@ ((struct.span_depth, struct.after_span_depth) /: tokens) { case ((x, y), tok) => if (tok.is_command) { - if (command_kind(tok, Keyword.theory_goal)) (2, 1) - else if (command_kind(tok, Keyword.theory)) (1, 0) - else if (command_kind(tok, Keyword.proof_goal) || tok.is_begin_block) (y + 2, y + 1) - else if (command_kind(tok, Keyword.qed) || tok.is_end_block) (y + 1, y - 1) - else if (command_kind(tok, Keyword.qed_global)) (1, 0) + if (keywords.command_kind(tok, Keyword.theory_goal)) + (2, 1) + else if (keywords.command_kind(tok, Keyword.theory)) + (1, 0) + else if (keywords.command_kind(tok, Keyword.proof_goal) || tok.is_begin_block) + (y + 2, y + 1) + else if (keywords.command_kind(tok, Keyword.qed) || tok.is_end_block) + (y + 1, y - 1) + else if (keywords.command_kind(tok, Keyword.qed_global)) + (1, 0) else (x, y) } else (x, y) @@ -211,7 +181,7 @@ def scan(input: CharSequence): List[Token] = { val in: Reader[Char] = new CharSequenceReader(input) - Token.Parsers.parseAll(Token.Parsers.rep(Token.Parsers.token(minor, major)), in) match { + Token.Parsers.parseAll(Token.Parsers.rep(Token.Parsers.token(keywords)), in) match { case Token.Parsers.Success(tokens, _) => tokens case _ => error("Unexpected failure of tokenizing input:\n" + input.toString) } @@ -223,7 +193,7 @@ val toks = new mutable.ListBuffer[Token] var ctxt = context while (!in.atEnd) { - Token.Parsers.parse(Token.Parsers.token_line(minor, major, ctxt), in) match { + Token.Parsers.parse(Token.Parsers.token_line(keywords, ctxt), in) match { case Token.Parsers.Success((x, c), rest) => { toks += x; ctxt = c; in = rest } case Token.Parsers.NoSuccess(_, rest) => error("Unexpected failure of tokenizing input:\n" + rest.source.toString) @@ -284,7 +254,7 @@ case "subsection" => Some(2) case "subsubsection" => Some(3) case _ => - keyword_kind(command.name) match { + keywords.kind(command.name) match { case Some(kind) if Keyword.theory(kind) => Some(4) case _ => None } diff -r 0a793c580685 -r 1435cc20b022 src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Wed Nov 05 15:32:11 2014 +0100 +++ b/src/Pure/Isar/token.scala Wed Nov 05 16:57:12 2014 +0100 @@ -51,7 +51,7 @@ string | (alt_string | (verb | (cart | cmt))) } - private def other_token(minor: Scan.Lexicon, major: Scan.Lexicon): Parser[Token] = + private def other_token(keywords: Keyword.Keywords): Parser[Token] = { val letdigs1 = many1(Symbol.is_letdig) val sub = one(s => s == Symbol.sub_decoded || s == "\\<^sub>") @@ -80,8 +80,8 @@ (x => Token(Token.Kind.SYM_IDENT, x)) val keyword = - literal(minor) ^^ (x => Token(Token.Kind.KEYWORD, x)) ||| - literal(major) ^^ (x => Token(Token.Kind.COMMAND, x)) + literal(keywords.minor) ^^ (x => Token(Token.Kind.KEYWORD, x)) ||| + literal(keywords.major) ^^ (x => Token(Token.Kind.COMMAND, x)) val space = many1(Symbol.is_blank) ^^ (x => Token(Token.Kind.SPACE, x)) @@ -98,10 +98,10 @@ keyword) | bad)) } - def token(minor: Scan.Lexicon, major: Scan.Lexicon): Parser[Token] = - delimited_token | other_token(minor, major) + def token(keywords: Keyword.Keywords): Parser[Token] = + delimited_token | other_token(keywords) - def token_line(minor: Scan.Lexicon, major: Scan.Lexicon, ctxt: Scan.Line_Context) + def token_line(keywords: Keyword.Keywords, ctxt: Scan.Line_Context) : Parser[(Token, Scan.Line_Context)] = { val string = @@ -111,7 +111,7 @@ val verb = verbatim_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.VERBATIM, x), c) } val cart = cartouche_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.CARTOUCHE, x), c) } val cmt = comment_line(ctxt) ^^ { case (x, c) => (Token(Token.Kind.COMMENT, x), c) } - val other = other_token(minor, major) ^^ { case x => (x, Scan.Finished) } + val other = other_token(keywords) ^^ { case x => (x, Scan.Finished) } string | (alt_string | (verb | (cart | (cmt | other)))) } diff -r 0a793c580685 -r 1435cc20b022 src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Wed Nov 05 15:32:11 2014 +0100 +++ b/src/Pure/Thy/thy_header.scala Wed Nov 05 16:57:12 2014 +0100 @@ -27,9 +27,10 @@ val AND = "and" val BEGIN = "begin" - private val lexicon = - Scan.Lexicon("%", "(", ")", ",", "::", "==", AND, BEGIN, - HEADER, CHAPTER, SECTION, SUBSECTION, SUBSUBSECTION, IMPORTS, KEYWORDS, THEORY) + private val keywords = + Keyword.Keywords( + List("%", "(", ")", ",", "::", "==", AND, BEGIN, + HEADER, CHAPTER, SECTION, SUBSECTION, SUBSUBSECTION, IMPORTS, KEYWORDS, THEORY)) /* theory file name */ @@ -95,7 +96,7 @@ def read(reader: Reader[Char]): Thy_Header = { - val token = Token.Parsers.token(lexicon, Scan.Lexicon.empty) + val token = Token.Parsers.token(keywords) val toks = new mutable.ListBuffer[Token] @tailrec def scan_to_begin(in: Reader[Char]) @@ -121,7 +122,7 @@ /* keywords */ - type Keywords = List[(String, Option[((String, List[String]), List[String])], Option[String])] + type Keywords = List[(String, Option[Keyword.Spec], Option[String])] } diff -r 0a793c580685 -r 1435cc20b022 src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Wed Nov 05 15:32:11 2014 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Wed Nov 05 16:57:12 2014 +0100 @@ -85,7 +85,7 @@ } def token_markup(syntax: Outer_Syntax, token: Token): Byte = - if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse("")) + if (token.is_command) command_style(syntax.keywords.kind(token.content).getOrElse("")) else if (token.is_delimiter) JEditToken.OPERATOR else token_style(token.kind) diff -r 0a793c580685 -r 1435cc20b022 src/Tools/jEdit/src/structure_matching.scala --- a/src/Tools/jEdit/src/structure_matching.scala Wed Nov 05 15:32:11 2014 +0100 +++ b/src/Tools/jEdit/src/structure_matching.scala Wed Nov 05 16:57:12 2014 +0100 @@ -44,6 +44,9 @@ case Some(syntax) => val limit = PIDE.options.value.int("jedit_structure_limit") max 0 + def command_kind(token: Token, pred: String => Boolean): Boolean = + syntax.keywords.command_kind(token, pred) + def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] = Token_Markup.line_token_iterator(syntax, buffer, line, line + lim). filter(_.info.is_proper) @@ -60,45 +63,45 @@ iterator(caret_line, 1).find(info => info.range.touches(caret)) match { - case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.theory_goal) => + case Some(Text.Info(range1, tok)) if command_kind(tok, Keyword.theory_goal) => find_block( - syntax.command_kind(_, Keyword.proof_goal), - syntax.command_kind(_, Keyword.qed), - syntax.command_kind(_, Keyword.qed_global), + command_kind(_, Keyword.proof_goal), + command_kind(_, Keyword.qed), + command_kind(_, Keyword.qed_global), t => - syntax.command_kind(t, Keyword.diag) || - syntax.command_kind(t, Keyword.proof), + command_kind(t, Keyword.diag) || + command_kind(t, Keyword.proof), caret_iterator()) - case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.proof_goal) => + case Some(Text.Info(range1, tok)) if command_kind(tok, Keyword.proof_goal) => find_block( - syntax.command_kind(_, Keyword.proof_goal), - syntax.command_kind(_, Keyword.qed), + command_kind(_, Keyword.proof_goal), + command_kind(_, Keyword.qed), _ => false, t => - syntax.command_kind(t, Keyword.diag) || - syntax.command_kind(t, Keyword.proof), + command_kind(t, Keyword.diag) || + command_kind(t, Keyword.proof), caret_iterator()) - case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.qed_global) => - rev_caret_iterator().find(info => syntax.command_kind(info.info, Keyword.theory)) + case Some(Text.Info(range1, tok)) if command_kind(tok, Keyword.qed_global) => + rev_caret_iterator().find(info => command_kind(info.info, Keyword.theory)) match { case Some(Text.Info(range2, tok)) - if syntax.command_kind(tok, Keyword.theory_goal) => Some((range1, range2)) + if command_kind(tok, Keyword.theory_goal) => Some((range1, range2)) case _ => None } - case Some(Text.Info(range1, tok)) if syntax.command_kind(tok, Keyword.qed) => + case Some(Text.Info(range1, tok)) if command_kind(tok, Keyword.qed) => find_block( - syntax.command_kind(_, Keyword.qed), + command_kind(_, Keyword.qed), t => - syntax.command_kind(t, Keyword.proof_goal) || - syntax.command_kind(t, Keyword.theory_goal), + command_kind(t, Keyword.proof_goal) || + command_kind(t, Keyword.theory_goal), _ => false, t => - syntax.command_kind(t, Keyword.diag) || - syntax.command_kind(t, Keyword.proof) || - syntax.command_kind(t, Keyword.theory_goal), + command_kind(t, Keyword.diag) || + command_kind(t, Keyword.proof) || + command_kind(t, Keyword.theory_goal), rev_caret_iterator()) case Some(Text.Info(range1, tok)) if tok.is_begin => @@ -114,7 +117,7 @@ find(info => info.info.is_command || info.info.is_begin) match { case Some(Text.Info(range3, tok)) => - if (syntax.command_kind(tok, Keyword.theory_block)) Some((range1, range3)) + if (command_kind(tok, Keyword.theory_block)) Some((range1, range3)) else Some((range1, range2)) case None => None }