equal
deleted
inserted
replaced
83 for an empty toplevel state. |
83 for an empty toplevel state. |
84 |
84 |
85 \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof |
85 \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof |
86 state if available, otherwise raises @{ML Toplevel.UNDEF}. |
86 state if available, otherwise raises @{ML Toplevel.UNDEF}. |
87 |
87 |
88 \item @{ML "Toplevel.debug := true"} makes the toplevel print further |
88 \item @{ML "Toplevel.debug := true"} enables low-level exception |
89 details about internal error conditions, exceptions being raised |
89 trace of the ML runtime system. Note that the result might appear |
90 etc. |
90 on some raw output window only, outside the formal context of the |
|
91 source text. |
91 |
92 |
92 \item @{ML "Toplevel.timing := true"} makes the toplevel print timing |
93 \item @{ML "Toplevel.timing := true"} makes the toplevel print timing |
93 information for each Isar command being executed. |
94 information for each Isar command being executed. |
94 |
95 |
95 \item @{ML Toplevel.profiling}~@{ML_text ":="}~@{text "n"} controls |
96 \item @{ML Toplevel.profiling}~@{ML_text ":="}~@{text "n"} controls |