equal
deleted
inserted
replaced
1900 text \<open> |
1900 text \<open> |
1901 The action @{action_def isabelle.preview} opens an HTML preview of the |
1901 The action @{action_def isabelle.preview} opens an HTML preview of the |
1902 current document node in the default web browser. The content is derived |
1902 current document node in the default web browser. The content is derived |
1903 from the semantic markup produced by the prover, and thus depends on the |
1903 from the semantic markup produced by the prover, and thus depends on the |
1904 status of formal processing. |
1904 status of formal processing. |
|
1905 |
|
1906 Action @{action_def isabelle.draft} is similar to @{action |
|
1907 isabelle.preview}, but shows a plain-text document draft. |
1905 \<close> |
1908 \<close> |
1906 |
1909 |
1907 |
1910 |
1908 chapter \<open>ML debugging within the Prover IDE\<close> |
1911 chapter \<open>ML debugging within the Prover IDE\<close> |
1909 |
1912 |