| changeset 34451 | 3b9d0074ed44 |
| parent 34408 | ad7b6c4813c8 |
| child 34456 | 14367c0715e8 |
--- a/src/Tools/jEdit/src/prover/Document.scala Sun Dec 28 20:31:13 2008 +0100 +++ b/src/Tools/jEdit/src/prover/Document.scala Sun Dec 28 20:35:34 2008 +0100 @@ -33,7 +33,7 @@ } } - def getContent(cmd : Command) = text.content(cmd.properStart, cmd.properStop) + def getContent(cmd : Command) = text.content(cmd.proper_start, cmd.proper_stop) def getNextCommandContaining(pos : Int) : Command = { for( cmd <- commands()) { if (pos < cmd.stop) return cmd }