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))