support for context block structure in Sidekick;
authorwenzelm
Thu Aug 04 20:55:36 2016 +0200 (2016-08-04)
changeset 63606fc3a23763617
parent 63605 c7916060f55e
child 63607 7246254d558f
support for context block structure in Sidekick;
tuned;
src/Pure/Isar/document_structure.scala
src/Pure/PIDE/command_span.scala
src/Tools/jEdit/src/isabelle_sidekick.scala
src/Tools/jEdit/src/services.xml
     1.1 --- a/src/Pure/Isar/document_structure.scala	Thu Aug 04 11:32:21 2016 +0200
     1.2 +++ b/src/Pure/Isar/document_structure.scala	Thu Aug 04 20:55:36 2016 +0200
     1.3 @@ -22,9 +22,13 @@
     1.4    { def length: Int = command.length }
     1.5  
     1.6  
     1.7 -  /* section headings etc. */
     1.8 +  private def is_theory_command(keywords: Keyword.Keywords, name: String): Boolean =
     1.9 +    keywords.kinds.get(name) match {
    1.10 +      case Some(kind) => Keyword.theory(kind) && !Keyword.theory_end(kind)
    1.11 +      case None => false
    1.12 +    }
    1.13  
    1.14 -  def heading_level(keywords: Keyword.Keywords, command: Command): Option[Int] =
    1.15 +  private def heading_level(keywords: Keyword.Keywords, command: Command): Option[Int] =
    1.16    {
    1.17      val name = command.span.name
    1.18      name match {
    1.19 @@ -34,14 +38,61 @@
    1.20        case Thy_Header.SUBSUBSECTION => Some(3)
    1.21        case Thy_Header.PARAGRAPH => Some(4)
    1.22        case Thy_Header.SUBPARAGRAPH => Some(5)
    1.23 -      case _ =>
    1.24 -        keywords.kinds.get(name) match {
    1.25 -          case Some(kind) if Keyword.theory(kind) && !Keyword.theory_end(kind) => Some(6)
    1.26 -          case _ => None
    1.27 -        }
    1.28 +      case _ if is_theory_command(keywords, name) => Some(6)
    1.29 +      case _ => None
    1.30      }
    1.31    }
    1.32  
    1.33 +
    1.34 +  /* context blocks */
    1.35 +
    1.36 +  def parse_blocks(
    1.37 +    syntax: Outer_Syntax,
    1.38 +    node_name: Document.Node.Name,
    1.39 +    text: CharSequence): List[Document] =
    1.40 +  {
    1.41 +    /* stack operations */
    1.42 +
    1.43 +    def buffer(): mutable.ListBuffer[Document] = new mutable.ListBuffer[Document]
    1.44 +
    1.45 +    var stack: List[(Command, mutable.ListBuffer[Document])] =
    1.46 +      List((Command.empty, buffer()))
    1.47 +
    1.48 +    def close(): Boolean =
    1.49 +      stack match {
    1.50 +        case (command, body) :: (_, body2) :: _ =>
    1.51 +          body2 += Block(command.span.name, command.source, body.toList)
    1.52 +          stack = stack.tail
    1.53 +          true
    1.54 +        case _ =>
    1.55 +          false
    1.56 +      }
    1.57 +
    1.58 +    def result(): List[Document] =
    1.59 +    {
    1.60 +      while (close()) { }
    1.61 +      stack.head._2.toList
    1.62 +    }
    1.63 +
    1.64 +    def add(command: Command)
    1.65 +    {
    1.66 +      if (command.span.is_begin) stack = (command, buffer()) :: stack
    1.67 +      else if (command.span.is_end) close()
    1.68 +
    1.69 +      stack.head._2 += Atom(command)
    1.70 +    }
    1.71 +
    1.72 +
    1.73 +    /* result structure */
    1.74 +
    1.75 +    val spans = syntax.parse_spans(text)
    1.76 +    spans.foreach(span => add(Command(Document_ID.none, node_name, Command.no_blobs, span)))
    1.77 +    result()
    1.78 +  }
    1.79 +
    1.80 +
    1.81 +  /* section headings etc. */
    1.82 +
    1.83    def parse_sections(
    1.84      syntax: Outer_Syntax,
    1.85      node_name: Document.Node.Name,
    1.86 @@ -49,8 +100,7 @@
    1.87    {
    1.88      /* stack operations */
    1.89  
    1.90 -    def buffer(): mutable.ListBuffer[Document] =
    1.91 -      new mutable.ListBuffer[Document]
    1.92 +    def buffer(): mutable.ListBuffer[Document] = new mutable.ListBuffer[Document]
    1.93  
    1.94      var stack: List[(Int, Command, mutable.ListBuffer[Document])] =
    1.95        List((0, Command.empty, buffer()))
    1.96 @@ -58,7 +108,7 @@
    1.97      @tailrec def close(level: Int => Boolean)
    1.98      {
    1.99        stack match {
   1.100 -        case (lev, command, body) :: (_, _, body2) :: rest if level(lev) =>
   1.101 +        case (lev, command, body) :: (_, _, body2) :: _ if level(lev) =>
   1.102            body2 += Block(command.span.name, command.source, body.toList)
   1.103            stack = stack.tail
   1.104            close(level)
     2.1 --- a/src/Pure/PIDE/command_span.scala	Thu Aug 04 11:32:21 2016 +0200
     2.2 +++ b/src/Pure/PIDE/command_span.scala	Thu Aug 04 20:55:36 2016 +0200
     2.3 @@ -32,6 +32,9 @@
     2.4      def position: Position.T =
     2.5        kind match { case Command_Span(_, pos) => pos case _ => Position.none }
     2.6  
     2.7 +    def is_begin: Boolean = content.exists(_.is_begin)
     2.8 +    def is_end: Boolean = content.exists(_.is_end)
     2.9 +
    2.10      def length: Int = (0 /: content)(_ + _.source.length)
    2.11  
    2.12      def compact_source: (String, Span) =
     3.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Aug 04 11:32:21 2016 +0200
     3.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Thu Aug 04 20:55:36 2016 +0200
     3.3 @@ -110,7 +110,8 @@
     3.4  
     3.5  class Isabelle_Sidekick_Structure(
     3.6      name: String,
     3.7 -    node_name: Buffer => Option[Document.Node.Name])
     3.8 +    node_name: Buffer => Option[Document.Node.Name],
     3.9 +    parse: (Outer_Syntax, Document.Node.Name, CharSequence) => List[Document_Structure.Document])
    3.10    extends Isabelle_Sidekick(name)
    3.11  {
    3.12    override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
    3.13 @@ -137,25 +138,33 @@
    3.14  
    3.15      node_name(buffer) match {
    3.16        case Some(name) =>
    3.17 -        make_tree(data.root, 0,
    3.18 -          Document_Structure.parse_sections(syntax, name, JEdit_Lib.buffer_text(buffer)))
    3.19 +        make_tree(data.root, 0, parse(syntax, name, JEdit_Lib.buffer_text(buffer)))
    3.20          true
    3.21 -      case None => false
    3.22 +      case None =>
    3.23 +        false
    3.24      }
    3.25    }
    3.26  }
    3.27  
    3.28  
    3.29  class Isabelle_Sidekick_Default extends
    3.30 -  Isabelle_Sidekick_Structure("isabelle", PIDE.resources.theory_node_name)
    3.31 +  Isabelle_Sidekick_Structure("isabelle",
    3.32 +    PIDE.resources.theory_node_name, Document_Structure.parse_sections _)
    3.33 +
    3.34 +
    3.35 +class Isabelle_Sidekick_Context extends
    3.36 +  Isabelle_Sidekick_Structure("isabelle-context",
    3.37 +    PIDE.resources.theory_node_name, Document_Structure.parse_blocks _)
    3.38  
    3.39  
    3.40  class Isabelle_Sidekick_Options extends
    3.41 -  Isabelle_Sidekick_Structure("isabelle-options", _ => Some(Document.Node.Name("options")))
    3.42 +  Isabelle_Sidekick_Structure("isabelle-options",
    3.43 +    _ => Some(Document.Node.Name("options")), Document_Structure.parse_sections _)
    3.44  
    3.45  
    3.46  class Isabelle_Sidekick_Root extends
    3.47 -  Isabelle_Sidekick_Structure("isabelle-root", _ => Some(Document.Node.Name("ROOT")))
    3.48 +  Isabelle_Sidekick_Structure("isabelle-root",
    3.49 +    _ => Some(Document.Node.Name("ROOT")), Document_Structure.parse_sections _)
    3.50  
    3.51  
    3.52  class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup")
     4.1 --- a/src/Tools/jEdit/src/services.xml	Thu Aug 04 11:32:21 2016 +0200
     4.2 +++ b/src/Tools/jEdit/src/services.xml	Thu Aug 04 20:55:36 2016 +0200
     4.3 @@ -17,6 +17,9 @@
     4.4    <SERVICE NAME="isabelle" CLASS="sidekick.SideKickParser">
     4.5      new isabelle.jedit.Isabelle_Sidekick_Default();
     4.6    </SERVICE>
     4.7 +  <SERVICE NAME="isabelle-context" CLASS="sidekick.SideKickParser">
     4.8 +    new isabelle.jedit.Isabelle_Sidekick_Context();
     4.9 +  </SERVICE>
    4.10    <SERVICE NAME="isabelle-markup" CLASS="sidekick.SideKickParser">
    4.11      new isabelle.jedit.Isabelle_Sidekick_Markup();
    4.12    </SERVICE>