# HG changeset patch
# User wenzelm
# Date 1290969314 -3600
# Node ID 1d71a45590e42840b7baefd6c19acdd804c68b49
# Parent  d71fe93e8e0c27c428eeb620944fe2472b904dd2
tuned signature;

diff -r d71fe93e8e0c -r 1d71a45590e4 src/Pure/Thy/thy_syntax.scala
--- 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 */
 
diff -r d71fe93e8e0c -r 1d71a45590e4 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala
--- 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))
   }