equal
deleted
inserted
replaced
90 val keyword1N: string val keyword1: T |
90 val keyword1N: string val keyword1: T |
91 val keyword2N: string val keyword2: T |
91 val keyword2N: string val keyword2: T |
92 val elapsedN: string |
92 val elapsedN: string |
93 val cpuN: string |
93 val cpuN: string |
94 val gcN: string |
94 val gcN: string |
|
95 val timing_properties: Timing.timing -> Properties.T |
95 val timingN: string val timing: Timing.timing -> T |
96 val timingN: string val timing: Timing.timing -> T |
96 val subgoalsN: string |
97 val subgoalsN: string |
97 val proof_stateN: string val proof_state: int -> T |
98 val proof_stateN: string val proof_state: int -> T |
98 val stateN: string val state: T |
99 val stateN: string val state: T |
99 val goalN: string val goal: T |
100 val goalN: string val goal: T |
321 val (keyword2N, keyword2) = markup_elem "keyword2"; |
322 val (keyword2N, keyword2) = markup_elem "keyword2"; |
322 |
323 |
323 |
324 |
324 (* timing *) |
325 (* timing *) |
325 |
326 |
326 val timingN = "timing"; |
|
327 val elapsedN = "elapsed"; |
327 val elapsedN = "elapsed"; |
328 val cpuN = "cpu"; |
328 val cpuN = "cpu"; |
329 val gcN = "gc"; |
329 val gcN = "gc"; |
330 |
330 |
331 fun timing {elapsed, cpu, gc} = |
331 fun timing_properties {elapsed, cpu, gc} = |
332 (timingN, |
332 [(elapsedN, Time.toString elapsed), |
333 [(elapsedN, Time.toString elapsed), |
333 (cpuN, Time.toString cpu), |
334 (cpuN, Time.toString cpu), |
334 (gcN, Time.toString gc)]; |
335 (gcN, Time.toString gc)]); |
335 |
|
336 val timingN = "timing"; |
|
337 fun timing t = (timingN, timing_properties t); |
336 |
338 |
337 |
339 |
338 (* toplevel *) |
340 (* toplevel *) |
339 |
341 |
340 val subgoalsN = "subgoals"; |
342 val subgoalsN = "subgoals"; |