equal
deleted
inserted
replaced
73 Programmers rarely need to care about Output.output or Output.raw at |
73 Programmers rarely need to care about Output.output or Output.raw at |
74 all, with some notable exceptions: Output.output is required when |
74 all, with some notable exceptions: Output.output is required when |
75 bypassing the standard channels (writeln etc.), or in token |
75 bypassing the standard channels (writeln etc.), or in token |
76 translations to produce properly formatted results; Output.raw is |
76 translations to produce properly formatted results; Output.raw is |
77 required when capturing already output material that will eventually |
77 required when capturing already output material that will eventually |
78 be presented to the user a second time. |
78 be presented to the user a second time. For the default print mode, |
|
79 both Output.output and Output.raw have no effect. |
79 |
80 |
80 |
81 |
81 *** HOL *** |
82 *** HOL *** |
82 |
83 |
83 * HOL/record: reimplementation of records. Improved scalability for |
84 * HOL/record: reimplementation of records. Improved scalability for |