Wed Aug 18 2010. See Trac #324. ----------------------------------------------------------------- Interactive: C-c C-n ### 12.461s elapsed time, 0.514s cpu time, 0.108s GC time 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 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-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 ----------------------------------------------------------------- Non-interactive: (progn (proof-process-buffer) (proof-shell-wait)) ### 4.368s elapsed time, 0.457s cpu time, 0.094s GC time 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-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-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