99 node_name: Buffer => Option[Document.Node.Name]) |
99 node_name: Buffer => Option[Document.Node.Name]) |
100 extends Isabelle_Sidekick(name) |
100 extends Isabelle_Sidekick(name) |
101 { |
101 { |
102 override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = |
102 override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = |
103 { |
103 { |
104 def make_tree(offset: Text.Offset, entry: Thy_Structure.Entry): List[DefaultMutableTreeNode] = |
104 def make_tree(offset: Text.Offset, document: Outer_Syntax.Document) |
105 entry match { |
105 : List[DefaultMutableTreeNode] = |
106 case Thy_Structure.Block(name, body) => |
106 document match { |
|
107 case Outer_Syntax.Document_Block(name, body) => |
107 val node = |
108 val node = |
108 new DefaultMutableTreeNode( |
109 new DefaultMutableTreeNode( |
109 new Isabelle_Sidekick.Asset(Library.first_line(name), offset, offset + entry.length)) |
110 new Isabelle_Sidekick.Asset( |
110 (offset /: body)((i, e) => |
111 Library.first_line(name), offset, offset + document.length)) |
|
112 (offset /: body)((i, doc) => |
111 { |
113 { |
112 make_tree(i, e) foreach (nd => node.add(nd)) |
114 for (nd <- make_tree(i, doc)) node.add(nd) |
113 i + e.length |
115 i + doc.length |
114 }) |
116 }) |
115 List(node) |
117 List(node) |
116 case Thy_Structure.Atom(command) |
118 |
|
119 case Outer_Syntax.Document_Atom(command) |
117 if command.is_proper && syntax.heading_level(command).isEmpty => |
120 if command.is_proper && syntax.heading_level(command).isEmpty => |
118 val node = |
121 val node = |
119 new DefaultMutableTreeNode( |
122 new DefaultMutableTreeNode( |
120 new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length)) |
123 new Isabelle_Sidekick.Asset(command.name, offset, offset + document.length)) |
121 List(node) |
124 List(node) |
122 case _ => Nil |
125 case _ => Nil |
123 } |
126 } |
124 |
127 |
125 node_name(buffer) match { |
128 node_name(buffer) match { |
126 case Some(name) => |
129 case Some(name) => |
127 val text = JEdit_Lib.buffer_text(buffer) |
130 val document = syntax.parse_document(name, JEdit_Lib.buffer_text(buffer)) |
128 val structure = Thy_Structure.parse(syntax, name, text) |
131 for (node <- make_tree(0, document)) data.root.add(node) |
129 make_tree(0, structure) foreach (node => data.root.add(node)) |
|
130 true |
132 true |
131 case None => false |
133 case None => false |
132 } |
134 } |
133 } |
135 } |
134 } |
136 } |