src/Pure/PIDE/document.scala
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