equal
deleted
inserted
replaced
192 val invoke_scala: string -> string -> Properties.T |
192 val invoke_scala: string -> string -> Properties.T |
193 val cancel_scala: string -> Properties.T |
193 val cancel_scala: string -> Properties.T |
194 val ML_statistics: Properties.entry |
194 val ML_statistics: Properties.entry |
195 val task_statistics: Properties.entry |
195 val task_statistics: Properties.entry |
196 val command_timing: Properties.entry |
196 val command_timing: Properties.entry |
|
197 val theory_timing: Properties.entry |
197 val loading_theory: string -> Properties.T |
198 val loading_theory: string -> Properties.T |
198 val dest_loading_theory: Properties.T -> string option |
199 val dest_loading_theory: Properties.T -> string option |
199 val build_session_finished: Properties.T |
200 val build_session_finished: Properties.T |
200 val print_operationsN: string |
201 val print_operationsN: string |
201 val print_operations: Properties.T |
202 val print_operations: Properties.T |
617 |
618 |
618 val task_statistics = (functionN, "task_statistics"); |
619 val task_statistics = (functionN, "task_statistics"); |
619 |
620 |
620 val command_timing = (functionN, "command_timing"); |
621 val command_timing = (functionN, "command_timing"); |
621 |
622 |
|
623 val theory_timing = (functionN, "theory_timing"); |
|
624 |
622 fun loading_theory name = [("function", "loading_theory"), ("name", name)]; |
625 fun loading_theory name = [("function", "loading_theory"), ("name", name)]; |
623 |
626 |
624 fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name |
627 fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name |
625 | dest_loading_theory _ = NONE; |
628 | dest_loading_theory _ = NONE; |
626 |
629 |