changeset 52509 | 2193d2c7f586 |
parent 52507 | 27925b58d6bd |
child 52524 | bc6e0144726a |
--- a/src/Pure/PIDE/command.scala Wed Jul 03 15:19:36 2013 +0200 +++ b/src/Pure/PIDE/command.scala Wed Jul 03 16:19:57 2013 +0200 @@ -217,7 +217,7 @@ id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED") - /* source text */ + /* source */ def length: Int = source.length val range: Text.Range = Text.Range(0, length)