changeset 26884 | 67c54c53da28 |
parent 26504 | 6e87c0a60104 |
child 27004 | 616c553c7cf1 |
26883:ae6ae88f9240 | 26884:67c54c53da28 |
---|---|
117 fun install_pp (path, pp) = (); |
117 fun install_pp (path, pp) = (); |
118 |
118 |
119 |
119 |
120 (* ML command execution *) |
120 (* ML command execution *) |
121 |
121 |
122 fun use_text _ _ _ _ txt = (Compiler.eval txt; ()); |
122 fun use_text _ _ _ _ _ txt = (Compiler.eval txt; ()); |
123 fun use_file _ _ _ name = use name; |
123 fun use_file _ _ _ _ name = use name; |
124 |
124 |
125 |
125 |
126 |
126 |
127 (** interrupts **) |
127 (** interrupts **) |
128 |
128 |