# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1234519028 0
# Node ID 13fd0a83d3c3b4fceee4778b89bbad48f9d250e6
# Parent  9b6c9d1723784d26dd47d2fa2d7fb00a3b118f29
properly handled linenumbers in ML-text and Isar-proofs

diff -r 9b6c9d172378 -r 13fd0a83d3c3 CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Fri Feb 13 01:05:31 2009 +0000
+++ b/CookBook/FirstSteps.thy	Fri Feb 13 09:57:08 2009 +0000
@@ -643,7 +643,7 @@
   the purpose of this combinator is to implement functions in a  
   ``waterfall fashion''. Consider for example the function *}
 
-ML %linenumbers{*fun inc_by_five x =
+ML %linenosgray{*fun inc_by_five x =
   x |> (fn x => x + 1)
     |> (fn x => (x, x))
     |> fst
@@ -706,7 +706,7 @@
 
  *}
 
-ML %linenumbers{*fun inc_by_three x =
+ML %linenosgray{*fun inc_by_three x =
      x |> (fn x => x + 1)
        |> tap (fn x => tracing (makestring x))
        |> (fn x => x + 2)*}
diff -r 9b6c9d172378 -r 13fd0a83d3c3 CookBook/Package/Ind_Examples.thy
--- a/CookBook/Package/Ind_Examples.thy	Fri Feb 13 01:05:31 2009 +0000
+++ b/CookBook/Package/Ind_Examples.thy	Fri Feb 13 09:57:08 2009 +0000
@@ -49,7 +49,7 @@
   (FIXME: add linenumbers to the proof below and the text above)
 *}
 
-lemma trcl_induct:
+lemma %linenos trcl_induct:
   assumes asm: "trcl R x y"
   shows "(\<And>x. P x x) \<Longrightarrow> (\<And>x y z. R x y \<Longrightarrow> P y z \<Longrightarrow> P x z) \<Longrightarrow> P x y"
 apply(atomize (full))
diff -r 9b6c9d172378 -r 13fd0a83d3c3 CookBook/Parsing.thy
--- a/CookBook/Parsing.thy	Fri Feb 13 01:05:31 2009 +0000
+++ b/CookBook/Parsing.thy	Fri Feb 13 09:57:08 2009 +0000
@@ -834,7 +834,7 @@
   we set the kind indicator to @{ML thy_goal in OuterKeyword}.
 *}
 
-ML%linenumbers{*let
+ML%linenosgray{*let
   fun set_up_thm str ctxt =
     let
       val prop = Syntax.read_prop ctxt str
diff -r 9b6c9d172378 -r 13fd0a83d3c3 CookBook/Readme.thy
--- a/CookBook/Readme.thy	Fri Feb 13 01:05:31 2009 +0000
+++ b/CookBook/Readme.thy	Fri Feb 13 09:57:08 2009 +0000
@@ -146,8 +146,9 @@
   the tutorial, however, ensures that the environment markers are not printed.
 
   \item Line numbers can be printed using 
-  \isacommand{ML} \isa{\%linenumbers}~@{text "\<verbopen> \<dots> \<verbclose>"}
-  for ML-code or \isacommand{lemma} \isa{\%linenumbers} @{text "..."} for proofs.
+  \isacommand{ML} \isa{\%linenos}~@{text "\<verbopen> \<dots> \<verbclose>"}
+  for ML-code or \isacommand{lemma} \isa{\%linenos} @{text "..."} for proofs. The
+  tag is \isa{\%linenosgray} when the numbered text should be gray. 
 
   \end{itemize}
 
diff -r 9b6c9d172378 -r 13fd0a83d3c3 CookBook/Recipes/Antiquotes.thy
--- a/CookBook/Recipes/Antiquotes.thy	Fri Feb 13 01:05:31 2009 +0000
+++ b/CookBook/Recipes/Antiquotes.thy	Fri Feb 13 09:57:08 2009 +0000
@@ -33,7 +33,7 @@
 
 *}
 
-ML%linenumbers{*fun ml_val code_txt = "val _ = " ^ code_txt
+ML%linenosgray{*fun ml_val code_txt = "val _ = " ^ code_txt
 
 fun output_ml src ctxt code_txt =
   (ML_Context.eval_in (SOME ctxt) false Position.none (ml_val code_txt); 
@@ -67,7 +67,7 @@
   can improve the code above slightly by writing 
 *}
 
-ML%linenumbers{*fun output_ml src ctxt (code_txt,pos) =
+ML%linenosgray{*fun output_ml src ctxt (code_txt,pos) =
   (ML_Context.eval_in (SOME ctxt) false pos (ml_val code_txt);
   ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt 
                                             (space_explode "\n" code_txt))
diff -r 9b6c9d172378 -r 13fd0a83d3c3 CookBook/Tactical.thy
--- a/CookBook/Tactical.thy	Fri Feb 13 01:05:31 2009 +0000
+++ b/CookBook/Tactical.thy	Fri Feb 13 09:57:08 2009 +0000
@@ -666,7 +666,7 @@
   of the tactic is as follows.\label{tac:selecttac}
 *}
 
-ML %linenumbers{*fun select_tac (t,i) =
+ML %linenosgray{*fun select_tac (t,i) =
   case t of
      @{term "Trueprop"} $ t' => select_tac (t',i)
    | @{term "op \<Longrightarrow>"} $ _ $ t' => select_tac (t',i)
diff -r 9b6c9d172378 -r 13fd0a83d3c3 CookBook/document/root.tex
--- a/CookBook/document/root.tex	Fri Feb 13 01:05:31 2009 +0000
+++ b/CookBook/document/root.tex	Fri Feb 13 09:57:08 2009 +0000
@@ -84,9 +84,14 @@
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % for code that has line numbers
-\isakeeptag{linenumbers}
-\renewcommand{\isataglinenumbers}{\begin{vanishML}\begin{graybox}\resetlinenumber\internallinenumbers}
-\renewcommand{\endisataglinenumbers}{\par\end{graybox}\end{vanishML}}
+\isakeeptag{linenos}
+\renewcommand{\isataglinenos}{\begingroup\resetlinenumber\internallinenumbers}
+\renewcommand{\endisataglinenos}{\par\nolinenumbers\endgroup}
+
+% should only be used in ML code
+\isakeeptag{linenosgray}
+\renewcommand{\isataglinenosgray}{\begin{vanishML}\begin{graybox}\resetlinenumber\internallinenumbers}
+\renewcommand{\endisataglinenosgray}{\par\nolinenumbers\end{graybox}\end{vanishML}}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \renewenvironment{isabelle}
diff -r 9b6c9d172378 -r 13fd0a83d3c3 cookbook.pdf
Binary file cookbook.pdf has changed