93 class Isabelle_Sidekick_Structure( |
93 class Isabelle_Sidekick_Structure( |
94 name: String, |
94 name: String, |
95 node_name: Buffer => Option[Document.Node.Name]) |
95 node_name: Buffer => Option[Document.Node.Name]) |
96 extends Isabelle_Sidekick(name) |
96 extends Isabelle_Sidekick(name) |
97 { |
97 { |
98 import Thy_Syntax.Structure |
|
99 |
|
100 override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = |
98 override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = |
101 { |
99 { |
102 def make_tree(offset: Text.Offset, entry: Structure.Entry): List[DefaultMutableTreeNode] = |
100 def make_tree(offset: Text.Offset, entry: Thy_Structure.Entry): List[DefaultMutableTreeNode] = |
103 entry match { |
101 entry match { |
104 case Structure.Block(name, body) => |
102 case Thy_Structure.Block(name, body) => |
105 val node = |
103 val node = |
106 new DefaultMutableTreeNode( |
104 new DefaultMutableTreeNode( |
107 new Isabelle_Sidekick.Asset(Library.first_line(name), offset, offset + entry.length)) |
105 new Isabelle_Sidekick.Asset(Library.first_line(name), offset, offset + entry.length)) |
108 (offset /: body)((i, e) => |
106 (offset /: body)((i, e) => |
109 { |
107 { |
110 make_tree(i, e) foreach (nd => node.add(nd)) |
108 make_tree(i, e) foreach (nd => node.add(nd)) |
111 i + e.length |
109 i + e.length |
112 }) |
110 }) |
113 List(node) |
111 List(node) |
114 case Structure.Atom(command) |
112 case Thy_Structure.Atom(command) |
115 if command.is_command && syntax.heading_level(command).isEmpty => |
113 if command.is_command && syntax.heading_level(command).isEmpty => |
116 val node = |
114 val node = |
117 new DefaultMutableTreeNode( |
115 new DefaultMutableTreeNode( |
118 new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length)) |
116 new Isabelle_Sidekick.Asset(command.name, offset, offset + entry.length)) |
119 List(node) |
117 List(node) |
121 } |
119 } |
122 |
120 |
123 node_name(buffer) match { |
121 node_name(buffer) match { |
124 case Some(name) => |
122 case Some(name) => |
125 val text = JEdit_Lib.buffer_text(buffer) |
123 val text = JEdit_Lib.buffer_text(buffer) |
126 val structure = Structure.parse(syntax, name, text) |
124 val structure = Thy_Structure.parse(syntax, name, text) |
127 make_tree(0, structure) foreach (node => data.root.add(node)) |
125 make_tree(0, structure) foreach (node => data.root.add(node)) |
128 true |
126 true |
129 case None => false |
127 case None => false |
130 } |
128 } |
131 } |
129 } |