etc/symbols
changeset 71887 f7d15620dd8e
parent 71881 71de0a253842
child 71902 1529336eaedc
--- a/etc/symbols	Sun May 24 19:57:13 2020 +0000
+++ b/etc/symbols	Mon May 25 19:10:38 2020 +0200
@@ -419,6 +419,9 @@
 \<^prop>                argument: cartouche
 \<^scala>               argument: cartouche
 \<^scala_function>      argument: cartouche
+\<^scala_method>        argument: cartouche
+\<^scala_object>        argument: cartouche
+\<^scala_type>          argument: cartouche
 \<^session>             argument: cartouche
 \<^simproc>             argument: cartouche
 \<^sort>                argument: cartouche