# HG changeset patch
# User wenzelm
# Date 1125528324 -7200
# Node ID af174eeafba198339150d11c35e8087c0a49db03
# Parent  ba65f3e5653c9e08a1730fb346d266a2f808b64a
updated;

diff -r ba65f3e5653c -r af174eeafba1 doc-src/AxClass/Group/document/isabelle.sty
--- a/doc-src/AxClass/Group/document/isabelle.sty	Wed Aug 31 18:46:56 2005 +0200
+++ b/doc-src/AxClass/Group/document/isabelle.sty	Thu Sep 01 00:45:24 2005 +0200
@@ -114,8 +114,8 @@
 \newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
 \newcommand{\isaendpar}{\par\medskip}
 \newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
-\newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}}
-\newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}}
+\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
+\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
 \newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
 
 
diff -r ba65f3e5653c -r af174eeafba1 doc-src/IsarOverview/Isar/document/isabelle.sty
--- a/doc-src/IsarOverview/Isar/document/isabelle.sty	Wed Aug 31 18:46:56 2005 +0200
+++ b/doc-src/IsarOverview/Isar/document/isabelle.sty	Thu Sep 01 00:45:24 2005 +0200
@@ -114,8 +114,8 @@
 \newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
 \newcommand{\isaendpar}{\par\medskip}
 \newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
-\newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}}
-\newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}}
+\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
+\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
 \newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
 
 
diff -r ba65f3e5653c -r af174eeafba1 doc-src/LaTeXsugar/Sugar/document/Sugar.tex
--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Wed Aug 31 18:46:56 2005 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Thu Sep 01 00:45:24 2005 +0200
@@ -7,7 +7,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
@@ -27,7 +26,7 @@
 bliss of writing \verb!@!\verb!{thm[display]setsum_cartesian_product[no_vars]}!
 and seeing Isabelle typeset it for them:
 \begin{isabelle}%
-{\isacharparenleft}{\isasymSum}x{\isasymin}A{\isachardot}\ {\isasymSum}y{\isasymin}B{\isachardot}\ f\ x\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}z{\isasymin}A\ {\isasymtimes}\ B{\isachardot}\ f\ {\isacharparenleft}fst\ z{\isacharparenright}\ {\isacharparenleft}snd\ z{\isacharparenright}{\isacharparenright}%
+{\isacharparenleft}{\isasymSum}x{\isasymin}A{\isachardot}\ {\isasymSum}y{\isasymin}B{\isachardot}\ f\ x\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isasymin}A\ {\isasymtimes}\ B{\isachardot}\ f\ x\ y{\isacharparenright}%
 \end{isabelle}
 No typos, no omissions, no sweat.
 If you have not experienced that joy, read Chapter 4, \emph{Presenting
@@ -170,7 +169,6 @@
 \endisadelimML
 %
 \isatagML
-\isamarkupfalse%
 %
 \endisatagML
 {\isafoldML}%
@@ -481,7 +479,6 @@
 \endisadelimML
 %
 \isatagML
-\isamarkupfalse%
 %
 \endisatagML
 {\isafoldML}%
@@ -526,7 +523,6 @@
 \endisadelimtheory
 %
 \isatagtheory
-\isamarkupfalse%
 %
 \endisatagtheory
 {\isafoldtheory}%
diff -r ba65f3e5653c -r af174eeafba1 doc-src/LaTeXsugar/Sugar/document/isabelle.sty
--- a/doc-src/LaTeXsugar/Sugar/document/isabelle.sty	Wed Aug 31 18:46:56 2005 +0200
+++ b/doc-src/LaTeXsugar/Sugar/document/isabelle.sty	Thu Sep 01 00:45:24 2005 +0200
@@ -22,10 +22,10 @@
 \newcommand{\isamath}[1]{\emph{$#1$}}
 \newcommand{\isatext}[1]{\emph{#1}}
 \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
-\newcommand{\isactrlsub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}}
-\newcommand{\isactrlsup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}}
-\newcommand{\isactrlisub}[1]{\emph{${}\sb{\mbox{\isastylescript{#1}}}$}}
-\newcommand{\isactrlisup}[1]{\emph{${}\sp{\mbox{\isastylescript{#1}}}$}}
+\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
+\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
+\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
+\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
 \newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript}
 \newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup}
 \newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript}
@@ -89,6 +89,8 @@
 \chardef\isacharbar=`\|
 \chardef\isacharbraceright=`\}
 \chardef\isachartilde=`\~
+\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}
+\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}
 
 
 % keyword and section markup
@@ -112,8 +114,8 @@
 \newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
 \newcommand{\isaendpar}{\par\medskip}
 \newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
-\newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}}
-\newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}}
+\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
+\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
 \newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
 
 
@@ -165,6 +167,8 @@
 \renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
 \renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
 \renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
+\renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}%
+\renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}%
 }
 
 \newcommand{\isabellestylesl}{%
diff -r ba65f3e5653c -r af174eeafba1 doc-src/Locales/Locales/document/isabelle.sty
--- a/doc-src/Locales/Locales/document/isabelle.sty	Wed Aug 31 18:46:56 2005 +0200
+++ b/doc-src/Locales/Locales/document/isabelle.sty	Thu Sep 01 00:45:24 2005 +0200
@@ -114,8 +114,8 @@
 \newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
 \newcommand{\isaendpar}{\par\medskip}
 \newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
-\newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}}
-\newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}}
+\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
+\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
 \newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
 
 
diff -r ba65f3e5653c -r af174eeafba1 doc-src/TutorialI/isabelle.sty
--- a/doc-src/TutorialI/isabelle.sty	Wed Aug 31 18:46:56 2005 +0200
+++ b/doc-src/TutorialI/isabelle.sty	Thu Sep 01 00:45:24 2005 +0200
@@ -114,8 +114,8 @@
 \newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
 \newcommand{\isaendpar}{\par\medskip}
 \newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
-\newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}}
-\newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}}
+\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
+\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
 \newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
 
 
diff -r ba65f3e5653c -r af174eeafba1 doc-src/ZF/isabelle.sty
--- a/doc-src/ZF/isabelle.sty	Wed Aug 31 18:46:56 2005 +0200
+++ b/doc-src/ZF/isabelle.sty	Thu Sep 01 00:45:24 2005 +0200
@@ -114,8 +114,8 @@
 \newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
 \newcommand{\isaendpar}{\par\medskip}
 \newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
-\newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}}
-\newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}}
+\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
+\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
 \newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}