tuned signature;
authorwenzelm
Sun, 28 Nov 2010 19:35:14 +0100
changeset 40792 1d71a45590e4
parent 40791 d71fe93e8e0c
child 40793 d21aedaa91e7
tuned signature;
src/Pure/Thy/thy_syntax.scala
src/Tools/jEdit/src/jedit/isabelle_sidekick.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 */
 
--- 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))
   }