--- a/src/Pure/Isar/outer_syntax.scala Thu Oct 16 12:09:57 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Thu Oct 16 12:24:19 2014 +0200
@@ -54,9 +54,21 @@
(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
+ }
+
+
+ /* load commands */
+
def load_command(name: String): Option[List[String]] =
keywords.get(name) match {
case Some((Keyword.THY_LOAD, exts)) => Some(exts)
@@ -69,6 +81,9 @@
def load_commands_in(text: String): Boolean =
load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
+
+ /* add keywords */
+
def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax =
{
val keywords1 = keywords + (name -> kind)
@@ -99,11 +114,8 @@
(Symbol.encode(name), replace)
}
- def is_command(name: String): Boolean =
- keyword_kind(name) match {
- case Some(kind) => kind != Keyword.MINOR
- case None => false
- }
+
+ /* document headings */
def heading_level(name: String): Option[Int] =
{