diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-08-18 15:21:09 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-08-18 15:21:09 +0000 |
| commit | 7d79479762513583e63f1d07762c81b12245e7c0 (patch) | |
| tree | 4611294838bf9ded15ad257973b2dca4ef798c27 /etc | |
| parent | 49c8e1185e263430157013149a4af6ed0eb494b0 (diff) | |
Updated with recent figures from Mac OS X.
Diffstat (limited to 'etc')
| -rw-r--r-- | etc/isar/profiling.txt | 894 |
1 files changed, 301 insertions, 593 deletions
diff --git a/etc/isar/profiling.txt b/etc/isar/profiling.txt index c9c0b883..27c9c8ff 100644 --- a/etc/isar/profiling.txt +++ b/etc/isar/profiling.txt @@ -1,614 +1,322 @@ -Profiling of hundred theorems: +Wed Aug 18 2010. See Trac #324. -proof-shell-filter 206 0.5755520000 0.0027939417 -proof-shell-filter-manage-output 206 0.4828650000 0.0023440048 -proof-shell-exec-loop 206 0.479615 0.0023282281 -proof-done-advancing 204 0.3241909999 0.0015891715 -proof-done-advancing-save 100 0.2885119999 0.0028851199 -proof-make-goalsave 100 0.2780209999 0.0027802099 -pg-add-proof-element 100 0.2667299999 0.0026672999 -proof-next-element-id 100 0.2568640000 0.0025686400 -proof-element-id 100 0.2559739999 0.0025597399 -proof-shell-insert 206 0.1490790000 0.0007236844 -scomint-send-input 206 0.0973649999 0.0004726456 -scomint-send-string 206 0.0899980000 0.0004368834 -pg-remove-specials 206 0.0822929999 0.0003994805 -isar-preprocessing 206 0.0361179999 0.0001753300 -proof-toolbar-next-enable-p 638 0.0286260000 4.486...e-05 -isar-command-wrapping 206 0.0269059999 0.0001306116 -proof-locked-region-full-p 639 0.0268030000 4.194...e-05 -pg-set-span-helphighlights 304 0.0225119999 7.405...e-05 -isar-positions-of 206 0.0202500000 9.830...e-05 -proof-toolbar-use-enable-p 319 0.0138090000 4.328...e-05 -proof-set-overlay-arrow 204 0.0115210000 5.647...e-05 -proof-string-match 1526 0.0104410000 6.842...e-06 -proof-shell-available-p 2233 0.0092940000 4.162...e-06 -proof-done-advancing-other 104 0.007964 7.657...e-05 -pg-last-output-displayform 304 0.0075990000 2.499...e-05 -isar-string-wrapping 412 0.0063830000 1.549...e-05 -proof-shell-strip-output-markup 304 0.0059760000 1.965...e-05 -isar-strip-output-markup 305 0.0048359999 1.585...e-05 -proof-replace-regexp-in-string 412 0.0047720000 1.158...e-05 -isar-shell-adjust-line-width 206 0.00416 2.019...e-05 -isar-global-save-command-p 100 0.0038479999 3.847...e-05 -proof-shell-process-urgent-messages 206 0.003735 1.813...e-05 -proof-string-match-safe 204 0.0032319999 1.584...e-05 -proof-toolbar-state-enable-p 319 0.0031699999 9.937...e-06 -pg-processing-complete-hint 1 0.002853 0.002853 -scomint-check-proc 2441 0.0028120000 1.151...e-06 -proof-get-name-from-goal 100 0.0026769999 2.676...e-05 -proof-toolbar-retract-enable-p 319 0.0025379999 7.956...e-06 -proof-toolbar-undo-enable-p 319 0.0024359999 7.636...e-06 -proof-toolbar-delete-enable-p 319 0.0023529999 7.376...e-06 -isar-goal-command-p 204 0.0021389999 1.048...e-05 -proof-toolbar-find-enable-p 319 0.0020489999 6.423...e-06 -proof-toolbar-context-enable-p 319 0.0018939999 5.937...e-06 -proof-toolbar-info-enable-p 319 0.0018169999 5.695...e-06 -proof-toolbar-command-enable-p 319 0.0017689999 5.545...e-06 -pg-add-element 100 0.0016860000 1.686...e-05 -proof-shell-classify-output 206 0.0016479999 7.999...e-06 -proof-locked-region-empty-p 320 0.0014510000 4.534...e-06 -pg-span-name 304 0.0012320000 4.052...e-06 -proof-process-buffer 1 0.001196 0.001196 -pg-add-to-input-history 104 0.0011950000 1.149...e-05 -proof-assert-until-point-interactive 1 0.001159 0.001159 -proof-assert-until-point 1 0.001155 0.001155 -proof-unprocessed-begin 1126 0.0010770000 9.564...e-07 -proof-shell-live-buffer 206 0.0010610000 5.150...e-06 -proof-assert-semis 1 0.001013 0.001013 -proof-splice-separator 206 0.0007109999 3.451...e-06 -proof-extend-queue 1 0.000638 0.000638 -proof-append-alist 1 0.00063 0.00063 -proof-semis-to-vanillas 1 0.000347 0.000347 -proof-next-element-count 100 0.0002829999 2.829...e-06 -proof-shell-process-urgent-message 1 0.00025 0.00025 -proof-toolbar-goto-enable-p 319 0.0002259999 7.084...e-07 -proof-toolbar-interrupt-enable-p 319 0.0001709999 5.360...e-07 -proof-debug 100 0.0001189999 1.189...e-06 -proof-segment-up-to-using-cache 1 9.6e-05 9.6e-05 -proof-segment-cache-contents-for 1 8.4e-05 8.4e-05 -pg-response-display-with-face 2 7.5e-05 3.75e-05 -proof-shell-message 1 7e-05 7e-05 -pg-response-maybe-erase 2 5e-05 2.5e-05 -pg-hint 1 3.9e-05 3.9e-05 -proof-re-search-backward 1 3e-05 3e-05 -proof-shell-ready-prover 2 2.100...e-05 1.050...e-05 -proof-shell-handle-delayed-output 1 2.1e-05 2.1e-05 -proof-activate-scripting 1 1.7e-05 1.7e-05 -proof-maybe-follow-locked-end 1 1.6e-05 1.6e-05 -proof-shell-start 2 1.5e-05 7.5e-06 -pg-response-display 1 1.4e-05 1.4e-05 -proof-grab-lock 1 1.2e-05 1.2e-05 -proof-script-next-command-advance 1 7e-06 7e-06 -proof-shell-strip-eager-annotations 1 7e-06 7e-06 -proof-shell-start-silent-item 1 6e-06 6e-06 -proof-shell-action-list-item 2 4e-06 2e-06 -proof-shell-stop-silent-item 1 4e-06 4e-06 -proof-queue-or-locked-end 4 3e-06 7.5e-07 -proof-shell-should-be-silent 1 2e-06 2e-06 -proof-shell-set-silent 1 1e-06 1e-06 -proof-shell-clear-silent 1 1e-06 1e-06 -proof-pbp-focus-on-first-goal 1 1e-06 1e-06 -proof-display-and-keep-buffer 1 1e-06 1e-06 -proof-release-lock 1 1e-06 1e-06 -pg-finish-tracing-display 1 1e-06 1e-06 - - -Profiling AThousandTheorems (inc parse) - -proof-shell-filter 2009 4.2185289999 0.0020998153 -proof-shell-filter-manage-output 2008 3.7156680000 0.0018504322 -proof-process-buffer 1 3.681492 3.681492 -proof-assert-until-point-interactive 1 3.681391 3.681391 -proof-assert-until-point 1 3.681388 3.681388 -proof-shell-exec-loop 2008 3.6569860000 0.0018212081 -proof-assert-semis 1 2.165613 2.165613 -proof-activate-scripting 1 2.1626339999 2.1626339999 -proof-shell-wait 3 2.157879 0.719293 -proof-shell-insert 2008 1.8324589999 0.0009125791 -proof-done-advancing 2004 1.7108090000 0.0008536971 -proof-segment-up-to-using-cache 1 1.515725 1.515725 -proof-segment-up-to 1 1.5153910000 1.5153910000 -proof-segment-up-to-cmdstart 1 1.515388 1.515388 -proof-looking-at-syntactic-context 2012 1.2962439999 0.0006442564 -isar-syntactic-context 2012 1.2880049999 0.0006401615 -proof-looking-at-syntactic-context-default 2012 1.283686 0.0006380149 -proof-buffer-syntactic-context 2013 1.2504469999 0.0006211857 -proof-register-possibly-new-processed-file 2 1.147767 0.5738835 -proof-deactivate-scripting 1 1.146929 1.146929 -proof-shell-invisible-command 2 1.144748 0.572374 -proof-cd-sync 1 1.014265 1.014265 -scomint-send-input 2008 1.0111659999 0.0005035687 -proof-toolbar-next-enable-p 7434 0.6904569999 9.287...e-05 -proof-done-advancing-save 1000 0.6694850000 0.0006694850 -proof-locked-region-full-p 7437 0.6680110000 8.982...e-05 -isar-preprocessing 2008 0.5888010000 0.0002932275 -scomint-send-string 2008 0.5238210000 0.0002608670 -isar-command-wrapping 2008 0.4266709999 0.0002124855 -isar-positions-of 2008 0.2837250000 0.0001412973 -proof-make-goalsave 1000 0.2802490000 0.0002802490 -pg-set-span-helphighlights 3004 0.2778229999 9.248...e-05 -pg-remove-specials 2008 0.2700440000 0.0001344840 -proof-toolbar-use-enable-p 3717 0.2482730000 6.679...e-05 -proof-shell-available-p 26019 0.1759880000 6.763...e-06 -proof-re-search-forward 2064 0.1741260000 8.436...e-05 -pg-add-proof-element 1000 0.1635090000 0.0001635090 -proof-string-match 15032 0.1542850000 1.026...e-05 -proof-done-advancing-other 1004 0.1512260000 0.0001506235 -isar-string-wrapping 4015 0.1382279999 3.442...e-05 -proof-get-name-from-goal 1000 0.1235100000 0.0001235100 -proof-replace-regexp-in-string 4015 0.1221689999 3.042...e-05 -isar-global-save-command-p 1000 0.1135740000 0.0001135740 -proof-string-match-safe 2004 0.1066289999 5.320...e-05 -proof-toolbar-command-enable-p 3717 0.0918040000 2.469...e-05 -proof-set-overlay-arrow 2004 0.0877379999 4.378...e-05 -pg-add-to-input-history 1004 0.0811079999 8.078...e-05 -pg-last-output-displayform 3004 0.0799419999 2.661...e-05 -pg-add-element 1000 0.0758799999 7.587...e-05 -proof-shell-process-urgent-messages 2009 0.0691360000 3.441...e-05 -proof-shell-strip-output-markup 3006 0.0621240000 2.066...e-05 -isar-strip-output-markup 3008 0.0508979999 1.692...e-05 -isar-shell-adjust-line-width 2008 0.0436570000 2.174...e-05 -proof-shell-classify-output 2008 0.0423230000 2.107...e-05 -proof-toolbar-state-enable-p 3717 0.0384680000 1.034...e-05 -scomint-check-proc 28033 0.0319450000 1.139...e-06 -proof-toolbar-retract-enable-p 3717 0.0305389999 8.216...e-06 -isar-goal-command-p 2004 0.026745 1.334...e-05 -proof-cmdstart-add-segment-for-cmd 2004 0.0246840000 1.231...e-05 -proof-toolbar-delete-enable-p 3717 0.0242569999 6.525...e-06 -proof-toolbar-undo-enable-p 3717 0.0241040000 6.484...e-06 -proof-toolbar-context-enable-p 3717 0.0233320000 6.277...e-06 -proof-toolbar-find-enable-p 3717 0.0226730000 6.099...e-06 -proof-toolbar-info-enable-p 3717 0.0210330000 5.658...e-06 -proof-locked-region-empty-p 3722 0.0176580000 4.744...e-06 -proof-looking-at-safe 4012 0.0171930000 4.285...e-06 -proof-next-element-id 1000 0.0129890000 1.298...e-05 -pg-span-name 3004 0.0127430000 4.242...e-06 -proof-shell-live-buffer 2008 0.0114760000 5.715...e-06 -proof-unprocessed-begin 11480 0.0112319999 9.783...e-07 -proof-looking-at 4012 0.0082560000 2.057...e-06 -proof-splice-separator 2008 0.0070060000 3.489...e-06 -pg-processing-complete-hint 3 0.0058870000 0.0019623333 -proof-element-id 1000 0.0039640000 3.964...e-06 -proof-next-element-count 1000 0.0028809999 2.880...e-06 -proof-toolbar-goto-enable-p 3717 0.0027980000 7.527...e-07 -proof-semis-to-vanillas 1 0.002604 0.002604 -proof-toolbar-interrupt-enable-p 3717 0.0022529999 6.061...e-07 -proof-shell-process-urgent-message 3 0.001543 0.0005143333 -proof-debug 1003 0.0012860000 1.282...e-06 -proof-append-alist 3 0.000957 0.000319 -isar-match-nesting 51 0.000897 1.758...e-05 -proof-start-queue 2 0.000614 0.000307 -proof-unregister-buffer-file-name 1 0.000609 0.000609 -proof-cd 1 0.000429 0.000429 -proof-extend-queue 1 0.00036 0.00036 -proof-shell-message 2 0.000257 0.0001285 -pg-response-display-with-face 5 0.0001839999 3.679...e-05 -proof-format-filename 2 0.000173 8.65e-05 -pg-response-maybe-erase 5 0.000124 2.48e-05 -proof-shell-handle-delayed-output 3 0.000117 3.9e-05 -pg-response-display 3 9.5e-05 3.166...e-05 -pg-hint 1 7.1e-05 7.1e-05 -proof-format 10 6.1e-05 6.1e-06 -proof-shell-ready-prover 6 5.899...e-05 9.833...e-06 -proof-shell-start 6 3.8e-05 6.333...e-06 -proof-grab-lock 3 3.5e-05 1.166...e-05 -proof-re-search-backward 1 3.3e-05 3.3e-05 -proof-init-segmentation 1 2.4e-05 2.4e-05 -proof-shell-strip-eager-annotations 2 1.5e-05 7.5e-06 -proof-complete-buffer-atomic 1 1.4e-05 1.4e-05 -proof-maybe-follow-locked-end 1 1.1e-05 1.1e-05 -proof-shell-action-list-item 4 1.099...e-05 2.749...e-06 -proof-queue-or-locked-end 4 8e-06 2e-06 -proof-script-end 1 7e-06 7e-06 -proof-shell-stop-silent-item 1 6e-06 6e-06 -proof-shell-should-be-silent 3 6e-06 2e-06 -proof-shell-start-silent-item 1 6e-06 6e-06 -proof-span-read-only 2 4e-06 2e-06 -proof-display-and-keep-buffer 3 4e-06 1.333...e-06 -proof-pbp-focus-on-first-goal 3 3e-06 1e-06 -proof-release-lock 3 3e-06 1e-06 -pg-finish-tracing-display 3 3e-06 1e-06 -proof-done-invisible 2 2e-06 1e-06 -proof-script-next-command-advance 1 2e-06 2e-06 -pg-clear-script-portions 1 2e-06 2e-06 -proof-shell-set-silent 1 1e-06 1e-06 -proof-shell-clear-silent 1 1e-06 1e-06 -pg-clear-input-ring 1 1e-06 1e-06 - - ------------------------------------------------------------------- - -Removing text properties on o/p: - -proof-shell-filter 205 0.3153689999 0.0015383853 -proof-shell-filter-manage-output 205 0.285285 0.0013916341 -proof-shell-exec-loop 205 0.2812860000 0.0013721268 -proof-shell-insert 205 0.2100919999 0.0010248390 -isar-preprocessing 205 0.1048260000 0.0005113463 -isar-command-wrapping 205 0.0952059999 0.0004644195 -scomint-send-input 205 0.0898139999 0.0004381170 -scomint-send-string 205 0.0825070000 0.0004024731 -isar-string-wrapping 410 0.0802999999 0.0001958536 -proof-toolbar-find-enable-p 434 0.0763130000 0.0001758364 -proof-done-advancing 203 0.0650530000 0.0003204581 -proof-done-advancing-save 100 0.0329679999 0.0003296799 -proof-toolbar-next-enable-p 868 0.0198050000 2.281...e-05 -proof-string-match 1521 0.0180250000 1.185...e-05 -proof-make-goalsave 100 0.0177230000 0.0001772300 -proof-locked-region-full-p 868 0.0173869999 2.003...e-05 -pg-remove-specials 205 0.0171139999 8.348...e-05 -pg-set-span-helphighlights 303 0.0167299999 5.521...e-05 -isar-positions-of 205 0.0142010000 6.927...e-05 -proof-shell-available-p 3038 0.0122500000 4.032...e-06 -pg-add-proof-element 100 0.0092029999 9.202...e-05 -proof-toolbar-use-enable-p 434 0.0086329999 1.989...e-05 -pg-last-output-displayform 303 0.0080759999 2.665...e-05 -proof-done-advancing-other 103 0.0071600000 6.951...e-05 -proof-get-name-from-goal 100 0.0066700000 6.670...e-05 -proof-shell-strip-output-markup 303 0.0060650000 2.001...e-05 -proof-shell-process-urgent-messages 205 0.0056970000 2.779...e-05 -proof-replace-regexp-in-string 410 0.0050399999 1.229...e-05 -isar-strip-output-markup 304 0.0049529999 1.629...e-05 -proof-set-overlay-arrow 203 0.0047199999 2.325...e-05 -proof-toolbar-state-enable-p 434 0.0045079999 1.038...e-05 -isar-shell-adjust-line-width 205 0.0044740000 2.182...e-05 -isar-global-save-command-p 100 0.0044660000 4.466...e-05 -proof-string-match-safe 203 0.004411 2.172...e-05 -scomint-check-proc 3245 0.0036840000 1.135...e-06 -proof-toolbar-retract-enable-p 434 0.0035050000 8.076...e-06 -isar-goal-command-p 203 0.0029189999 1.437...e-05 -proof-toolbar-undo-enable-p 434 0.0027759999 6.396...e-06 -proof-toolbar-delete-enable-p 434 0.0027319999 6.294...e-06 -proof-toolbar-context-enable-p 434 0.0025609999 5.900...e-06 -pg-processing-complete-hint 1 0.002415 0.002415 -proof-toolbar-info-enable-p 434 0.0023879999 5.502...e-06 -proof-toolbar-command-enable-p 434 0.0023849999 5.495...e-06 -proof-shell-classify-output 205 0.0023099999 1.126...e-05 -proof-locked-region-empty-p 434 0.0020360000 4.691...e-06 -pg-add-element 100 0.0016829999 1.682...e-05 -pg-span-name 303 0.0012490000 4.122...e-06 -proof-next-element-id 100 0.0012420000 1.242...e-05 -proof-unprocessed-begin 1311 0.0012220000 9.321...e-07 -pg-add-to-input-history 103 0.0011820000 1.147...e-05 -proof-shell-live-buffer 205 0.0011550000 5.634...e-06 -proof-process-buffer 1 0.001021 0.001021 -proof-assert-until-point-interactive 1 0.000982 0.000982 -proof-assert-until-point 1 0.000978 0.000978 -proof-assert-semis 1 0.000821 0.000821 -proof-shell-process-urgent-message 1 0.000807 0.000807 -proof-splice-separator 205 0.0007269999 3.546...e-06 -proof-shell-message 1 0.000621 0.000621 -proof-extend-queue 1 0.000458 0.000458 -proof-append-alist 1 0.000449 0.000449 -proof-element-id 100 0.0003609999 3.609...e-06 -proof-semis-to-vanillas 1 0.000335 0.000335 -proof-toolbar-goto-enable-p 434 0.0003060000 7.050...e-07 -proof-next-element-count 100 0.0002759999 2.759...e-06 -proof-toolbar-interrupt-enable-p 434 0.0002509999 5.783...e-07 -proof-debug 100 0.0001249999 1.249...e-06 -pg-response-display-with-face 2 0.0001089999 5.449...e-05 -proof-segment-up-to-using-cache 1 9.7e-05 9.7e-05 -proof-segment-cache-contents-for 1 8.5e-05 8.5e-05 -proof-re-search-backward 1 4.3e-05 4.3e-05 -proof-shell-handle-delayed-output 1 2.1e-05 2.1e-05 -proof-shell-ready-prover 2 1.999...e-05 9.999...e-06 -proof-activate-scripting 1 1.8e-05 1.8e-05 -pg-response-maybe-erase 2 1.7e-05 8.5e-06 -pg-response-display 1 1.4e-05 1.4e-05 -proof-shell-start 2 1.2e-05 6e-06 -proof-shell-strip-eager-annotations 1 1.2e-05 1.2e-05 -proof-grab-lock 1 1.1e-05 1.1e-05 -proof-maybe-follow-locked-end 1 9e-06 9e-06 -proof-shell-stop-silent-item 1 6e-06 6e-06 -proof-shell-start-silent-item 1 6e-06 6e-06 -proof-shell-action-list-item 2 4.999...e-06 2.499...e-06 -proof-queue-or-locked-end 4 3e-06 7.5e-07 -proof-shell-should-be-silent 1 2e-06 2e-06 -proof-script-next-command-advance 1 2e-06 2e-06 -proof-display-and-keep-buffer 1 2e-06 2e-06 -proof-shell-set-silent 1 1e-06 1e-06 -proof-shell-clear-silent 1 1e-06 1e-06 -proof-release-lock 1 1e-06 1e-06 -pg-finish-tracing-display 1 1e-06 1e-06 -proof-pbp-focus-on-first-goal 1 0.0 0.0 - - ------------------------------------------------------------------- +----------------------------------------------------------------- -Removing text properties on i/p: +Interactive: C-c C-n +### 12.461s elapsed time, 0.514s cpu time, 0.108s GC time -proof-shell-filter 205 0.2767050000 0.0013497804 -proof-shell-filter-manage-output 205 0.2491030000 0.0012151365 -proof-shell-exec-loop 205 0.2451139999 0.0011956780 -proof-shell-insert 205 0.1729689999 0.0008437512 -isar-preprocessing 205 0.1062019999 0.0005180585 -isar-command-wrapping 205 0.0964980000 0.0004707219 -isar-string-wrapping 410 0.0816209999 0.0001990756 -proof-replace-regexp-in-string 410 0.0799649999 0.0001950365 -proof-done-advancing 203 0.0659069999 0.0003246650 -scomint-send-string 205 0.0444790000 0.0002169707 -proof-done-advancing-save 100 0.0334109999 0.0003341099 -proof-toolbar-next-enable-p 844 0.0199650000 2.365...e-05 -proof-string-match 1521 0.0182100000 1.197...e-05 -proof-make-goalsave 100 0.0179040000 0.0001790400 -proof-locked-region-full-p 844 0.0175779999 2.082...e-05 -pg-set-span-helphighlights 303 0.0168959999 5.576...e-05 -pg-remove-specials 205 0.0149570000 7.296...e-05 -isar-positions-of 205 0.0141460000 6.900...e-05 -proof-shell-available-p 2954 0.0121580000 4.115...e-06 -pg-add-proof-element 100 0.0092979999 9.297...e-05 -proof-toolbar-use-enable-p 422 0.0084190000 1.995...e-05 -pg-last-output-displayform 303 0.0081589999 2.692...e-05 -proof-done-advancing-other 103 0.0071879999 6.978...e-05 -proof-get-name-from-goal 100 0.0067640000 6.764...e-05 -proof-shell-strip-output-markup 303 0.0061680000 2.035...e-05 -proof-shell-process-urgent-messages 205 0.0055640000 2.714...e-05 -isar-strip-output-markup 304 0.0050069999 1.647...e-05 -proof-set-overlay-arrow 203 0.0047559999 2.342...e-05 -proof-toolbar-state-enable-p 422 0.0045959999 1.089...e-05 -isar-shell-adjust-line-width 205 0.0045240000 2.206...e-05 -isar-global-save-command-p 100 0.0044959999 4.495...e-05 -proof-string-match-safe 203 0.0044810000 2.207...e-05 -scomint-check-proc 3161 0.0035870000 1.134...e-06 -proof-toolbar-retract-enable-p 422 0.0034850000 8.258...e-06 -isar-goal-command-p 203 0.0029089999 1.433...e-05 -proof-toolbar-context-enable-p 422 0.0028079999 6.654...e-06 -proof-toolbar-delete-enable-p 422 0.0026959999 6.388...e-06 -proof-toolbar-undo-enable-p 422 0.0026899999 6.374...e-06 -proof-toolbar-find-enable-p 422 0.0025549999 6.054...e-06 -pg-processing-complete-hint 1 0.002402 0.002402 -proof-toolbar-info-enable-p 422 0.0023749999 5.627...e-06 -proof-toolbar-command-enable-p 422 0.0023369999 5.537...e-06 -proof-shell-classify-output 205 0.0023229999 1.133...e-05 -proof-locked-region-empty-p 422 0.0020260000 4.800...e-06 -pg-add-element 100 0.0017310000 1.731...e-05 -proof-next-element-id 100 0.001276 1.276e-05 -pg-span-name 303 0.0012510000 4.128...e-06 -proof-unprocessed-begin 1275 0.0012280000 9.631...e-07 -pg-add-to-input-history 103 0.0011990000 1.164...e-05 -proof-shell-live-buffer 205 0.0011910000 5.809...e-06 -proof-process-buffer 1 0.000879 0.000879 -proof-assert-until-point-interactive 1 0.00084 0.00084 -proof-assert-until-point 1 0.000836 0.000836 -proof-shell-process-urgent-message 1 0.000797 0.000797 -proof-splice-separator 205 0.0007339999 3.580...e-06 -proof-assert-semis 1 0.000676 0.000676 -proof-shell-message 1 0.00061 0.00061 -proof-element-id 100 0.0003689999 3.689...e-06 -proof-semis-to-vanillas 1 0.000326 0.000326 -proof-extend-queue 1 0.000322 0.000322 -proof-append-alist 1 0.000315 0.000315 -proof-toolbar-goto-enable-p 422 0.0003090000 7.322...e-07 -proof-next-element-count 100 0.0002779999 2.779...e-06 -proof-toolbar-interrupt-enable-p 422 0.0002469999 5.853...e-07 -proof-debug 100 0.0001319999 1.319...e-06 -pg-response-display-with-face 2 0.000113 5.65e-05 -proof-segment-up-to-using-cache 1 9.3e-05 9.3e-05 -proof-segment-cache-contents-for 1 8.1e-05 8.1e-05 -proof-re-search-backward 1 4.9e-05 4.9e-05 -proof-shell-handle-delayed-output 1 2.1e-05 2.1e-05 -proof-shell-ready-prover 2 1.999...e-05 9.999...e-06 -proof-activate-scripting 1 1.8e-05 1.8e-05 -pg-response-maybe-erase 2 1.7e-05 8.5e-06 -proof-shell-start 2 1.300...e-05 6.500...e-06 -pg-response-display 1 1.3e-05 1.3e-05 -proof-grab-lock 1 1.1e-05 1.1e-05 +scomint-output-filter 206 3.6426039999 0.0176825436 +proof-shell-filter 206 3.629433 0.0176186067 +proof-shell-filter-manage-output 206 3.6140779999 0.0175440679 +proof-shell-exec-loop 206 3.5814560000 0.0173857087 +mapc 208 3.4833689999 0.0167469663 +proof-shell-invoke-callback 206 3.4798549999 0.0168924999 +proof-done-advancing 204 3.4786709999 0.0170523088 +proof-done-advancing-other 104 3.2460199999 0.0312117307 +pg-add-element 204 3.2301699999 0.0158341666 +proof-debug 99 3.2140250000 0.0324648989 +pg-autotest-message 99 3.211558 0.0324399797 +redisplay 99 3.140468 0.0317218989 +proof-done-advancing-save 100 0.107982 0.00107982 +proof-process-buffer 1 0.103025 0.103025 +proof-assert-until-point-interactive 1 0.102849 0.102849 +proof-assert-until-point 1 0.102845 0.102845 +proof-make-goalsave 100 0.0734089999 0.0007340899 +proof-assert-semis 1 0.0729 0.0729 +proof-semis-to-vanillas 1 0.069353 0.069353 +span-at-before 200 0.0607209999 0.0003036049 +proof-shell-insert-action-item 206 0.0561400000 0.0002725242 +proof-shell-insert 206 0.0552149999 0.0002680339 +pg-set-span-helphighlights 304 0.0523910000 0.0001723388 +pg-add-proof-element 100 0.0507439999 0.0005074399 +isar-global-save-command-p 100 0.0403249999 0.0004032499 +isar-command-wrapping 204 0.0389439999 0.0001909019 +isar-positions-of 204 0.0342390000 0.0001678382 +proof-segment-up-to-using-cache 1 0.029667 0.029667 +proof-segment-up-to 1 0.029599 0.029599 +proof-segment-up-to-parser 1 0.02959 0.02959 +proof-script-generic-parse-cmdstart 204 0.0265809999 0.0001302990 +span-live-p 408 0.0245460000 6.016...e-05 +span-property 2226 0.0242540000 1.089...e-05 +proof-set-locked-end 204 0.0179210000 8.784...e-05 +proof-set-locked-endpoints 204 0.0169129999 8.290...e-05 +goto-char 3401 0.0159649999 4.694...e-06 +replace-regexp-in-string 613 0.0154579999 2.521...e-05 +pg-processing-complete-hint 1 0.014814 0.014814 +proof-buffer-syntactic-context 411 0.0145479999 3.539...e-05 +pg-last-output-displayform 304 0.0140980000 4.637...e-05 +proof-buffer-syntactic-context-emulate 411 0.0135870000 3.305...e-05 +span-set-property 4968 0.0131570000 2.648...e-06 +proof-shell-strip-output-markup 202 0.0121529999 6.016...e-05 +isar-strip-output-markup 202 0.0115120000 5.699...e-05 +proof-set-overlay-arrow 204 0.0110750000 5.428...e-05 +pg-hint 1 0.010877 0.010877 +scomint-send-input 206 0.0096710000 4.694...e-05 +skip-chars-forward 917 0.0088720000 9.675...e-06 +string-match 3879 0.0085580000 2.206...e-06 +proof-string-match 1114 0.0083859999 7.527...e-06 +re-search-forward 1084 0.0076900000 7.094...e-06 +proof-shell-process-urgent-messages 206 0.0072959999 3.541...e-05 +proof-shell-handle-immediate-output 206 0.0069180000 3.358...e-05 +span-set-endpoints 409 0.0060590000 1.481...e-05 +isar-preprocessing 206 0.0057689999 2.800...e-05 +isar-string-wrapping 408 0.0057090000 1.399...e-05 +move-overlay 410 0.0048900000 1.192...e-05 +insert 718 0.0043259999 6.025...e-06 +proof-set-queue-start 204 0.0039419999 1.932...e-05 +proof-next-element-id 204 0.0038919999 1.907...e-05 +proof-re-search-forward-safe 824 0.0038370000 4.656...e-06 +proof-script-delete-secondary-spans 1 0.003218 0.003218 +span-delete-spans 1 0.003215 0.003215 +span-mapc-spans 1 0.003214 0.003214 +span-set-start 204 0.003181 1.559...e-05 +pg-add-to-input-history 204 0.0030040000 1.472...e-05 +isar-goal-command-p 204 0.0029059999 1.424...e-05 +span-make 608 0.0029059999 4.779...e-06 +span-end 928 0.0026819999 2.890...e-06 +proof-get-name-from-goal 100 0.0024339999 2.433...e-05 +proof-string-match-safe 204 0.0024330000 1.192...e-05 +overlay-put 4970 0.0023869999 4.802...e-07 +span-delete 304 0.002174 7.151...e-06 +pg-span-name 102 0.00199 1.950...e-05 +proof-element-id 204 0.0019369999 9.495...e-06 +span-start 604 0.0018080000 2.993...e-06 +replace-match 1009 0.0016779999 1.663...e-06 +skip-chars-backward 207 0.0015489999 7.483...e-06 +make-overlay 609 0.0014599999 2.397...e-06 +proof-shell-slurp-comments 207 0.0012420000 6.000...e-06 +delete-overlay 306 0.0011619999 3.797...e-06 +font-lock-fontify-region 2 0.000982 0.000491 +font-lock-default-fontify-region 2 0.0009649999 0.0004824999 +set-marker 1853 0.0009280000 5.008...e-07 +proof-shell-handle-delayed-output 1 0.000917 0.000917 +proof-shell-display-output-as-response 1 0.000892 0.000892 +pg-response-display 1 0.000888 0.000888 +font-lock-fontify-keywords-region 2 0.000882 0.000441 +proof-display-and-keep-buffer 1 0.00087 0.00087 +kill-buffer 4 0.000787 0.00019675 +proof-next-element-count 204 0.0006769999 3.318...e-06 +spans-at-region-prop 1 0.000641 0.000641 +overlay-end 1129 0.0004920000 4.357...e-07 +match-string 308 0.0004569999 1.483...e-06 +marker-position 1237 0.0004520000 3.654...e-07 +buffer-live-p 723 0.0003860000 5.338...e-07 +isar-shell-adjust-line-width 206 0.0003380000 1.640...e-06 +get-buffer-process 212 0.0002819999 1.330...e-06 +proof-extend-queue 1 0.000254 0.000254 +proof-shell-process-urgent-message 1 0.00024 0.00024 +overlay-start 605 0.0002349999 3.884...e-07 +proof-add-to-queue 1 0.000231 0.000231 +proof-only-whitespace-to-locked-region-p 1 0.000192 0.000192 +isar-font-lock-fontify-syntactically-region 2 0.000184 9.2e-05 +nreverse 209 0.0001679999 8.038...e-07 +proof-shell-process-urgent-message-default 1 0.000163 0.000163 +proof-get-window-for-buffer 1 0.000161 0.000161 +proof-re-search-backward 1 0.000157 0.000157 +re-search-backward 1 8.5e-05 8.5e-05 +pg-response-display-with-face 2 7.999...e-05 3.999...e-05 +proof-queue-or-locked-end 6 7.2e-05 1.2e-05 +pg-response-maybe-erase 2 5.9e-05 2.95e-05 +proof-shell-ready-prover 2 5.3e-05 2.65e-05 +proof-looking-at-safe 8 5.1e-05 6.375e-06 +proof-shell-start 2 4.6e-05 2.3e-05 +proof-unprocessed-begin 5 4.3e-05 8.6e-06 +isar-match-nesting 1 4.3e-05 4.3e-05 +proof-activate-scripting 1 4.2e-05 4.2e-05 +proof-shell-live-buffer 2 3.9e-05 1.95e-05 +proof-looking-at 7 3.6e-05 5.142...e-06 +proof-re-search-forward 2 3.500...e-05 1.750...e-05 +proof-detach-queue 1 3.1e-05 3.1e-05 +scomint-check-proc 2 2.9e-05 1.45e-05 +span-detach 1 2.8e-05 2.8e-05 +proof-maybe-follow-locked-end 1 2.7e-05 2.7e-05 +proof-locked-region-full-p 1 2.7e-05 2.7e-05 +proof-grab-lock 1 2.4e-05 2.4e-05 +font-lock-fontify-syntactically-region 1 2.3e-05 2.3e-05 +font-lock-mode 1 2e-05 2e-05 +font-lock-unfontify-region 2 1.7e-05 8.5e-06 +font-lock-extend-jit-lock-region-after-change 3 1.1e-05 3.666...e-06 +proof-locked-region-empty-p 1 1e-05 1e-05 +proof-set-queue-endpoints 1 1e-05 1e-05 proof-shell-strip-eager-annotations 1 1e-05 1e-05 -proof-maybe-follow-locked-end 1 9e-06 9e-06 -proof-shell-start-silent-item 1 6e-06 6e-06 -proof-shell-stop-silent-item 1 5e-06 5e-06 -proof-queue-or-locked-end 4 4e-06 1e-06 -proof-shell-action-list-item 2 4e-06 2e-06 -proof-script-next-command-advance 1 2e-06 2e-06 -proof-display-and-keep-buffer 1 2e-06 2e-06 +font-lock-default-unfontify-region 2 7.000...e-06 3.500...e-06 +proof-associated-windows 1 7e-06 7e-06 +proof-shell-should-be-silent 1 6e-06 6e-06 +font-lock-default-function 1 5e-06 5e-06 +proof-shell-stop-silent-item 1 4e-06 4e-06 +proof-shell-start-silent-item 1 4e-06 4e-06 +proof-script-next-command-advance 1 4e-06 4e-06 +proof-shell-action-list-item 2 3e-06 1.5e-06 +font-lock-set-defaults 2 3e-06 1.5e-06 +proof-associated-buffers 2 2e-06 1e-06 +font-lock-extend-region-wholelines 2 2e-06 1e-06 +font-lock-extend-region-multiline 2 2e-06 1e-06 +proof-minibuffer-message 1 1e-06 1e-06 proof-shell-set-silent 1 1e-06 1e-06 -proof-shell-should-be-silent 1 1e-06 1e-06 proof-shell-clear-silent 1 1e-06 1e-06 proof-pbp-focus-on-first-goal 1 1e-06 1e-06 proof-release-lock 1 1e-06 1e-06 pg-finish-tracing-display 1 1e-06 1e-06 +nconc 1 1e-06 1e-06 +process-status 2 0.0 0.0 ----------------------------------------------------------------- -disabling command wrapping +Non-interactive: (progn (proof-process-buffer) (proof-shell-wait)) -proof-shell-filter 210 0.3514800000 0.0016737142 -proof-shell-filter-manage-output 210 0.2228989999 0.0010614238 -proof-shell-exec-loop 210 0.2188429999 0.0010421095 -proof-done-advancing 204 0.143215 0.0007020343 -pg-remove-specials 210 0.112124 0.0005339238 -proof-done-advancing-save 100 0.109444 0.00109444 -proof-string-match 1334 0.0918810000 6.887...e-05 -proof-shell-available-p 3129 0.0881120000 2.815...e-05 -proof-get-name-from-goal 100 0.0816939999 0.0008169399 -scomint-check-proc 3343 0.0788330000 2.358...e-05 -proof-toolbar-command-enable-p 447 0.0775490000 0.0001734876 -proof-shell-insert 210 0.0685579999 0.0003264666 -scomint-send-string 210 0.0358410000 0.0001706714 -proof-toolbar-next-enable-p 894 0.0220169999 2.462...e-05 -proof-locked-region-full-p 894 0.0195010000 2.181...e-05 -proof-make-goalsave 100 0.0190809999 0.0001908099 -pg-set-span-helphighlights 304 0.0184809999 6.079...e-05 -pg-add-proof-element 100 0.0098279999 9.827...e-05 -proof-toolbar-use-enable-p 447 0.0091759999 2.052...e-05 -pg-last-output-displayform 304 0.0083169999 2.735...e-05 -proof-done-advancing-other 104 0.0077229999 7.425...e-05 -proof-set-overlay-arrow 205 0.0065570000 3.198...e-05 -proof-shell-process-urgent-messages 210 0.0064929999 3.091...e-05 -proof-shell-strip-output-markup 304 0.0062850000 2.067...e-05 -isar-strip-output-markup 306 0.0052059999 1.701...e-05 -proof-toolbar-state-enable-p 447 0.0047669999 1.066...e-05 -isar-global-save-command-p 100 0.0046590000 4.659...e-05 -isar-shell-adjust-line-width 210 0.004655 2.216...e-05 -proof-string-match-safe 204 0.0045679999 2.239...e-05 -proof-toolbar-retract-enable-p 447 0.0036200000 8.098...e-06 -isar-goal-command-p 205 0.0029619999 1.444...e-05 -proof-toolbar-delete-enable-p 447 0.0029529999 6.606...e-06 -proof-toolbar-undo-enable-p 447 0.0029139999 6.519...e-06 -proof-toolbar-find-enable-p 447 0.0027339999 6.116...e-06 -proof-toolbar-context-enable-p 447 0.0026389999 5.903...e-06 -proof-toolbar-info-enable-p 447 0.0026119999 5.843...e-06 -pg-processing-complete-hint 2 0.00235 0.001175 -proof-shell-classify-output 210 0.0023079999 1.099...e-05 -proof-locked-region-empty-p 451 0.0021040000 4.665...e-06 -proof-shell-process-urgent-message 3 0.001961 0.0006536666 -proof-replace-regexp-in-string 210 0.0018659999 8.885...e-06 -pg-add-element 100 0.001693 1.693...e-05 -proof-shell-message 2 0.00146 0.00073 -proof-unprocessed-begin 1367 0.0013369999 9.780...e-07 -proof-next-element-id 100 0.0012740000 1.274...e-05 -pg-span-name 304 0.0012510000 4.115...e-06 -pg-add-to-input-history 104 0.0012130000 1.166...e-05 -proof-shell-live-buffer 210 0.0011750000 5.595...e-06 -proof-done-retracting 2 0.001148 0.000574 -proof-script-delete-spans 2 0.0010550000 0.0005275000 -proof-process-buffer 1 0.001009 0.001009 -proof-assert-until-point-interactive 1 0.000976 0.000976 -proof-assert-until-point 1 0.000972 0.000972 -proof-assert-semis 1 0.000825 0.000825 -proof-append-alist 2 0.000691 0.0003455 -proof-retract-buffer 1 0.000549 0.000549 -proof-retract-until-point-interactive 1 0.000532 0.000532 -proof-retract-until-point 1 0.000528 0.000528 -pg-remove-element 30 0.000473 1.576...e-05 -proof-extend-queue 1 0.000463 0.000463 -proof-retract-target 1 0.000451 0.000451 -proof-element-id 100 0.0003829999 3.829...e-06 -proof-semis-to-vanillas 1 0.000334 0.000334 -proof-toolbar-goto-enable-p 447 0.0003170000 7.091...e-07 -proof-toolbar-interrupt-enable-p 447 0.0002790000 6.241...e-07 -proof-next-element-count 100 0.0002759999 2.759...e-06 -proof-start-queue 1 0.000241 0.000241 -pg-response-display-with-face 4 0.000229 5.725e-05 -proof-goto-end-of-locked 1 0.000182 0.000182 -proof-debug 100 0.0001309999 1.309...e-06 -isar-find-and-forget 1 9.7e-05 9.7e-05 -pg-remove-script-element 30 9.600...e-05 3.200...e-06 -proof-segment-up-to-using-cache 1 9.5e-05 9.5e-05 -pg-response-maybe-erase 4 8.999...e-05 2.249...e-05 -proof-segment-cache-contents-for 1 8.3e-05 8.3e-05 -proof-last-goal-or-goalsave 1 8e-05 8e-05 -pg-make-element-visible 30 7.600...e-05 2.533...e-06 -pg-redisplay-for-gnuemacs 30 6.8e-05 2.266...e-06 -proof-activate-scripting 2 4.3e-05 2.15e-05 -proof-shell-ready-prover 4 4.2e-05 1.05e-05 -proof-shell-handle-delayed-output 2 3.999...e-05 1.999...e-05 -proof-re-search-backward 1 3.6e-05 3.6e-05 -proof-shell-start 4 2.8e-05 7e-06 -proof-clean-buffer 1 2.6e-05 2.6e-05 -pg-response-display 2 2.499...e-05 1.249...e-05 -proof-grab-lock 2 2.2e-05 1.1e-05 -proof-shell-strip-eager-annotations 2 2.2e-05 1.1e-05 -proof-maybe-follow-locked-end 2 1.2e-05 6e-06 -proof-shell-stop-silent-item 2 1.1e-05 5.5e-06 -proof-shell-start-silent-item 2 1.1e-05 5.5e-06 -proof-setup-retract-action 2 7e-06 3.5e-06 -proof-shell-action-list-item 4 6.999...e-06 1.749...e-06 -proof-locked-end 2 6e-06 3e-06 -proof-queue-or-locked-end 4 4e-06 1e-06 -proof-shell-should-be-silent 2 3e-06 1.5e-06 -proof-display-and-keep-buffer 2 3e-06 1.5e-06 -proof-shell-set-silent 2 2e-06 1e-06 -proof-shell-clear-silent 2 2e-06 1e-06 -proof-script-next-command-advance 1 2e-06 2e-06 -proof-release-lock 2 2e-06 1e-06 -pg-finish-tracing-display 2 2e-06 1e-06 -isar-remove 1 2e-06 2e-06 -proof-pbp-focus-on-first-goal 2 1e-06 5e-07 +### 4.368s elapsed time, 0.457s cpu time, 0.094s GC time - ------------------------------------------------------------------ - -disabling shell cleaning - -proof-shell-filter-manage-output 205 0.2435890000 0.0011882390 -proof-shell-exec-loop 205 0.2398479999 0.0011699902 -proof-shell-insert 205 0.1606790000 0.0007838000 -proof-toolbar-find-enable-p 431 0.0806610000 0.0001871484 -proof-toolbar-retract-enable-p 431 0.0792429999 0.0001838584 -proof-locked-region-empty-p 432 0.0777940000 0.0001800787 -proof-done-advancing 203 0.0700679999 0.0003451625 -scomint-send-string 205 0.0527400000 0.0002572682 -proof-done-advancing-save 100 0.0341680000 0.00034168 -proof-toolbar-next-enable-p 862 0.0243430000 2.824...e-05 -proof-locked-region-full-p 863 0.0218720000 2.534...e-05 -proof-make-goalsave 100 0.0196210000 0.0001962100 -pg-set-span-helphighlights 303 0.0194000000 6.402...e-05 -proof-string-match 1316 0.0168150000 1.277...e-05 -proof-shell-available-p 3017 0.0122670000 4.065...e-06 -proof-toolbar-use-enable-p 431 0.0112489999 2.609...e-05 -pg-add-proof-element 100 0.0103299999 0.0001032999 -proof-done-advancing-other 103 0.0080660000 7.831...e-05 -pg-last-output-displayform 303 0.0080109999 2.643...e-05 -proof-set-overlay-arrow 203 0.0077329999 3.809...e-05 -proof-get-name-from-goal 100 0.0066490000 6.649...e-05 -proof-shell-strip-output-markup 303 0.0060620000 2.000...e-05 -proof-shell-process-urgent-messages 205 0.005429 2.648...e-05 -isar-global-save-command-p 100 0.0053289999 5.328...e-05 -pg-processing-complete-hint 1 0.005194 0.005194 -isar-strip-output-markup 304 0.0049429999 1.625...e-05 -isar-shell-adjust-line-width 205 0.0044570000 2.174...e-05 -proof-toolbar-state-enable-p 431 0.0043999999 1.020...e-05 -proof-string-match-safe 203 0.0041589999 2.048...e-05 -scomint-check-proc 3224 0.0036730000 1.139...e-06 -isar-goal-command-p 203 0.0028909999 1.424...e-05 -proof-toolbar-delete-enable-p 431 0.0028049999 6.508...e-06 -proof-toolbar-undo-enable-p 431 0.0027749999 6.438...e-06 -proof-toolbar-info-enable-p 431 0.0025189999 5.844...e-06 -proof-toolbar-context-enable-p 431 0.0025069999 5.816...e-06 -proof-toolbar-command-enable-p 431 0.0024369999 5.654...e-06 -proof-shell-classify-output 205 0.0019569999 9.546...e-06 -pg-hint 1 0.001928 0.001928 -proof-replace-regexp-in-string 205 0.0016949999 8.268...e-06 -pg-add-element 100 0.0016770000 1.677...e-05 -proof-shell-process-urgent-message 1 0.001473 0.001473 -proof-shell-message 1 0.00126 0.00126 -proof-next-element-id 100 0.0012599999 1.259...e-05 -pg-span-name 303 0.0012540000 4.138...e-06 -proof-unprocessed-begin 1311 0.0012240000 9.336...e-07 -pg-add-to-input-history 103 0.0012010000 1.166...e-05 -proof-shell-live-buffer 205 0.0011310000 5.517...e-06 -proof-process-buffer 1 0.000884 0.000884 -proof-assert-until-point-interactive 1 0.000848 0.000848 -proof-assert-until-point 1 0.000845 0.000845 -proof-assert-semis 1 0.000686 0.000686 -proof-goto-end-of-locked 3 0.000527 0.0001756666 -proof-element-id 100 0.0003679999 3.679...e-06 -proof-semis-to-vanillas 1 0.000335 0.000335 -proof-extend-queue 1 0.000324 0.000324 -proof-toolbar-goto-enable-p 431 0.0003190000 7.401...e-07 -proof-append-alist 1 0.000315 0.000315 -proof-next-element-count 100 0.0002809999 2.809...e-06 -proof-toolbar-interrupt-enable-p 431 0.0002599999 6.032...e-07 -pg-response-display-with-face 2 0.000134 6.7e-05 -proof-debug 100 0.0001269999 1.269...e-06 -proof-segment-up-to-using-cache 1 9e-05 9e-05 -proof-segment-cache-contents-for 1 7.9e-05 7.9e-05 -proof-re-search-backward 1 5.1e-05 5.1e-05 -proof-shell-handle-delayed-output 1 2.3e-05 2.3e-05 -proof-shell-ready-prover 2 1.9e-05 9.5e-06 -proof-activate-scripting 1 1.7e-05 1.7e-05 -pg-response-maybe-erase 2 1.7e-05 8.5e-06 -pg-response-display 1 1.6e-05 1.6e-05 -proof-shell-start 2 1.300...e-05 6.500...e-06 -proof-shell-strip-eager-annotations 1 1.3e-05 1.3e-05 -proof-grab-lock 1 1.1e-05 1.1e-05 -proof-maybe-follow-locked-end 1 9e-06 9e-06 -proof-shell-stop-silent-item 1 6e-06 6e-06 -proof-shell-start-silent-item 1 5e-06 5e-06 -proof-queue-or-locked-end 4 4e-06 1e-06 +proof-shell-wait 1 4.484316 4.484316 +accept-process-output 73 3.8998559999 0.0534226849 +redisplay 172 3.7155909999 0.0216022732 +scomint-output-filter 206 3.5921849999 0.0174377912 +proof-shell-filter 206 3.5562370000 0.0172632864 +proof-shell-filter-manage-output 206 3.5167620000 0.0170716601 +proof-shell-exec-loop 206 3.5079160000 0.0170287184 +mapc 208 3.4532319999 0.0166020769 +proof-shell-invoke-callback 206 3.4492200000 0.0167437864 +proof-done-advancing 204 3.4481900000 0.0169028921 +proof-done-advancing-other 104 3.2636610000 0.0313813557 +pg-add-element 204 3.2225049999 0.0157965931 +proof-debug 99 3.1809079999 0.0321303838 +pg-autotest-message 99 3.1785960000 0.0321070303 +proof-process-buffer 1 0.098653 0.098653 +proof-assert-until-point-interactive 1 0.098513 0.098513 +proof-assert-until-point 1 0.098508 0.098508 +proof-done-advancing-save 100 0.0861289999 0.0008612899 +pg-set-span-helphighlights 304 0.0751920000 0.0002473421 +proof-make-goalsave 100 0.074799 0.00074799 +proof-assert-semis 1 0.072791 0.072791 +proof-shell-insert-action-item 206 0.0508700000 0.0002469417 +proof-shell-insert 206 0.0500239999 0.0002428349 +proof-set-locked-end 204 0.0447420000 0.0002193235 +proof-semis-to-vanillas 1 0.043912 0.043912 +proof-set-locked-endpoints 204 0.0438019999 0.0002147156 +proof-set-overlay-arrow 204 0.039986 0.0001960098 +span-set-property 4968 0.0389520000 7.840...e-06 +isar-command-wrapping 204 0.0359119999 0.0001760392 +isar-global-save-command-p 100 0.0357419999 0.0003574199 +span-at-before 200 0.033411 0.0001670550 +proof-script-delete-secondary-spans 1 0.02853 0.02853 +span-delete-spans 1 0.028527 0.028527 +span-mapc-spans 1 0.028523 0.028523 +pg-add-proof-element 100 0.0274090000 0.0002740900 +proof-segment-up-to-using-cache 1 0.025547 0.025547 +proof-segment-up-to 1 0.025512 0.025512 +proof-segment-up-to-parser 1 0.025509 0.025509 +proof-script-generic-parse-cmdstart 204 0.023117 0.0001133186 +replace-regexp-in-string 612 0.0151239999 2.471...e-05 +pg-last-output-displayform 304 0.0137170000 4.512...e-05 +goto-char 3399 0.0134079999 3.944...e-06 +proof-buffer-syntactic-context 411 0.0133350000 3.244...e-05 +proof-buffer-syntactic-context-emulate 411 0.0125479999 3.053...e-05 +proof-shell-strip-output-markup 202 0.0118950000 5.888...e-05 +isar-strip-output-markup 202 0.01126 5.574...e-05 +scomint-send-input 206 0.0089030000 4.321...e-05 +skip-chars-forward 917 0.0077629999 8.465...e-06 +proof-string-match 1114 0.0076579999 6.874...e-06 +string-match 3859 0.0065880000 1.707...e-06 +isar-positions-of 204 0.0063140000 3.095...e-05 +proof-shell-handle-immediate-output 206 0.0061669999 2.993...e-05 +proof-shell-process-urgent-messages 206 0.006087 2.954...e-05 +re-search-forward 1048 0.0060810000 5.802...e-06 +isar-string-wrapping 408 0.0055940000 1.371...e-05 +isar-preprocessing 206 0.0048040000 2.332...e-05 +insert 718 0.0036899999 5.139...e-06 +proof-re-search-forward-safe 824 0.0034060000 4.133...e-06 +proof-next-element-id 204 0.0033579999 1.646...e-05 +span-set-endpoints 409 0.0031649999 7.738...e-06 +proof-set-queue-start 204 0.0029729999 1.457...e-05 +span-delete 304 0.0027480000 9.039...e-06 +isar-goal-command-p 204 0.0027019999 1.324...e-05 +span-make 608 0.0026310000 4.327...e-06 +span-end 926 0.0024999999 2.699...e-06 +overlay-put 4977 0.0024500000 4.922...e-07 +pg-add-to-input-history 204 0.002432 1.192...e-05 +proof-string-match-safe 204 0.0024030000 1.177...e-05 +proof-get-name-from-goal 100 0.0022690000 2.269...e-05 +span-set-start 204 0.0022479999 1.101...e-05 +move-overlay 413 0.0020689999 5.009...e-06 +pg-span-name 102 0.0019750000 1.936...e-05 +span-start 604 0.0016740000 2.771...e-06 +replace-match 1008 0.0015839999 1.571...e-06 +span-live-p 408 0.0015820000 3.877...e-06 +proof-element-id 204 0.0015369999 7.534...e-06 +span-property 2226 0.0014979999 6.729...e-07 +make-overlay 609 0.0012819999 2.105...e-06 +delete-overlay 309 0.0012420000 4.019...e-06 +skip-chars-backward 206 0.0011609999 5.635...e-06 +proof-shell-slurp-comments 207 0.0011250000 5.434...e-06 +set-marker 1853 0.0009220000 4.975...e-07 +pg-processing-complete-hint 1 0.000625 0.000625 +proof-next-element-count 204 0.0005830000 2.857...e-06 +spans-at-region-prop 1 0.000573 0.000573 +proof-shell-handle-delayed-output 1 0.000495 0.000495 +proof-shell-display-output-as-response 1 0.000478 0.000478 +pg-response-display 1 0.000474 0.000474 +proof-display-and-keep-buffer 1 0.000463 0.000463 +overlay-end 1126 0.0004170000 3.703...e-07 +marker-position 1236 0.0004100000 3.317...e-07 +match-string 308 0.0003959999 1.285...e-06 +buffer-live-p 725 0.0003580000 4.937...e-07 +isar-shell-adjust-line-width 206 0.0003170000 1.538...e-06 +proof-extend-queue 1 0.000293 0.000293 +proof-add-to-queue 1 0.000266 0.000266 +get-buffer-process 209 0.0002369999 1.133...e-06 +overlay-start 604 0.0002369999 3.923...e-07 +proof-shell-process-urgent-message 1 0.000232 0.000232 +proof-shell-process-urgent-message-default 1 0.000169 0.000169 +font-lock-fontify-region 1 0.000167 0.000167 +font-lock-default-fontify-region 1 0.00016 0.00016 +nreverse 209 0.0001489999 7.129...e-07 +proof-get-window-for-buffer 1 0.000124 0.000124 +font-lock-fontify-keywords-region 1 0.000117 0.000117 +proof-only-whitespace-to-locked-region-p 1 0.000108 0.000108 +proof-re-search-backward 1 8.2e-05 8.2e-05 +pg-response-display-with-face 2 8.2e-05 4.1e-05 +re-search-backward 1 6.7e-05 6.7e-05 +pg-response-maybe-erase 2 5.900...e-05 2.950...e-05 +font-lock-mode 3 5.8e-05 1.933...e-05 +proof-queue-or-locked-end 6 5.600...e-05 9.333...e-06 +proof-shell-ready-prover 2 4.6e-05 2.3e-05 +proof-looking-at-safe 8 4.2e-05 5.25e-06 +proof-shell-start 2 3.700...e-05 1.850...e-05 +proof-maybe-follow-locked-end 1 3.5e-05 3.5e-05 +proof-shell-live-buffer 2 3.1e-05 1.55e-05 +proof-activate-scripting 1 2.8e-05 2.8e-05 +proof-looking-at 7 2.8e-05 4e-06 +proof-grab-lock 1 2.7e-05 2.7e-05 +proof-unprocessed-begin 3 2.399...e-05 8e-06 +proof-shell-should-be-silent 1 2.2e-05 2.2e-05 +proof-detach-queue 1 1.8e-05 1.8e-05 +scomint-check-proc 2 1.7e-05 8.5e-06 +font-lock-fontify-syntactically-region 1 1.7e-05 1.7e-05 +isar-font-lock-fontify-syntactically-region 1 1.6e-05 1.6e-05 +span-detach 1 1.5e-05 1.5e-05 +font-lock-default-function 3 1.400...e-05 4.666...e-06 +proof-shell-strip-eager-annotations 1 1.1e-05 1.1e-05 +font-lock-extend-jit-lock-region-after-change 3 1e-05 3.333...e-06 +proof-set-queue-endpoints 1 8e-06 8e-06 +font-lock-unfontify-region 1 7e-06 7e-06 +proof-re-search-forward 1 6e-06 6e-06 +proof-associated-windows 1 6e-06 6e-06 +proof-script-next-command-advance 1 6e-06 6e-06 +proof-shell-stop-silent-item 1 4e-06 4e-06 +proof-shell-start-silent-item 1 4e-06 4e-06 proof-shell-action-list-item 2 3e-06 1.5e-06 -proof-script-next-command-advance 1 2e-06 2e-06 +proof-shell-clear-silent 1 3e-06 3e-06 +process-status 2 2e-06 1e-06 +font-lock-set-defaults 1 2e-06 2e-06 +proof-associated-buffers 2 1e-06 5e-07 +proof-minibuffer-message 1 1e-06 1e-06 proof-shell-set-silent 1 1e-06 1e-06 -proof-shell-should-be-silent 1 1e-06 1e-06 -proof-shell-clear-silent 1 1e-06 1e-06 -proof-pbp-focus-on-first-goal 1 1e-06 1e-06 -proof-display-and-keep-buffer 1 1e-06 1e-06 proof-release-lock 1 1e-06 1e-06 pg-finish-tracing-display 1 1e-06 1e-06 +nconc 1 1e-06 1e-06 +font-lock-extend-region-wholelines 1 1e-06 1e-06 +font-lock-default-unfontify-region 1 1e-06 1e-06 +proof-pbp-focus-on-first-goal 1 0.0 0.0 +font-lock-extend-region-multiline 1 0.0 0.0 - ------------------------------------------------------------------ |