equal
deleted
inserted
replaced
693 \end{matharray} |
693 \end{matharray} |
694 |
694 |
695 @{rail \<open> |
695 @{rail \<open> |
696 @@{ML_antiquotation make_string} |
696 @@{ML_antiquotation make_string} |
697 ; |
697 ; |
698 @@{ML_antiquotation print} @{syntax name}? |
698 @@{ML_antiquotation print} embedded? |
699 \<close>} |
699 \<close>} |
700 |
700 |
701 \<^descr> \<open>@{make_string}\<close> inlines a function to print arbitrary values similar to |
701 \<^descr> \<open>@{make_string}\<close> inlines a function to print arbitrary values similar to |
702 the ML toplevel. The result is compiler dependent and may fall back on "?" |
702 the ML toplevel. The result is compiler dependent and may fall back on "?" |
703 in certain situations. The value of configuration option @{attribute_ref |
703 in certain situations. The value of configuration option @{attribute_ref |