# 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