# HG changeset patch
# User wenzelm
# Date 1470336936 -7200
# Node ID fc3a23763617a310a0184bf3c16f8372743c2759
# Parent c7916060f55e983edae2109d9ae0dbfe9c137579
support for context block structure in Sidekick;
tuned;
diff -r c7916060f55e -r fc3a23763617 src/Pure/Isar/document_structure.scala
--- a/src/Pure/Isar/document_structure.scala Thu Aug 04 11:32:21 2016 +0200
+++ b/src/Pure/Isar/document_structure.scala Thu Aug 04 20:55:36 2016 +0200
@@ -22,9 +22,13 @@
{ def length: Int = command.length }
- /* section headings etc. */
+ private def is_theory_command(keywords: Keyword.Keywords, name: String): Boolean =
+ keywords.kinds.get(name) match {
+ case Some(kind) => Keyword.theory(kind) && !Keyword.theory_end(kind)
+ case None => false
+ }
- def heading_level(keywords: Keyword.Keywords, command: Command): Option[Int] =
+ private def heading_level(keywords: Keyword.Keywords, command: Command): Option[Int] =
{
val name = command.span.name
name match {
@@ -34,14 +38,61 @@
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
- }
+ case _ if is_theory_command(keywords, name) => Some(6)
+ case _ => None
}
}
+
+ /* context blocks */
+
+ def parse_blocks(
+ 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[(Command, mutable.ListBuffer[Document])] =
+ List((Command.empty, buffer()))
+
+ def close(): Boolean =
+ stack match {
+ case (command, body) :: (_, body2) :: _ =>
+ body2 += Block(command.span.name, command.source, body.toList)
+ stack = stack.tail
+ true
+ case _ =>
+ false
+ }
+
+ def result(): List[Document] =
+ {
+ while (close()) { }
+ stack.head._2.toList
+ }
+
+ def add(command: Command)
+ {
+ if (command.span.is_begin) stack = (command, buffer()) :: stack
+ else if (command.span.is_end) close()
+
+ stack.head._2 += 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()
+ }
+
+
+ /* section headings etc. */
+
def parse_sections(
syntax: Outer_Syntax,
node_name: Document.Node.Name,
@@ -49,8 +100,7 @@
{
/* stack operations */
- def buffer(): mutable.ListBuffer[Document] =
- new mutable.ListBuffer[Document]
+ def buffer(): mutable.ListBuffer[Document] = new mutable.ListBuffer[Document]
var stack: List[(Int, Command, mutable.ListBuffer[Document])] =
List((0, Command.empty, buffer()))
@@ -58,7 +108,7 @@
@tailrec def close(level: Int => Boolean)
{
stack match {
- case (lev, command, body) :: (_, _, body2) :: rest if level(lev) =>
+ case (lev, command, body) :: (_, _, body2) :: _ if level(lev) =>
body2 += Block(command.span.name, command.source, body.toList)
stack = stack.tail
close(level)
diff -r c7916060f55e -r fc3a23763617 src/Pure/PIDE/command_span.scala
--- a/src/Pure/PIDE/command_span.scala Thu Aug 04 11:32:21 2016 +0200
+++ b/src/Pure/PIDE/command_span.scala Thu Aug 04 20:55:36 2016 +0200
@@ -32,6 +32,9 @@
def position: Position.T =
kind match { case Command_Span(_, pos) => pos case _ => Position.none }
+ def is_begin: Boolean = content.exists(_.is_begin)
+ def is_end: Boolean = content.exists(_.is_end)
+
def length: Int = (0 /: content)(_ + _.source.length)
def compact_source: (String, Span) =
diff -r c7916060f55e -r fc3a23763617 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Aug 04 11:32:21 2016 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Thu Aug 04 20:55:36 2016 +0200
@@ -110,7 +110,8 @@
class Isabelle_Sidekick_Structure(
name: String,
- node_name: Buffer => Option[Document.Node.Name])
+ node_name: Buffer => Option[Document.Node.Name],
+ parse: (Outer_Syntax, Document.Node.Name, CharSequence) => List[Document_Structure.Document])
extends Isabelle_Sidekick(name)
{
override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
@@ -137,25 +138,33 @@
node_name(buffer) match {
case Some(name) =>
- make_tree(data.root, 0,
- Document_Structure.parse_sections(syntax, name, JEdit_Lib.buffer_text(buffer)))
+ make_tree(data.root, 0, parse(syntax, name, JEdit_Lib.buffer_text(buffer)))
true
- case None => false
+ case None =>
+ false
}
}
}
class Isabelle_Sidekick_Default extends
- Isabelle_Sidekick_Structure("isabelle", PIDE.resources.theory_node_name)
+ Isabelle_Sidekick_Structure("isabelle",
+ PIDE.resources.theory_node_name, Document_Structure.parse_sections _)
+
+
+class Isabelle_Sidekick_Context extends
+ Isabelle_Sidekick_Structure("isabelle-context",
+ PIDE.resources.theory_node_name, Document_Structure.parse_blocks _)
class Isabelle_Sidekick_Options extends
- Isabelle_Sidekick_Structure("isabelle-options", _ => Some(Document.Node.Name("options")))
+ Isabelle_Sidekick_Structure("isabelle-options",
+ _ => Some(Document.Node.Name("options")), Document_Structure.parse_sections _)
class Isabelle_Sidekick_Root extends
- Isabelle_Sidekick_Structure("isabelle-root", _ => Some(Document.Node.Name("ROOT")))
+ Isabelle_Sidekick_Structure("isabelle-root",
+ _ => Some(Document.Node.Name("ROOT")), Document_Structure.parse_sections _)
class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup")
diff -r c7916060f55e -r fc3a23763617 src/Tools/jEdit/src/services.xml
--- a/src/Tools/jEdit/src/services.xml Thu Aug 04 11:32:21 2016 +0200
+++ b/src/Tools/jEdit/src/services.xml Thu Aug 04 20:55:36 2016 +0200
@@ -17,6 +17,9 @@
new isabelle.jedit.Isabelle_Sidekick_Default();
+
+ new isabelle.jedit.Isabelle_Sidekick_Context();
+
new isabelle.jedit.Isabelle_Sidekick_Markup();