516 session-qualified theory name (e.g.\ \<^verbatim>\<open>HOL-ex.Seq\<close>). |
516 session-qualified theory name (e.g.\ \<^verbatim>\<open>HOL-ex.Seq\<close>). |
517 |
517 |
518 \<^item> \<^bold>\<open>type\<close> \<open>node_status = {ok: bool, total: int, unprocessed: int, running: |
518 \<^item> \<^bold>\<open>type\<close> \<open>node_status = {ok: bool, total: int, unprocessed: int, running: |
519 int, warned: int, failed: int, finished: int, canceled: bool, initialized: |
519 int, warned: int, failed: int, finished: int, canceled: bool, initialized: |
520 bool, consolidated: bool}\<close> represents a formal theory node status of the |
520 bool, consolidated: bool}\<close> represents a formal theory node status of the |
521 PIDE document model. Fields \<open>total\<close>, \<open>unprocessed\<close>, \<open>running\<close>, \<open>warned\<close>, |
521 PIDE document model as follows. |
522 \<open>failed\<close>, \<open>finished\<close> account for individual commands within a theory node; |
522 |
523 \<open>ok\<close> is an abstraction for \<open>failed = 0\<close>. The \<open>canceled\<close> flag tells if some |
523 \<^item> Fields \<open>total\<close>, \<open>unprocessed\<close>, \<open>running\<close>, \<open>warned\<close>, \<open>failed\<close>, \<open>finished\<close> |
524 command in the theory has been spontaneously canceled (by an Interrupt |
524 account for individual commands within a theory node; \<open>ok\<close> is an |
525 exception that could also indicate resource problems). The \<open>terminated\<close> flag |
525 abstraction for \<open>failed = 0\<close>. |
526 indicates that all evaluations in the node has finished. The \<open>initialized\<close> |
526 |
527 flag indicates that the initial \<^theory_text>\<open>theory\<close> command has been processed. The |
527 \<^item> The \<open>canceled\<close> flag tells if some command in the theory has been |
528 \<open>consolidated\<close> flag indicates whether the outermost theory command structure |
528 spontaneously canceled (by an Interrupt exception that could also |
529 has finished (or failed) and the final \<^theory_text>\<open>end\<close> command has been checked. |
529 indicate resource problems). |
|
530 |
|
531 \<^item> The \<open>terminated\<close> flag indicates that all evaluations in the node has |
|
532 finished. |
|
533 |
|
534 \<^item> The \<open>initialized\<close> flag indicates that the initial \<^theory_text>\<open>theory\<close> command has |
|
535 been processed. |
|
536 |
|
537 \<^item> The \<open>consolidated\<close> flag indicates whether the outermost theory command |
|
538 structure has finished (or failed) and the final \<^theory_text>\<open>end\<close> command has been |
|
539 checked. |
530 \<close> |
540 \<close> |
531 |
541 |
532 |
542 |
533 section \<open>Server commands and results\<close> |
543 section \<open>Server commands and results\<close> |
534 |
544 |