tuned comments;
authorwenzelm
Thu Oct 16 12:24:19 2014 +0200 (2014-10-16)
changeset 5869591839729224e
parent 58694 983e98da2a42
child 58696 6b7445774ce3
tuned comments;
src/Pure/Isar/outer_syntax.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Thu Oct 16 12:09:57 2014 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Thu Oct 16 12:24:19 2014 +0200
     1.3 @@ -54,9 +54,21 @@
     1.4          (if (files.isEmpty) "" else " (" + commas_quote(files) + ")")
     1.5      }).toList.sorted.mkString("keywords\n  ", " and\n  ", "")
     1.6  
     1.7 +
     1.8 +  /* keyword kind */
     1.9 +
    1.10    def keyword_kind_files(name: String): Option[(String, List[String])] = keywords.get(name)
    1.11    def keyword_kind(name: String): Option[String] = keyword_kind_files(name).map(_._1)
    1.12  
    1.13 +  def is_command(name: String): Boolean =
    1.14 +    keyword_kind(name) match {
    1.15 +      case Some(kind) => kind != Keyword.MINOR
    1.16 +      case None => false
    1.17 +    }
    1.18 +
    1.19 +
    1.20 +  /* load commands */
    1.21 +
    1.22    def load_command(name: String): Option[List[String]] =
    1.23      keywords.get(name) match {
    1.24        case Some((Keyword.THY_LOAD, exts)) => Some(exts)
    1.25 @@ -69,6 +81,9 @@
    1.26    def load_commands_in(text: String): Boolean =
    1.27      load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
    1.28  
    1.29 +
    1.30 +  /* add keywords */
    1.31 +
    1.32    def + (name: String, kind: (String, List[String]), replace: Option[String]): Outer_Syntax =
    1.33    {
    1.34      val keywords1 = keywords + (name -> kind)
    1.35 @@ -99,11 +114,8 @@
    1.36            (Symbol.encode(name), replace)
    1.37      }
    1.38  
    1.39 -  def is_command(name: String): Boolean =
    1.40 -    keyword_kind(name) match {
    1.41 -      case Some(kind) => kind != Keyword.MINOR
    1.42 -      case None => false
    1.43 -    }
    1.44 +
    1.45 +  /* document headings */
    1.46  
    1.47    def heading_level(name: String): Option[Int] =
    1.48    {