# HG changeset patch
# User wenzelm
# Date 1470303141 -7200
# Node ID c7916060f55e983edae2109d9ae0dbfe9c137579
# Parent  d8de4f8b95eb87b74c4a360749c5690dfdcf569e
tuned;

diff -r d8de4f8b95eb -r c7916060f55e src/Pure/Isar/document_structure.scala
--- a/src/Pure/Isar/document_structure.scala	Thu Aug 04 11:17:11 2016 +0200
+++ b/src/Pure/Isar/document_structure.scala	Thu Aug 04 11:32:21 2016 +0200
@@ -13,7 +13,7 @@
 
 object Document_Structure
 {
-  /** section headings etc. **/
+  /* general structure */
 
   sealed abstract class Document { def length: Int }
   case class Block(name: String, text: String, body: List[Document]) extends Document
@@ -21,6 +21,9 @@
   case class Atom(command: Command) extends Document
   { def length: Int = command.length }
 
+
+  /* section headings etc. */
+
   def heading_level(keywords: Keyword.Keywords, command: Command): Option[Int] =
   {
     val name = command.span.name
@@ -39,7 +42,7 @@
     }
   }
 
-  def parse_document(
+  def parse_sections(
     syntax: Outer_Syntax,
     node_name: Document.Node.Name,
     text: CharSequence): List[Document] =
diff -r d8de4f8b95eb -r c7916060f55e src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Aug 04 11:17:11 2016 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Aug 04 11:32:21 2016 +0200
@@ -138,7 +138,7 @@
     node_name(buffer) match {
       case Some(name) =>
         make_tree(data.root, 0,
-          Document_Structure.parse_document(syntax, name, JEdit_Lib.buffer_text(buffer)))
+          Document_Structure.parse_sections(syntax, name, JEdit_Lib.buffer_text(buffer)))
         true
       case None => false
     }