# HG changeset patch # User wenzelm # Date 1415205445 -3600 # Node ID 47809a811ebae6f2dfae146c9866beb12ce93c5e # Parent 1435cc20b022d6573bb80bf738c1f6237df849aa clarified representation of type Keywords; tuned signature; diff -r 1435cc20b022 -r 47809a811eba src/Pure/Isar/keyword.scala --- a/src/Pure/Isar/keyword.scala Wed Nov 05 16:57:12 2014 +0100 +++ b/src/Pure/Isar/keyword.scala Wed Nov 05 17:37:25 2014 +0100 @@ -13,7 +13,6 @@ /* kinds */ - val MINOR = "minor" val DIAG = "diag" val HEADING = "heading" val THY_BEGIN = "thy_begin" @@ -74,55 +73,59 @@ { def empty: Keywords = new Keywords() - def apply(names: List[String]): Keywords = - (empty /: names)({ case (keywords, a) => keywords + (a, (MINOR, Nil)) }) + def apply(keywords: List[String]): Keywords = (empty /: keywords)(_ + _) } 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) + val major: Scan.Lexicon = Scan.Lexicon.empty, + command_kinds: Map[String, (String, List[String])] = Map.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 = minor.isEmpty && major.isEmpty - def is_empty: Boolean = keywords.isEmpty + def + (name: String): Keywords = + new Keywords(minor + name, major, command_kinds) 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) + val major1 = major + name + val command_kinds1 = command_kinds + (name -> kind) + new Keywords(minor, major1, command_kinds1) + } + + override def toString: String = + { + val keywords = minor.iterator.map(quote(_)).toList + val commands = + for ((name, (kind, files)) <- command_kinds.toList.sortBy(_._1)) yield { + quote(name) + " :: " + quote(kind) + + (if (files.isEmpty) "" else " (" + commas_quote(files) + ")") + } + (keywords ::: commands).mkString("keywords\n ", " and\n ", "") } - /* kind */ + /* command kind */ - def kind(name: String): Option[String] = keywords.get(name).map(_._1) + def command_kind(name: String): Option[String] = command_kinds.get(name).map(_._1) - def command_kind(token: Token, pred: String => Boolean): Boolean = + def is_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 }) + (command_kind(token.source) match { case Some(k) => pred(k) case None => false }) /* load commands */ def load_command(name: String): Option[List[String]] = - keywords.get(name) match { + command_kinds.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 + (for ((name, (THY_LOAD, files)) <- command_kinds.iterator) yield (name, files)).toList def load_commands_in(text: String): Boolean = load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) }) diff -r 1435cc20b022 -r 47809a811eba src/Pure/Isar/outer_syntax.scala --- a/src/Pure/Isar/outer_syntax.scala Wed Nov 05 16:57:12 2014 +0100 +++ b/src/Pure/Isar/outer_syntax.scala Wed Nov 05 17:37:25 2014 +0100 @@ -86,33 +86,29 @@ /* add keywords */ - def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax = + def + (name: String, opt_kind: Option[(String, List[String])], replace: Option[String]) + : Outer_Syntax = { - val keywords1 = keywords + (name, kind) + val keywords1 = + opt_kind match { + case None => keywords + name + case Some(kind) => keywords + (name, kind) + } val completion1 = if (replace == Some("")) completion else completion + (name, replace getOrElse name) new Outer_Syntax(keywords1, completion1, language_context, true) } - - def + (name: String, kind: (String, List[String])): Outer_Syntax = - this + (name, kind, Some(name)) - def + (name: String, kind: String): Outer_Syntax = - this + (name, (kind, Nil), Some(name)) - def + (name: String, replace: Option[String]): Outer_Syntax = - this + (name, (Keyword.MINOR, Nil), replace) - def + (name: String): Outer_Syntax = this + (name, None) + def + (name: String): Outer_Syntax = this + (name, None, None) + def + (name: String, kind: String): Outer_Syntax = this + (name, Some((kind, Nil)), None) def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax = (this /: keywords) { - case (syntax, (name, Some((kind, _)), replace)) => + case (syntax, (name, opt_spec, replace)) => + val opt_kind = opt_spec.map(_._1) syntax + - (Symbol.decode(name), kind, replace) + - (Symbol.encode(name), kind, replace) - case (syntax, (name, None, replace)) => - syntax + - (Symbol.decode(name), replace) + - (Symbol.encode(name), replace) + (Symbol.decode(name), opt_kind, replace) + + (Symbol.encode(name), opt_kind, replace) } @@ -149,7 +145,7 @@ val command1 = tokens.exists(_.is_command) val depth1 = - if (tokens.exists(tok => keywords.command_kind(tok, Keyword.theory))) 0 + if (tokens.exists(tok => keywords.is_command_kind(tok, Keyword.theory))) 0 else if (command1) struct.after_span_depth else struct.span_depth @@ -157,15 +153,15 @@ ((struct.span_depth, struct.after_span_depth) /: tokens) { case ((x, y), tok) => if (tok.is_command) { - if (keywords.command_kind(tok, Keyword.theory_goal)) + if (keywords.is_command_kind(tok, Keyword.theory_goal)) (2, 1) - else if (keywords.command_kind(tok, Keyword.theory)) + else if (keywords.is_command_kind(tok, Keyword.theory)) (1, 0) - else if (keywords.command_kind(tok, Keyword.proof_goal) || tok.is_begin_block) + else if (keywords.is_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) + else if (keywords.is_command_kind(tok, Keyword.qed) || tok.is_end_block) (y + 1, y - 1) - else if (keywords.command_kind(tok, Keyword.qed_global)) + else if (keywords.is_command_kind(tok, Keyword.qed_global)) (1, 0) else (x, y) } @@ -254,7 +250,7 @@ case "subsection" => Some(2) case "subsubsection" => Some(3) case _ => - keywords.kind(command.name) match { + keywords.command_kind(command.name) match { case Some(kind) if Keyword.theory(kind) => Some(4) case _ => None } diff -r 1435cc20b022 -r 47809a811eba src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Wed Nov 05 16:57:12 2014 +0100 +++ b/src/Tools/jEdit/src/rendering.scala Wed Nov 05 17:37:25 2014 +0100 @@ -85,7 +85,7 @@ } def token_markup(syntax: Outer_Syntax, token: Token): Byte = - if (token.is_command) command_style(syntax.keywords.kind(token.content).getOrElse("")) + if (token.is_command) command_style(syntax.keywords.command_kind(token.content).getOrElse("")) else if (token.is_delimiter) JEditToken.OPERATOR else token_style(token.kind) diff -r 1435cc20b022 -r 47809a811eba src/Tools/jEdit/src/structure_matching.scala --- a/src/Tools/jEdit/src/structure_matching.scala Wed Nov 05 16:57:12 2014 +0100 +++ b/src/Tools/jEdit/src/structure_matching.scala Wed Nov 05 17:37:25 2014 +0100 @@ -44,8 +44,8 @@ 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 is_command_kind(token: Token, pred: String => Boolean): Boolean = + syntax.keywords.is_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). @@ -63,45 +63,45 @@ iterator(caret_line, 1).find(info => info.range.touches(caret)) match { - case Some(Text.Info(range1, tok)) if command_kind(tok, Keyword.theory_goal) => + case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.theory_goal) => find_block( - command_kind(_, Keyword.proof_goal), - command_kind(_, Keyword.qed), - command_kind(_, Keyword.qed_global), + is_command_kind(_, Keyword.proof_goal), + is_command_kind(_, Keyword.qed), + is_command_kind(_, Keyword.qed_global), t => - command_kind(t, Keyword.diag) || - command_kind(t, Keyword.proof), + is_command_kind(t, Keyword.diag) || + is_command_kind(t, Keyword.proof), caret_iterator()) - case Some(Text.Info(range1, tok)) if command_kind(tok, Keyword.proof_goal) => + case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.proof_goal) => find_block( - command_kind(_, Keyword.proof_goal), - command_kind(_, Keyword.qed), + is_command_kind(_, Keyword.proof_goal), + is_command_kind(_, Keyword.qed), _ => false, t => - command_kind(t, Keyword.diag) || - command_kind(t, Keyword.proof), + is_command_kind(t, Keyword.diag) || + is_command_kind(t, Keyword.proof), caret_iterator()) - case Some(Text.Info(range1, tok)) if command_kind(tok, Keyword.qed_global) => - rev_caret_iterator().find(info => command_kind(info.info, Keyword.theory)) + case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.qed_global) => + rev_caret_iterator().find(info => is_command_kind(info.info, Keyword.theory)) match { case Some(Text.Info(range2, tok)) - if command_kind(tok, Keyword.theory_goal) => Some((range1, range2)) + if is_command_kind(tok, Keyword.theory_goal) => Some((range1, range2)) case _ => None } - case Some(Text.Info(range1, tok)) if command_kind(tok, Keyword.qed) => + case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.qed) => find_block( - command_kind(_, Keyword.qed), + is_command_kind(_, Keyword.qed), t => - command_kind(t, Keyword.proof_goal) || - command_kind(t, Keyword.theory_goal), + is_command_kind(t, Keyword.proof_goal) || + is_command_kind(t, Keyword.theory_goal), _ => false, t => - command_kind(t, Keyword.diag) || - command_kind(t, Keyword.proof) || - command_kind(t, Keyword.theory_goal), + is_command_kind(t, Keyword.diag) || + is_command_kind(t, Keyword.proof) || + is_command_kind(t, Keyword.theory_goal), rev_caret_iterator()) case Some(Text.Info(range1, tok)) if tok.is_begin => @@ -117,7 +117,7 @@ find(info => info.info.is_command || info.info.is_begin) match { case Some(Text.Info(range3, tok)) => - if (command_kind(tok, Keyword.theory_block)) Some((range1, range3)) + if (is_command_kind(tok, Keyword.theory_block)) Some((range1, range3)) else Some((range1, range2)) case None => None }