--- a/src/Pure/Thy/thy_syntax.scala Sun Nov 28 19:30:52 2010 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Sun Nov 28 19:35:14 2010 +0100
@@ -27,7 +27,7 @@
def length: Int = command.length
}
- def parse_sections(syntax: Outer_Syntax, root_name: String, text: CharSequence): Entry =
+ def parse(syntax: Outer_Syntax, root_name: String, text: CharSequence): Entry =
{
/* stack operations */
--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Sun Nov 28 19:30:52 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Sun Nov 28 19:35:14 2010 +0100
@@ -138,7 +138,7 @@
}
val text = Isabelle.buffer_text(model.buffer)
- val structure = Structure.parse_sections(syntax, "theory " + model.thy_name, text)
+ val structure = Structure.parse(syntax, "theory " + model.thy_name, text)
make_tree(0, structure) foreach (node => data.root.add(node))
}