| changeset 26385 | ae7564661e76 |
| parent 26227 | 58790194116c |
| child 26474 | 94735cff132c |
| 26384:0aed2ba71388 | 26385:ae7564661e76 |
|---|---|
115 fun install_pp (path, pp) = (); |
115 fun install_pp (path, pp) = (); |
116 |
116 |
117 |
117 |
118 (* ML command execution *) |
118 (* ML command execution *) |
119 |
119 |
120 fun use_text tune name (print, err) verbose txt = (Compiler.eval txt; ()); |
120 fun use_text _ _ _ _ txt = (Compiler.eval txt; ()); |
121 |
121 fun use_file _ _ _ name = use name; |
122 fun use_file tune output verbose name = use name; |
|
123 |
122 |
124 |
123 |
125 |
124 |
126 (** interrupts **) |
125 (** interrupts **) |
127 |
126 |