equal
deleted
inserted
replaced
77 for an empty toplevel state. |
77 for an empty toplevel state. |
78 |
78 |
79 \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof |
79 \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof |
80 state if available, otherwise raises @{ML Toplevel.UNDEF}. |
80 state if available, otherwise raises @{ML Toplevel.UNDEF}. |
81 |
81 |
82 \item @{ML "Toplevel.debug := true"} enables low-level exception |
82 \item @{ML "Toplevel.debug := true"} enables exception trace of the |
83 trace of the ML runtime system. Note that the result might appear |
83 ML runtime system. |
84 on some raw output window only, outside the formal context of the |
|
85 source text. |
|
86 |
84 |
87 \item @{ML "Toplevel.timing := true"} makes the toplevel print timing |
85 \item @{ML "Toplevel.timing := true"} makes the toplevel print timing |
88 information for each Isar command being executed. |
86 information for each Isar command being executed. |
89 |
87 |
90 \item @{ML Toplevel.profiling}~@{ML_text ":="}~@{text "n"} controls |
88 \item @{ML Toplevel.profiling}~@{ML_text ":="}~@{text "n"} controls |