more on Isabelle document preparation and bibtex files;
authorwenzelm
Mon May 04 20:05:50 2015 +0200 (2015-05-04)
changeset 602550466bd194d74
parent 60254 52110106c0ca
child 60256 2925c5552e25
more on Isabelle document preparation and bibtex files;
src/Doc/JEdit/JEdit.thy
src/Doc/JEdit/document/bibtex-mode.png
src/Doc/JEdit/document/cite-completion.png
src/Doc/JEdit/document/sidekick-document.png
src/Doc/ROOT
     1.1 --- a/src/Doc/JEdit/JEdit.thy	Mon May 04 19:55:30 2015 +0200
     1.2 +++ b/src/Doc/JEdit/JEdit.thy	Mon May 04 20:05:50 2015 +0200
     1.3 @@ -1567,6 +1567,70 @@
     1.4    nonetheless, say to remove earlier proof attempts.\<close>
     1.5  
     1.6  
     1.7 +chapter \<open>Isabelle document preparation\<close>
     1.8 +
     1.9 +text \<open>The ultimate purpose of Isabelle is to produce nicely rendered documents
    1.10 +  with the Isabelle document preparation system, which is based on {\LaTeX};
    1.11 +  see also @{cite "isabelle-sys" and "isabelle-isar-ref"}. Isabelle/jEdit
    1.12 +  provides some additional support for document editing.\<close>
    1.13 +
    1.14 +
    1.15 +section \<open>Document outline\<close>
    1.16 +
    1.17 +text \<open>Theory sources may contain document markup commands, such as
    1.18 +  @{command_ref chapter}, @{command_ref section}, @{command subsection}. The
    1.19 +  Isabelle SideKick parser (\secref{sec:sidekick}) represents this document
    1.20 +  outline as structured tree view, with formal statements and proofs nested
    1.21 +  inside; see \figref{fig:sidekick-document}.
    1.22 +
    1.23 +  \begin{figure}[htb]
    1.24 +  \begin{center}
    1.25 +  \includegraphics[scale=0.333]{sidekick-document}
    1.26 +  \end{center}
    1.27 +  \caption{Isabelle document outline via SideKick tree view}
    1.28 +  \label{fig:sidekick-document}
    1.29 +  \end{figure}
    1.30 +\<close>
    1.31 +
    1.32 +section \<open>Citations and Bib{\TeX} entries\<close>
    1.33 +
    1.34 +text \<open>Citations are managed by {\LaTeX} and Bib{\TeX} in @{verbatim ".bib"}
    1.35 +  files. The Isabelle session build process and the
    1.36 +  @{verbatim "isabelle latex"} tool @{cite "isabelle-sys"} are smart enough
    1.37 +  to assemble the result, based on the session directory layout.
    1.38 +
    1.39 +  The document antiquotation @{text "@{cite}"} is described in @{cite
    1.40 +  "isabelle-isar-ref"}. Within the Prover IDE it provides semantic markup for
    1.41 +  tooltips, hyperlinks, and completion for Bib{\TeX} database entries.
    1.42 +  Isabelle/jEdit does \emph{not} know about the actual Bib{\TeX} environment
    1.43 +  used in {\LaTeX} batch-mode, but it can take citations from those @{verbatim
    1.44 +  ".bib"} files that happen to be open in the editor; see
    1.45 +  \figref{fig:cite-completion}.
    1.46 +
    1.47 +  \begin{figure}[htb]
    1.48 +  \begin{center}
    1.49 +  \includegraphics[scale=0.333]{cite-completion}
    1.50 +  \end{center}
    1.51 +  \caption{Semantic completion of citations from open Bib{\TeX} files}
    1.52 +  \label{fig:cite-completion}
    1.53 +  \end{figure}
    1.54 +
    1.55 +  Isabelle/jEdit also provides some support for editing @{verbatim ".bib"}
    1.56 +  files themselves. There is syntax highlighting based on entry types
    1.57 +  (according to standard Bib{\TeX} styles), a context-menu to compose entries
    1.58 +  systematically, and a SideKick tree view of the overall content; see
    1.59 +  \figref{fig:bibtex-mode}.
    1.60 +
    1.61 +  \begin{figure}[htb]
    1.62 +  \begin{center}
    1.63 +  \includegraphics[scale=0.333]{bibtex-mode}
    1.64 +  \end{center}
    1.65 +  \caption{Bib{\TeX} mode with context menu and SideKick tree view}
    1.66 +  \label{fig:bibtex-mode}
    1.67 +  \end{figure}
    1.68 +\<close>
    1.69 +
    1.70 +
    1.71  chapter \<open>Miscellaneous tools\<close>
    1.72  
    1.73  section \<open>Timing\<close>
     2.1 Binary file src/Doc/JEdit/document/bibtex-mode.png has changed
     3.1 Binary file src/Doc/JEdit/document/cite-completion.png has changed
     4.1 Binary file src/Doc/JEdit/document/sidekick-document.png has changed
     5.1 --- a/src/Doc/ROOT	Mon May 04 19:55:30 2015 +0200
     5.2 +++ b/src/Doc/ROOT	Mon May 04 20:05:50 2015 +0200
     5.3 @@ -183,7 +183,9 @@
     5.4      "style.sty"
     5.5    document_files
     5.6      "auto-tools.png"
     5.7 +    "bibtex-mode.png"
     5.8      "build"
     5.9 +    "cite-completion.png"
    5.10      "isabelle-jedit.png"
    5.11      "output.png"
    5.12      "query.png"
    5.13 @@ -191,6 +193,7 @@
    5.14      "popup2.png"
    5.15      "root.tex"
    5.16      "sidekick.png"
    5.17 +    "sidekick-document.png"
    5.18      "sledgehammer.png"
    5.19      "theories.png"
    5.20