--- 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 =
--- 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) })
+ }
}
--- 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
}
--- 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))))
}
--- 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])]
}
--- 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)
--- 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
}