# HG changeset patch # User wenzelm # Date 1470302231 -7200 # Node ID d8de4f8b95eb87b74c4a360749c5690dfdcf569e # Parent 9d9ea2c6bc38989ed37c67554423c5008733e28d clarified modules; diff -r 9d9ea2c6bc38 -r d8de4f8b95eb src/Pure/Isar/document_structure.scala --- /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() + } +} diff -r 9d9ea2c6bc38 -r d8de4f8b95eb src/Pure/Isar/outer_syntax.scala --- 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() - } } diff -r 9d9ea2c6bc38 -r d8de4f8b95eb src/Pure/build-jars --- 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 diff -r 9d9ea2c6bc38 -r d8de4f8b95eb src/Tools/jEdit/src/isabelle_sidekick.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 }