equal
deleted
inserted
replaced
582 |
582 |
583 *** ML *** |
583 *** ML *** |
584 |
584 |
585 * Syntax.pretty_priority (default 0) configures the required priority |
585 * Syntax.pretty_priority (default 0) configures the required priority |
586 of pretty-printed output and thus affects insertion of parentheses. |
586 of pretty-printed output and thus affects insertion of parentheses. |
|
587 |
|
588 * Syntax.default_root (default "any") configures the inner syntax |
|
589 category (nonterminal symbol) for parsing of terms. |
587 |
590 |
588 * Former exception Library.UnequalLengths now coincides with |
591 * Former exception Library.UnequalLengths now coincides with |
589 ListPair.UnequalLengths. |
592 ListPair.UnequalLengths. |
590 |
593 |
591 * Renamed raw "explode" function to "raw_explode" to emphasize its |
594 * Renamed raw "explode" function to "raw_explode" to emphasize its |