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