--- 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
}