equal
deleted
inserted
replaced
124 val functionN: string |
124 val functionN: string |
125 val assign_execs: Properties.T |
125 val assign_execs: Properties.T |
126 val removed_versions: Properties.T |
126 val removed_versions: Properties.T |
127 val invoke_scala: string -> string -> Properties.T |
127 val invoke_scala: string -> string -> Properties.T |
128 val cancel_scala: string -> Properties.T |
128 val cancel_scala: string -> Properties.T |
|
129 val ML_statistics: Properties.T |
129 val no_output: Output.output * Output.output |
130 val no_output: Output.output * Output.output |
130 val default_output: T -> Output.output * Output.output |
131 val default_output: T -> Output.output * Output.output |
131 val add_mode: string -> (T -> Output.output * Output.output) -> unit |
132 val add_mode: string -> (T -> Output.output * Output.output) -> unit |
132 val output: T -> Output.output * Output.output |
133 val output: T -> Output.output * Output.output |
133 val enclose: T -> Output.output -> Output.output |
134 val enclose: T -> Output.output -> Output.output |
385 val assign_execs = [(functionN, "assign_execs")]; |
386 val assign_execs = [(functionN, "assign_execs")]; |
386 val removed_versions = [(functionN, "removed_versions")]; |
387 val removed_versions = [(functionN, "removed_versions")]; |
387 |
388 |
388 fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)]; |
389 fun invoke_scala name id = [(functionN, "invoke_scala"), (nameN, name), (idN, id)]; |
389 fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)]; |
390 fun cancel_scala id = [(functionN, "cancel_scala"), (idN, id)]; |
|
391 |
|
392 val ML_statistics = [(functionN, "ML_statistics")]; |
390 |
393 |
391 |
394 |
392 |
395 |
393 (** print mode operations **) |
396 (** print mode operations **) |
394 |
397 |