tuned signature and modules;

--- a/src/Pure/Isar/outer_syntax.scala	Sat Oct 18 22:50:35 2014 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Sun Oct 19 11:20:03 2014 +0200
@@ -9,10 +9,20 @@
 
 import scala.util.parsing.input.{Reader, CharSequenceReader}
 import scala.collection.mutable
+import scala.annotation.tailrec
 
 
 object Outer_Syntax
 {
+  /* syntax */
+
+  val empty: Outer_Syntax = new Outer_Syntax()
+
+  def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
+
+
+  /* string literals */
+
   def quote_string(str: String): String =
   {
     val result = new StringBuilder(str.length + 10)
@@ -34,10 +44,6 @@
     result.toString
   }
 
-  val empty: Outer_Syntax = new Outer_Syntax()
-
-  def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
-
 
   /* line-oriented structure */
 
@@ -52,6 +58,19 @@
     depth: Int = 0,
     span_depth: Int = 0,
     after_span_depth: Int = 0)
+
+
+  /* overall document structure */
+
+  sealed abstract class Document { def length: Int }
+  case class Document_Block(val name: String, val body: List[Document]) extends Document
+  {
+    val length: Int = (0 /: body)(_ + _.length)
+  }
+  case class Document_Atom(val command: Command) extends Document
+  {
+    def length: Int = command.length
+  }
 }
 
 final class Outer_Syntax private(
@@ -61,6 +80,8 @@
   val language_context: Completion.Language_Context = Completion.Language_Context.outer,
   val has_tokens: Boolean = true) extends Prover.Syntax
 {
+  /** syntax content **/
+
   override def toString: String =
     (for ((name, (kind, files)) <- keywords) yield {
       if (kind == Keyword.MINOR) quote(name)
@@ -134,24 +155,23 @@
     }
 
 
-  /* document headings */
+  /* language context */
 
-  def heading_level(name: String): Option[Int] =
+  def set_language_context(context: Completion.Language_Context): Outer_Syntax =
+    new Outer_Syntax(keywords, lexicon, completion, context, has_tokens)
+
+  def no_tokens: Outer_Syntax =
   {
-    keyword_kind(name) match {
-      case _ if name == "header" => Some(0)
-      case Some(Keyword.THY_HEADING1) => Some(1)
-      case Some(Keyword.THY_HEADING2) | Some(Keyword.PRF_HEADING2) => Some(2)
-      case Some(Keyword.THY_HEADING3) | Some(Keyword.PRF_HEADING3) => Some(3)
-      case Some(Keyword.THY_HEADING4) | Some(Keyword.PRF_HEADING4) => Some(4)
-      case Some(kind) if Keyword.theory(kind) => Some(5)
-      case _ => None
-    }
+    require(keywords.isEmpty && lexicon.isEmpty)
+    new Outer_Syntax(
+      completion = completion,
+      language_context = language_context,
+      has_tokens = false)
   }
 
-  def heading_level(command: Command): Option[Int] =
-    heading_level(command.name)
+
 
+  /** parsing **/
 
   /* line-oriented structure */
 
@@ -217,7 +237,7 @@
   }
 
 
-  /* parse_spans */
+  /* command spans */
 
   def parse_spans(toks: List[Token]): List[Command_Span.Span] =
   {
@@ -258,17 +278,65 @@
     parse_spans(scan(input))
 
 
-  /* language context */
+  /* overall document structure */
 
-  def set_language_context(context: Completion.Language_Context): Outer_Syntax =
-    new Outer_Syntax(keywords, lexicon, completion, context, has_tokens)
+  def heading_level(command: Command): Option[Int] =
+  {
+    keyword_kind(command.name) match {
+      case _ if command.name == "header" => Some(0)
+      case Some(Keyword.THY_HEADING1) => Some(1)
+      case Some(Keyword.THY_HEADING2) | Some(Keyword.PRF_HEADING2) => Some(2)
+      case Some(Keyword.THY_HEADING3) | Some(Keyword.PRF_HEADING3) => Some(3)
+      case Some(Keyword.THY_HEADING4) | Some(Keyword.PRF_HEADING4) => Some(4)
+      case Some(kind) if Keyword.theory(kind) => Some(5)
+      case _ => None
+    }
+  }
+
+  def parse_document(node_name: Document.Node.Name, text: CharSequence): Outer_Syntax.Document =
+  {
+    /* stack operations */
+
+    def buffer(): mutable.ListBuffer[Outer_Syntax.Document] =
+      new mutable.ListBuffer[Outer_Syntax.Document]
+
+    var stack: List[(Int, String, mutable.ListBuffer[Outer_Syntax.Document])] =
+      List((0, node_name.toString, buffer()))
 
-  def no_tokens: Outer_Syntax =
-  {
-    require(keywords.isEmpty && lexicon.isEmpty)
-    new Outer_Syntax(
-      completion = completion,
-      language_context = language_context,
-      has_tokens = false)
+    @tailrec def close(level: Int => Boolean)
+    {
+      stack match {
+        case (lev, name, body) :: (_, _, body2) :: rest if level(lev) =>
+          body2 += Outer_Syntax.Document_Block(name, body.toList)
+          stack = stack.tail
+          close(level)
+        case _ =>
+      }
+    }
+
+    def result(): Outer_Syntax.Document =
+    {
+      close(_ => true)
+      val (_, name, body) = stack.head
+      Outer_Syntax.Document_Block(name, body.toList)
+    }
+
+    def add(command: Command)
+    {
+      heading_level(command) match {
+        case Some(i) =>
+          close(_ > i)
+          stack = (i + 1, command.source, buffer()) :: stack
+        case None =>
+      }
+      stack.head._3 += Outer_Syntax.Document_Atom(command)
+    }
+
+
+    /* result structure */
+
+    val spans = parse_spans(text)
+    spans.foreach(span => add(Command(Document_ID.none, node_name, Nil, span)))
+    result()
   }
 }

--- a/src/Pure/Thy/thy_structure.scala	Sat Oct 18 22:50:35 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,71 +0,0 @@
-/*  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 = syntax.parse_spans(text)
-    spans.foreach(span => add(Command(Document_ID.none, node_name, Nil, span)))
-    result()
-  }
-}
-

--- a/src/Pure/build-jars	Sat Oct 18 22:50:35 2014 +0200
+++ b/src/Pure/build-jars	Sun Oct 19 11:20:03 2014 +0200
@@ -83,7 +83,6 @@
   Thy/present.scala
   Thy/thy_header.scala
   Thy/thy_info.scala
-  Thy/thy_structure.scala
   Thy/thy_syntax.scala
   Tools/bibtex.scala
   Tools/build.scala

--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Sat Oct 18 22:50:35 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Sun Oct 19 11:20:03 2014 +0200
@@ -101,32 +101,34 @@
 {
   override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
   {
-    def make_tree(offset: Text.Offset, entry: Thy_Structure.Entry): List[DefaultMutableTreeNode] =
-      entry match {
-        case Thy_Structure.Block(name, body) =>
+    def make_tree(offset: Text.Offset, document: Outer_Syntax.Document)
+        : List[DefaultMutableTreeNode] =
+      document match {
+        case Outer_Syntax.Document_Block(name, body) =>
           val node =
             new DefaultMutableTreeNode(
-              new Isabelle_Sidekick.Asset(Library.first_line(name), offset, offset + entry.length))
-          (offset /: body)((i, e) =>
+              new Isabelle_Sidekick.Asset(
+                Library.first_line(name), offset, offset + document.length))
+          (offset /: body)((i, doc) =>
             {
-              make_tree(i, e) foreach (nd => node.add(nd))
-              i + e.length
+              for (nd <- make_tree(i, doc)) node.add(nd)
+              i + doc.length
             })
           List(node)
-        case Thy_Structure.Atom(command)
+
+        case Outer_Syntax.Document_Atom(command)
         if command.is_proper && syntax.heading_level(command).isEmpty =>
           val node =
             new DefaultMutableTreeNode(
-              new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length))
+              new Isabelle_Sidekick.Asset(command.name, offset, offset + document.length))
           List(node)
         case _ => Nil
       }
 
     node_name(buffer) match {
       case Some(name) =>
-        val text = JEdit_Lib.buffer_text(buffer)
-        val structure = Thy_Structure.parse(syntax, name, text)
-        make_tree(0, structure) foreach (node => data.root.add(node))
+        val document = syntax.parse_document(name, JEdit_Lib.buffer_text(buffer))
+        for (node <- make_tree(0, document)) data.root.add(node)
         true
       case None => false
     }