| changeset 43560 | d1650e3720fd |
| parent 43552 | 156c822f181a |
| child 43564 | 9864182c6bad |
| 43559:c1966f322105 | 43560:d1650e3720fd |
|---|---|
187 |
187 |
188 val ML_SOURCE = "ML_source" |
188 val ML_SOURCE = "ML_source" |
189 val DOC_SOURCE = "doc_source" |
189 val DOC_SOURCE = "doc_source" |
190 |
190 |
191 val ANTIQ = "antiq" |
191 val ANTIQ = "antiq" |
192 val ML_ANTIQ = "ML_antiq" |
192 val ML_ANTIQUOTATION = "ML antiquotation" |
193 val DOC_ANTIQ = "doc_antiq" |
193 val DOC_ANTIQ = "doc_antiq" |
194 |
194 |
195 |
195 |
196 /* ML syntax */ |
196 /* ML syntax */ |
197 |
197 |