default Sidekick parser based on section headings;
authorwenzelm
Wed Nov 10 15:17:25 2010 +0100 (2010-11-10)
changeset 40455e035dad8eca2
parent 40454 2516ea25a54b
child 40456 e91b3c2145b4
default Sidekick parser based on section headings;
src/Pure/Isar/outer_syntax.scala
src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Wed Nov 10 15:00:40 2010 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Wed Nov 10 15:17:25 2010 +0100
     1.3 @@ -38,6 +38,12 @@
     1.4        case None => false
     1.5      }
     1.6  
     1.7 +  def is_heading(name: String): Boolean =
     1.8 +    keywords.get(name) match {
     1.9 +      case Some(kind) => Keyword.heading(kind)
    1.10 +      case None => false
    1.11 +    }
    1.12 +
    1.13    def heading_level(name: String): Option[Int] =
    1.14      name match {
    1.15        // FIXME avoid hard-wired info
     2.1 --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Wed Nov 10 15:00:40 2010 +0100
     2.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Wed Nov 10 15:17:25 2010 +0100
     2.3 @@ -110,20 +110,38 @@
     2.4  
     2.5  class Isabelle_Sidekick_Default extends Isabelle_Sidekick("isabelle")
     2.6  {
     2.7 +  import Thy_Syntax.Structure
     2.8 +
     2.9    def parser(data: SideKickParsedData, model: Document_Model)
    2.10    {
    2.11 -    val root = data.root
    2.12 -    val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
    2.13 -    for {
    2.14 -      (command, command_start) <- snapshot.node.command_range()
    2.15 -      if command.is_command && !stopped
    2.16 -    }
    2.17 -    {
    2.18 -      val node =
    2.19 -        new DefaultMutableTreeNode(
    2.20 -          new Isabelle_Sidekick.Asset(command.name, command_start, command_start + command.length))
    2.21 -      root.add(node)
    2.22 -    }
    2.23 +    val syntax = model.session.current_syntax()
    2.24 +
    2.25 +    def make_tree(offset: Int, entry: Structure.Entry): List[DefaultMutableTreeNode] =
    2.26 +      entry match {
    2.27 +        case Structure.Block(name, body) =>
    2.28 +          val node =
    2.29 +            new DefaultMutableTreeNode(
    2.30 +              new Isabelle_Sidekick.Asset(name, offset, offset + entry.length))
    2.31 +          (offset /: body)((i, e) =>
    2.32 +            {
    2.33 +              make_tree(i, e) foreach (nd => node.add(nd))
    2.34 +              i + e.length
    2.35 +            })
    2.36 +          List(node)
    2.37 +        case Structure.Atom(command)
    2.38 +        if command.is_command && !syntax.is_heading(command.name) =>
    2.39 +          val node =
    2.40 +            new DefaultMutableTreeNode(
    2.41 +              new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length))
    2.42 +          List(node)
    2.43 +        case _ => Nil
    2.44 +      }
    2.45 +
    2.46 +    val buffer = model.buffer
    2.47 +    val text = Isabelle.buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
    2.48 +    val structure = Structure.parse_sections(syntax, "theory " + model.thy_name, text)
    2.49 +
    2.50 +    make_tree(0, structure) foreach (node => data.root.add(node))
    2.51    }
    2.52  }
    2.53