equal
deleted
inserted
replaced
200 val protocolN: string |
200 val protocolN: string |
201 val reportN: string val report: T |
201 val reportN: string val report: T |
202 val no_reportN: string val no_report: T |
202 val no_reportN: string val no_report: T |
203 val badN: string val bad: unit -> T |
203 val badN: string val bad: unit -> T |
204 val intensifyN: string val intensify: T |
204 val intensifyN: string val intensify: T |
|
205 val countN: string |
|
206 val ML_profiling_entryN: string |
|
207 val ML_profiling_entry: {name: string, count: int} -> T |
|
208 val ML_profilingN: string |
|
209 val ML_profiling: string -> T |
205 val browserN: string |
210 val browserN: string |
206 val graphviewN: string |
211 val graphviewN: string |
207 val theory_exportsN: string |
212 val theory_exportsN: string |
208 val sendbackN: string |
213 val sendbackN: string |
209 val paddingN: string |
214 val paddingN: string |
655 fun bad () = (badN, serial_properties (serial ())); |
660 fun bad () = (badN, serial_properties (serial ())); |
656 |
661 |
657 val (intensifyN, intensify) = markup_elem "intensify"; |
662 val (intensifyN, intensify) = markup_elem "intensify"; |
658 |
663 |
659 |
664 |
|
665 (* ML profiling *) |
|
666 |
|
667 val countN = "count"; |
|
668 |
|
669 val ML_profiling_entryN = "ML_profiling_entry"; |
|
670 fun ML_profiling_entry {name, count} = |
|
671 (ML_profiling_entryN, [(nameN, name), (countN, Value.print_int count)]); |
|
672 |
|
673 val (ML_profilingN, ML_profiling) = markup_string "ML_profiling" kindN; |
|
674 |
|
675 |
660 (* active areas *) |
676 (* active areas *) |
661 |
677 |
662 val browserN = "browser" |
678 val browserN = "browser" |
663 val graphviewN = "graphview"; |
679 val graphviewN = "graphview"; |
664 val theory_exportsN = "theory_exports"; |
680 val theory_exportsN = "theory_exports"; |