equal
deleted
inserted
replaced
136 List(node) |
136 List(node) |
137 case _ => Nil |
137 case _ => Nil |
138 } |
138 } |
139 |
139 |
140 val text = Isabelle.buffer_text(model.buffer) |
140 val text = Isabelle.buffer_text(model.buffer) |
141 val structure = Structure.parse_sections(syntax, "theory " + model.thy_name, text) |
141 val structure = Structure.parse(syntax, "theory " + model.thy_name, text) |
142 |
142 |
143 make_tree(0, structure) foreach (node => data.root.add(node)) |
143 make_tree(0, structure) foreach (node => data.root.add(node)) |
144 } |
144 } |
145 } |
145 } |
146 |
146 |