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