changeset 76933 | dd53bb198eb1 |
parent 76932 | f88c239d1a83 |
child 77004 | 8ecf99ac5359 |
--- a/src/Pure/PIDE/document.scala Fri Jan 06 15:35:48 2023 +0100 +++ b/src/Pure/PIDE/document.scala Fri Jan 06 16:43:51 2023 +0100 @@ -580,15 +580,6 @@ node_name :: node.load_commands.flatMap(_.blobs_names) - /* source text */ - - def source: String = - snippet_command match { - case Some(command) => command.source - case None => node.source - } - - /* pending edits */ def is_outdated: Boolean = !pending_edits.is_stable