# HG changeset patch
# User wenzelm
# Date 1407782816 -7200
# Node ID fd03765b06c0db67d9ec852843875b3abced974a
# Parent  5867d1306712915c5a5a247941a835b94aa1a42f
clarified modules;

diff -r 5867d1306712 -r fd03765b06c0 src/Pure/Thy/thy_structure.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Thy/thy_structure.scala	Mon Aug 11 20:46:56 2014 +0200
@@ -0,0 +1,71 @@
+/*  Title:      Pure/Thy/thy_structure.scala
+    Author:     Makarius
+
+Nested structure of theory source.
+*/
+
+package isabelle
+
+
+import scala.collection.mutable
+import scala.annotation.tailrec
+
+
+object Thy_Structure
+{
+  sealed abstract class Entry { def length: Int }
+  case class Block(val name: String, val body: List[Entry]) extends Entry
+  {
+    val length: Int = (0 /: body)(_ + _.length)
+  }
+  case class Atom(val command: Command) extends Entry
+  {
+    def length: Int = command.length
+  }
+
+  def parse(syntax: Outer_Syntax, node_name: Document.Node.Name, text: CharSequence): Entry =
+  {
+    /* stack operations */
+
+    def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry]
+    var stack: List[(Int, String, mutable.ListBuffer[Entry])] =
+      List((0, node_name.toString, buffer()))
+
+    @tailrec def close(level: Int => Boolean)
+    {
+      stack match {
+        case (lev, name, body) :: (_, _, body2) :: rest if level(lev) =>
+          body2 += Block(name, body.toList)
+          stack = stack.tail
+          close(level)
+        case _ =>
+      }
+    }
+
+    def result(): Entry =
+    {
+      close(_ => true)
+      val (_, name, body) = stack.head
+      Block(name, body.toList)
+    }
+
+    def add(command: Command)
+    {
+      syntax.heading_level(command) match {
+        case Some(i) =>
+          close(_ > i)
+          stack = (i + 1, command.source, buffer()) :: stack
+        case None =>
+      }
+      stack.head._3 += Atom(command)
+    }
+
+
+    /* result structure */
+
+    val spans = Thy_Syntax.parse_spans(syntax.scan(text))
+    spans.foreach(span => add(Command(Document_ID.none, node_name, Nil, span)))
+    result()
+  }
+}
+
diff -r 5867d1306712 -r fd03765b06c0 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Mon Aug 11 20:30:01 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Mon Aug 11 20:46:56 2014 +0200
@@ -13,68 +13,6 @@
 
 object Thy_Syntax
 {
-  /** nested structure **/
-
-  object Structure
-  {
-    sealed abstract class Entry { def length: Int }
-    case class Block(val name: String, val body: List[Entry]) extends Entry
-    {
-      val length: Int = (0 /: body)(_ + _.length)
-    }
-    case class Atom(val command: Command) extends Entry
-    {
-      def length: Int = command.length
-    }
-
-    def parse(syntax: Outer_Syntax, node_name: Document.Node.Name, text: CharSequence): Entry =
-    {
-      /* stack operations */
-
-      def buffer(): mutable.ListBuffer[Entry] = new mutable.ListBuffer[Entry]
-      var stack: List[(Int, String, mutable.ListBuffer[Entry])] =
-        List((0, node_name.toString, buffer()))
-
-      @tailrec def close(level: Int => Boolean)
-      {
-        stack match {
-          case (lev, name, body) :: (_, _, body2) :: rest if level(lev) =>
-            body2 += Block(name, body.toList)
-            stack = stack.tail
-            close(level)
-          case _ =>
-        }
-      }
-
-      def result(): Entry =
-      {
-        close(_ => true)
-        val (_, name, body) = stack.head
-        Block(name, body.toList)
-      }
-
-      def add(command: Command)
-      {
-        syntax.heading_level(command) match {
-          case Some(i) =>
-            close(_ > i)
-            stack = (i + 1, command.source, buffer()) :: stack
-          case None =>
-        }
-        stack.head._3 += Atom(command)
-      }
-
-
-      /* result structure */
-
-      val spans = parse_spans(syntax.scan(text))
-      spans.foreach(span => add(Command(Document_ID.none, node_name, Nil, span)))
-      result()
-    }
-  }
-
-
-
   /** parse spans **/
 
   def parse_spans(toks: List[Token]): List[List[Token]] =
diff -r 5867d1306712 -r fd03765b06c0 src/Pure/build-jars
--- a/src/Pure/build-jars	Mon Aug 11 20:30:01 2014 +0200
+++ b/src/Pure/build-jars	Mon Aug 11 20:46:56 2014 +0200
@@ -83,6 +83,7 @@
   Thy/present.scala
   Thy/thy_header.scala
   Thy/thy_info.scala
+  Thy/thy_structure.scala
   Thy/thy_syntax.scala
   Tools/build.scala
   Tools/build_console.scala
diff -r 5867d1306712 -r fd03765b06c0 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Aug 11 20:30:01 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Aug 11 20:46:56 2014 +0200
@@ -95,13 +95,11 @@
     node_name: Buffer => Option[Document.Node.Name])
   extends Isabelle_Sidekick(name)
 {
-  import Thy_Syntax.Structure
-
   override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
   {
-    def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] =
+    def make_tree(offset: Text.Offset, entry: Thy_Structure.Entry): List[DefaultMutableTreeNode] =
       entry match {
-        case Structure.Block(name, body) =>
+        case Thy_Structure.Block(name, body) =>
           val node =
             new DefaultMutableTreeNode(
               new Isabelle_Sidekick.Asset(Library.first_line(name), offset, offset + entry.length))
@@ -111,7 +109,7 @@
               i + e.length
             })
           List(node)
-        case Structure.Atom(command)
+        case Thy_Structure.Atom(command)
         if command.is_command && syntax.heading_level(command).isEmpty =>
           val node =
             new DefaultMutableTreeNode(
@@ -123,7 +121,7 @@
     node_name(buffer) match {
       case Some(name) =>
         val text = JEdit_Lib.buffer_text(buffer)
-        val structure = Structure.parse(syntax, name, text)
+        val structure = Thy_Structure.parse(syntax, name, text)
         make_tree(0, structure) foreach (node => data.root.add(node))
         true
       case None => false