# HG changeset patch # User wenzelm # Date 1335621990 -7200 # Node ID 34b44d28fc4bb90f253df53a289989641fb40b2a # Parent a2d604542a34d4f1c56820b4b81f609ea9233dcf some updates concerning current Proof General 4.x, which lacks X-Symbol mode of 3.x; removed historic note about Poly/ML vs. SML/NJ; diff -r a2d604542a34 -r 34b44d28fc4b doc-src/IsarRef/Thy/Outer_Syntax.thy --- a/doc-src/IsarRef/Thy/Outer_Syntax.thy Sat Apr 28 11:24:20 2012 +0200 +++ b/doc-src/IsarRef/Thy/Outer_Syntax.thy Sat Apr 28 16:06:30 2012 +0200 @@ -168,12 +168,11 @@ Common mathematical symbols such as @{text \} are represented in Isabelle as @{verbatim \}. There are infinitely many Isabelle symbols like this, although proper presentation is left to front-end - tools such as {\LaTeX} or Proof~General with the X-Symbol package. - A list of predefined Isabelle symbols that work well with these - tools is given in \appref{app:symbols}. Note that @{verbatim "\"} - does not belong to the @{text letter} category, since it is already - used differently in the Pure term language. -*} + tools such as {\LaTeX}, Proof~General, or Isabelle/jEdit. A list of + predefined Isabelle symbols that work well with these tools is given + in \appref{app:symbols}. Note that @{verbatim "\"} does not belong + to the @{text letter} category, since it is already used differently + in the Pure term language. *} section {* Common syntax entities *} diff -r a2d604542a34 -r 34b44d28fc4b doc-src/IsarRef/Thy/Symbols.thy --- a/doc-src/IsarRef/Thy/Symbols.thy Sat Apr 28 11:24:20 2012 +0200 +++ b/doc-src/IsarRef/Thy/Symbols.thy Sat Apr 28 16:06:30 2012 +0200 @@ -14,8 +14,7 @@ appropriate definitions of @{verbatim "\\"}@{verbatim isasym}@{text name} for each @{verbatim "\\"}@{verbatim "<"}@{text name}@{verbatim ">"} in the @{verbatim isabellesym.sty} file. Most of these symbols - are displayed properly in Proof~General if used with the X-Symbol - package. + are displayed properly in Proof~General and Isabelle/jEdit. Moreover, any single symbol (or ASCII character) may be prefixed by @{verbatim "\\"}@{verbatim "<^sup>"}, for superscript and @{verbatim diff -r a2d604542a34 -r 34b44d28fc4b doc-src/IsarRef/Thy/document/Outer_Syntax.tex --- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex Sat Apr 28 11:24:20 2012 +0200 +++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex Sat Apr 28 16:06:30 2012 +0200 @@ -183,11 +183,11 @@ Common mathematical symbols such as \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}} are represented in Isabelle as \verb|\|. There are infinitely many Isabelle symbols like this, although proper presentation is left to front-end - tools such as {\LaTeX} or Proof~General with the X-Symbol package. - A list of predefined Isabelle symbols that work well with these - tools is given in \appref{app:symbols}. Note that \verb|\| - does not belong to the \isa{letter} category, since it is already - used differently in the Pure term language.% + tools such as {\LaTeX}, Proof~General, or Isabelle/jEdit. A list of + predefined Isabelle symbols that work well with these tools is given + in \appref{app:symbols}. Note that \verb|\| does not belong + to the \isa{letter} category, since it is already used differently + in the Pure term language.% \end{isamarkuptext}% \isamarkuptrue% % diff -r a2d604542a34 -r 34b44d28fc4b doc-src/IsarRef/Thy/document/Symbols.tex --- a/doc-src/IsarRef/Thy/document/Symbols.tex Sat Apr 28 11:24:20 2012 +0200 +++ b/doc-src/IsarRef/Thy/document/Symbols.tex Sat Apr 28 16:06:30 2012 +0200 @@ -29,8 +29,7 @@ The collection of predefined standard symbols given below is available by default for Isabelle document output, due to appropriate definitions of \verb|\|\verb|isasym|\isa{name} for each \verb|\|\verb|<|\isa{name}\verb|>| in the \verb|isabellesym.sty| file. Most of these symbols - are displayed properly in Proof~General if used with the X-Symbol - package. + are displayed properly in Proof~General and Isabelle/jEdit. Moreover, any single symbol (or ASCII character) may be prefixed by \verb|\|\verb|<^sup>|, for superscript and \verb|\|\verb|<^sub>|, for subscript, such as \verb|A\|\verb|<^sup>\|, for \isa{{\isaliteral{22}{\isachardoublequote}}A\isaliteral{5C3C5E7375703E}{}\isactrlsup {\isaliteral{5C3C737461723E}{\isasymstar}}{\isaliteral{22}{\isachardoublequote}}} the alternative diff -r a2d604542a34 -r 34b44d28fc4b doc-src/System/Thy/Interfaces.thy --- a/doc-src/System/Thy/Interfaces.thy Sat Apr 28 11:24:20 2012 +0200 +++ b/doc-src/System/Thy/Interfaces.thy Sat Apr 28 16:06:30 2012 +0200 @@ -62,12 +62,13 @@ interface} script. \item[@{setting_def XSYMBOL_INSTALLFONTS}] may contain a small shell - script to install the X11 fonts required for the X-Symbols mode of - Proof General. This is only relevant if the X11 display server runs - on a different machine than the Emacs application, with a different - file-system view on the Proof General installation. Under most - circumstances Proof General is able to refer to the font files that - are part of its distribution. + script to install the X11 fonts required for the old X-Symbols mode + of Proof General. This is only relevant if the X11 display server + runs on a different machine than the Emacs application, with a + different file-system view on the Proof General installation. Under + most circumstances Proof General 3.x is able to refer to the font + files that are part of its distribution, and Proof General 4.x finds + its fonts by different means. \end{description} *} diff -r a2d604542a34 -r 34b44d28fc4b doc-src/System/Thy/document/Interfaces.tex --- a/doc-src/System/Thy/document/Interfaces.tex Sat Apr 28 11:24:20 2012 +0200 +++ b/doc-src/System/Thy/document/Interfaces.tex Sat Apr 28 16:06:30 2012 +0200 @@ -82,12 +82,13 @@ the command line of any invocation of the Proof General \verb|interface| script. \item[\indexdef{}{setting}{XSYMBOL\_INSTALLFONTS}\hypertarget{setting.XSYMBOL-INSTALLFONTS}{\hyperlink{setting.XSYMBOL-INSTALLFONTS}{\mbox{\isa{\isatt{XSYMBOL{\isaliteral{5F}{\isacharunderscore}}INSTALLFONTS}}}}}] may contain a small shell - script to install the X11 fonts required for the X-Symbols mode of - Proof General. This is only relevant if the X11 display server runs - on a different machine than the Emacs application, with a different - file-system view on the Proof General installation. Under most - circumstances Proof General is able to refer to the font files that - are part of its distribution. + script to install the X11 fonts required for the old X-Symbols mode + of Proof General. This is only relevant if the X11 display server + runs on a different machine than the Emacs application, with a + different file-system view on the Proof General installation. Under + most circumstances Proof General 3.x is able to refer to the font + files that are part of its distribution, and Proof General 4.x finds + its fonts by different means. \end{description}% \end{isamarkuptext}% diff -r a2d604542a34 -r 34b44d28fc4b doc-src/TutorialI/Documents/Documents.thy --- a/doc-src/TutorialI/Documents/Documents.thy Sat Apr 28 11:24:20 2012 +0200 +++ b/doc-src/TutorialI/Documents/Documents.thy Sat Apr 28 16:06:30 2012 +0200 @@ -148,10 +148,10 @@ (*>*) text {* - \noindent The X-Symbol package within Proof~General provides several - input methods to enter @{text \} in the text. If all fails one may - just type a named entity \verb,\,\verb,, by hand; the - corresponding symbol will be displayed after further input. + \noindent Proof~General provides several input methods to enter + @{text \} in the text. If all fails one may just type a named + entity \verb,\,\verb,, by hand; the corresponding symbol will + be displayed after further input. More flexible is to provide alternative syntax forms through the \bfindex{print mode} concept~\cite{isabelle-ref}. By diff -r a2d604542a34 -r 34b44d28fc4b doc-src/TutorialI/Documents/document/Documents.tex --- a/doc-src/TutorialI/Documents/document/Documents.tex Sat Apr 28 11:24:20 2012 +0200 +++ b/doc-src/TutorialI/Documents/document/Documents.tex Sat Apr 28 16:06:30 2012 +0200 @@ -182,10 +182,10 @@ \endisadelimML % \begin{isamarkuptext}% -\noindent The X-Symbol package within Proof~General provides several - input methods to enter \isa{{\isaliteral{5C3C6F706C75733E}{\isasymoplus}}} in the text. If all fails one may - just type a named entity \verb,\,\verb,, by hand; the - corresponding symbol will be displayed after further input. +\noindent Proof~General provides several input methods to enter + \isa{{\isaliteral{5C3C6F706C75733E}{\isasymoplus}}} in the text. If all fails one may just type a named + entity \verb,\,\verb,, by hand; the corresponding symbol will + be displayed after further input. More flexible is to provide alternative syntax forms through the \bfindex{print mode} concept~\cite{isabelle-ref}. By diff -r a2d604542a34 -r 34b44d28fc4b doc-src/TutorialI/preface.tex --- a/doc-src/TutorialI/preface.tex Sat Apr 28 11:24:20 2012 +0200 +++ b/doc-src/TutorialI/preface.tex Sat Apr 28 16:06:30 2012 +0200 @@ -35,17 +35,11 @@ from output generated in this way. The final chapter of Part~I explains how users may produce their own formal documents in a similar fashion. -Isabelle's \hfootref{http://isabelle.in.tum.de/}{web site} contains links to -the download area and to documentation and other information. Most Isabelle -sessions are now run from within David Aspinall's\index{Aspinall, David} -wonderful user interface, \hfootref{http://proofgeneral.inf.ed.ac.uk/}{Proof - General}, even together with the -\hfootref{http://x-symbol.sourceforge.net}{X-Symbol} package for XEmacs. This -book says very little about Proof General, which has its own documentation. -In order to run Isabelle, you will need a Standard ML compiler. We recommend -\hfootref{http://www.polyml.org/}{Poly/ML}, which is free and gives the best -performance. The other fully supported compiler is -\hfootref{http://www.smlnj.org/index.html}{Standard ML of New Jersey}. +Isabelle's \hfootref{http://isabelle.in.tum.de/}{web site} contains +links to the download area and to documentation and other information. +The classic Isabelle user interface is Proof~General~/ Emacs by David +Aspinall's\index{Aspinall, David}. This book says very little about +Proof General, which has its own documentation. This tutorial owes a lot to the constant discussions with and the valuable feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf