# HG changeset patch
# User wenzelm
# Date 1413455059 -7200
# Node ID 91839729224eaaf8691eb1e06ab205884abc2a1f
# Parent  983e98da2a42a13b669b8ab5c6d7f9416287cbd8
tuned comments;

diff -r 983e98da2a42 -r 91839729224e src/Pure/Isar/outer_syntax.scala
--- 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] =
   {