# HG changeset patch # User wenzelm # Date 1413710403 -7200 # Node ID 70a947611792f0678f2eef06562b1ec3a2196905 # Parent ad09a4635e26eb1f3d208371d27bcdf9e0bf6d8d tuned signature and modules; diff -r ad09a4635e26 -r 70a947611792 src/Pure/Isar/outer_syntax.scala --- 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() } } diff -r ad09a4635e26 -r 70a947611792 src/Pure/Thy/thy_structure.scala --- 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() - } -} - diff -r ad09a4635e26 -r 70a947611792 src/Pure/build-jars --- 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 diff -r ad09a4635e26 -r 70a947611792 src/Tools/jEdit/src/isabelle_sidekick.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 }