--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/document_structure.scala Thu Aug 04 11:17:11 2016 +0200
@@ -0,0 +1,90 @@
+/* Title: Pure/Isar/document_structure.scala
+ Author: Makarius
+
+Overall document structure.
+*/
+
+package isabelle
+
+
+import scala.collection.mutable
+import scala.annotation.tailrec
+
+
+object Document_Structure
+{
+ /** section headings etc. **/
+
+ sealed abstract class Document { def length: Int }
+ case class Block(name: String, text: String, body: List[Document]) extends Document
+ { val length: Int = (0 /: body)(_ + _.length) }
+ case class Atom(command: Command) extends Document
+ { def length: Int = command.length }
+
+ def heading_level(keywords: Keyword.Keywords, command: Command): Option[Int] =
+ {
+ val name = command.span.name
+ name match {
+ case Thy_Header.CHAPTER => Some(0)
+ case Thy_Header.SECTION => Some(1)
+ case Thy_Header.SUBSECTION => Some(2)
+ case Thy_Header.SUBSUBSECTION => Some(3)
+ case Thy_Header.PARAGRAPH => Some(4)
+ case Thy_Header.SUBPARAGRAPH => Some(5)
+ case _ =>
+ keywords.kinds.get(name) match {
+ case Some(kind) if Keyword.theory(kind) && !Keyword.theory_end(kind) => Some(6)
+ case _ => None
+ }
+ }
+ }
+
+ def parse_document(
+ syntax: Outer_Syntax,
+ node_name: Document.Node.Name,
+ text: CharSequence): List[Document] =
+ {
+ /* stack operations */
+
+ def buffer(): mutable.ListBuffer[Document] =
+ new mutable.ListBuffer[Document]
+
+ var stack: List[(Int, Command, mutable.ListBuffer[Document])] =
+ List((0, Command.empty, buffer()))
+
+ @tailrec def close(level: Int => Boolean)
+ {
+ stack match {
+ case (lev, command, body) :: (_, _, body2) :: rest if level(lev) =>
+ body2 += Block(command.span.name, command.source, body.toList)
+ stack = stack.tail
+ close(level)
+ case _ =>
+ }
+ }
+
+ def result(): List[Document] =
+ {
+ close(_ => true)
+ stack.head._3.toList
+ }
+
+ def add(command: Command)
+ {
+ heading_level(syntax.keywords, command) match {
+ case Some(i) =>
+ close(_ > i)
+ stack = (i + 1, command, 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, Command.no_blobs, span)))
+ result()
+ }
+}
--- a/src/Pure/Isar/outer_syntax.scala Thu Aug 04 10:55:51 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Thu Aug 04 11:17:11 2016 +0200
@@ -8,7 +8,6 @@
import scala.collection.mutable
-import scala.annotation.tailrec
object Outer_Syntax
@@ -42,19 +41,6 @@
result += '"'
result.toString
}
-
-
- /* overall document structure */
-
- sealed abstract class Document { def length: Int }
- case class Document_Block(name: String, text: String, body: List[Document]) extends Document
- {
- val length: Int = (0 /: body)(_ + _.length)
- }
- case class Document_Atom(command: Command) extends Document
- {
- def length: Int = command.length
- }
}
final class Outer_Syntax private(
@@ -188,72 +174,4 @@
def parse_spans(input: CharSequence): List[Command_Span.Span] =
parse_spans(Token.explode(keywords, input))
-
-
- /* overall document structure */
-
- def heading_level(command: Command): Option[Int] =
- {
- val name = command.span.name
- name match {
- case Thy_Header.CHAPTER => Some(0)
- case Thy_Header.SECTION => Some(1)
- case Thy_Header.SUBSECTION => Some(2)
- case Thy_Header.SUBSUBSECTION => Some(3)
- case Thy_Header.PARAGRAPH => Some(4)
- case Thy_Header.SUBPARAGRAPH => Some(5)
- case _ =>
- keywords.kinds.get(name) match {
- case Some(kind) if Keyword.theory(kind) && !Keyword.theory_end(kind) => Some(6)
- case _ => None
- }
- }
- }
-
- def parse_document(node_name: Document.Node.Name, text: CharSequence):
- List[Outer_Syntax.Document] =
- {
- /* stack operations */
-
- def buffer(): mutable.ListBuffer[Outer_Syntax.Document] =
- new mutable.ListBuffer[Outer_Syntax.Document]
-
- var stack: List[(Int, Command, mutable.ListBuffer[Outer_Syntax.Document])] =
- List((0, Command.empty, buffer()))
-
- @tailrec def close(level: Int => Boolean)
- {
- stack match {
- case (lev, command, body) :: (_, _, body2) :: rest if level(lev) =>
- body2 += Outer_Syntax.Document_Block(command.span.name, command.source, body.toList)
- stack = stack.tail
- close(level)
- case _ =>
- }
- }
-
- def result(): List[Outer_Syntax.Document] =
- {
- close(_ => true)
- stack.head._3.toList
- }
-
- def add(command: Command)
- {
- heading_level(command) match {
- case Some(i) =>
- close(_ > i)
- stack = (i + 1, command, 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, Command.no_blobs, span)))
- result()
- }
}
--- a/src/Pure/build-jars Thu Aug 04 10:55:51 2016 +0200
+++ b/src/Pure/build-jars Thu Aug 04 11:17:11 2016 +0200
@@ -49,6 +49,7 @@
General/url.scala
General/word.scala
General/xz_file.scala
+ Isar/document_structure.scala
Isar/keyword.scala
Isar/line_structure.scala
Isar/outer_syntax.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Aug 04 10:55:51 2016 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Aug 04 11:17:11 2016 +0200
@@ -118,11 +118,11 @@
def make_tree(
parent: DefaultMutableTreeNode,
offset: Text.Offset,
- documents: List[Outer_Syntax.Document])
+ documents: List[Document_Structure.Document])
{
(offset /: documents) { case (i, document) =>
document match {
- case Outer_Syntax.Document_Block(name, text, body) =>
+ case Document_Structure.Block(name, text, body) =>
val range = Text.Range(i, i + document.length)
val node =
new DefaultMutableTreeNode(
@@ -137,7 +137,8 @@
node_name(buffer) match {
case Some(name) =>
- make_tree(data.root, 0, syntax.parse_document(name, JEdit_Lib.buffer_text(buffer)))
+ make_tree(data.root, 0,
+ Document_Structure.parse_document(syntax, name, JEdit_Lib.buffer_text(buffer)))
true
case None => false
}