# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1233091347 0
# Node ID b02904872d6b2af4b880e376d641a520c37c348e
# Parent  624279d187e19af95f7e61f9418b3f6e1797074a
better handling of {* and *}

diff -r 624279d187e1 -r b02904872d6b CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Tue Jan 27 17:50:08 2009 +0000
+++ b/CookBook/FirstSteps.thy	Tue Jan 27 21:22:27 2009 +0000
@@ -30,11 +30,10 @@
 
 \begin{isabelle}
 \begin{graybox}
-\isa{\isacommand{ML}
-\isacharverbatimopen\isanewline
+\isacommand{ML}~@{text "\<verbopen>"}\isanewline
 \hspace{5mm}@{ML "3 + 4"}\isanewline
-\isacharverbatimclose\isanewline
-@{text "> 7"}\smallskip}
+@{text "\<verbclose>"}\isanewline
+@{text "> 7"}\smallskip
 \end{graybox}
 \end{isabelle}
 
@@ -43,7 +42,7 @@
   your Isabelle environment. The code inside the \isacommand{ML}-command 
   can also contain value and function bindings, and even those can be
   undone when the proof script is retracted. As mentioned earlier, we will  
-  drop the \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} 
+  drop the \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} 
   whenever we show code.
 
   Once a portion of code is relatively stable, one usually wants to 
diff -r 624279d187e1 -r b02904872d6b CookBook/Intro.thy
--- a/CookBook/Intro.thy	Tue Jan 27 17:50:08 2009 +0000
+++ b/CookBook/Intro.thy	Tue Jan 27 21:22:27 2009 +0000
@@ -71,18 +71,16 @@
 
   \begin{isabelle}
   \begin{graybox}
-  \isa{\isacommand{ML}
-  \isacharverbatimopen\isanewline
+  \isacommand{ML}~@{text "\<verbopen>"}\isanewline
   \hspace{5mm}@{ML "3 + 4"}\isanewline
-  \isacharverbatimclose}
+  @{text "\<verbclose>"}
   \end{graybox}
   \end{isabelle}
   
   This corresponds to how code can be processed inside the interactive
   environment of Isabelle. It is therefore easy to experiment with the code
   (which by the way is highly recommended). However, for better readability we
-  will drop the enclosing \isacommand{ML} \isa{\isacharverbatimopen \ldots
-  \isacharverbatimclose} and just write
+  will drop the enclosing \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"} and just write
 
 
   @{ML [display,gray] "3 + 4"}
diff -r 624279d187e1 -r b02904872d6b CookBook/Parsing.thy
--- a/CookBook/Parsing.thy	Tue Jan 27 17:50:08 2009 +0000
+++ b/CookBook/Parsing.thy	Tue Jan 27 21:22:27 2009 +0000
@@ -597,7 +597,7 @@
   \isacommand{theory}~@{text Command}\\
   \isacommand{imports}~@{text Main}\\
   \isacommand{begin}\\
-  \isacommand{ML}~\isa{\isacharverbatimopen}\\
+  \isacommand{ML}~@{text "\<verbopen>"}\\
   @{ML
 "let
   val do_nothing = Scan.succeed (Toplevel.theory I)
@@ -605,7 +605,7 @@
 in
   OuterSyntax.command \"foobar\" \"description of foobar\" kind do_nothing
 end"}\\
-  \isa{\isacharverbatimclose}\\
+  @{text "\<verbclose>"}\\
   \isacommand{end}
   \end{graybox}
   \caption{\small The file @{text "Command.thy"} is necessary for generating a log 
diff -r 624279d187e1 -r b02904872d6b CookBook/Readme.thy
--- a/CookBook/Readme.thy	Tue Jan 27 17:50:08 2009 +0000
+++ b/CookBook/Readme.thy	Tue Jan 27 21:22:27 2009 +0000
@@ -143,12 +143,12 @@
 
 
   \item Functions and value bindings cannot be defined inside antiquotations; they need
-  to be included inside \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose}
+  to be included inside \isacommand{ML}~@{text "\<verbopen> \<dots> \<verbclose>"}
   environments. In this way they are also checked by the compiler. Some \LaTeX-hack in 
   the Cookbook, however, ensures that the environment markers are not printed.
 
   \item Line numbers can be printed using 
-  \isacommand{ML} \isa{\%linenumbers} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} 
+  \isacommand{ML} \isa{\%linenumbers}~@{text "\<verbopen> \<dots> \<verbclose>"}
   for ML-code or \isacommand{lemma} \isa{\%linenumbers} @{text "..."} for proofs.
 
   \end{itemize}
diff -r 624279d187e1 -r b02904872d6b CookBook/document/root.tex
--- a/CookBook/document/root.tex	Tue Jan 27 17:50:08 2009 +0000
+++ b/CookBook/document/root.tex	Tue Jan 27 21:22:27 2009 +0000
@@ -85,6 +85,12 @@
 \renewenvironment{isabelle}
 {\begin{trivlist}\begin{isabellebody}\small\item\relax}
 {\end{isabellebody}\end{trivlist}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% for {*  *} in antiquotations
+\newcommand{\isasymverbopen}{\isacharverbatimopen}
+\newcommand{\isasymverbclose}{\isacharverbatimclose}
+
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{document}
 
diff -r 624279d187e1 -r b02904872d6b cookbook.pdf
Binary file cookbook.pdf has changed