1304 |
1304 |
1305 * Pure/Syntax: generic interfaces for parsing (Syntax.parse_term etc.) |
1305 * Pure/Syntax: generic interfaces for parsing (Syntax.parse_term etc.) |
1306 and type checking (Syntax.check_term etc.), with common combinations |
1306 and type checking (Syntax.check_term etc.), with common combinations |
1307 (Syntax.read_term etc.). These supersede former Sign.read_term etc. |
1307 (Syntax.read_term etc.). These supersede former Sign.read_term etc. |
1308 which are considered legacy and await removal. |
1308 which are considered legacy and await removal. |
|
1309 |
|
1310 * Pure/Syntax: generic interfaces for type unchecking |
|
1311 (Syntax.uncheck_terms etc.) and unparsing (Syntax.unparse_term etc.), |
|
1312 with common combinations (Syntax.pretty_term, Syntax.string_of_term |
|
1313 etc.). Former Sign.pretty_term, Sign.string_of_term etc. are still |
|
1314 available for convenience, but refer to the very same operations |
|
1315 (using a mere theory instead of a full context). |
1309 |
1316 |
1310 * Isar: simplified treatment of user-level errors, using exception |
1317 * Isar: simplified treatment of user-level errors, using exception |
1311 ERROR of string uniformly. Function error now merely raises ERROR, |
1318 ERROR of string uniformly. Function error now merely raises ERROR, |
1312 without any side effect on output channels. The Isar toplevel takes |
1319 without any side effect on output channels. The Isar toplevel takes |
1313 care of proper display of ERROR exceptions. ML code may use plain |
1320 care of proper display of ERROR exceptions. ML code may use plain |