src/Pure/PIDE/command.scala
changeset 46712 8650d9a95736
parent 46164 a01c969f2e14
child 46813 bb7280848c99
--- a/src/Pure/PIDE/command.scala	Mon Feb 27 16:56:25 2012 +0100
+++ b/src/Pure/PIDE/command.scala	Mon Feb 27 17:13:25 2012 +0100
@@ -121,7 +121,7 @@
 }
 
 
-class Command private(
+final class Command private(
     val id: Document.Command_ID,
     val node_name: Document.Node.Name,
     val span: List[Token],