# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1237289194 -3600
# Node ID 4d0e2edd476d2c60844e8cea04b0f2aa4c9e691e
# Parent  5baaabe1ab9206f4ff41606e4f859c647c793f95
added hyperlinks for every file pointer

diff -r 5baaabe1ab92 -r 4d0e2edd476d CookBook/Appendix.thy
--- a/CookBook/Appendix.thy	Tue Mar 17 11:47:01 2009 +0100
+++ b/CookBook/Appendix.thy	Tue Mar 17 12:26:34 2009 +0100
@@ -3,6 +3,7 @@
 imports Main
 begin
 
+
 text {* \appendix *}
 
 
diff -r 5baaabe1ab92 -r 4d0e2edd476d CookBook/Intro.thy
--- a/CookBook/Intro.thy	Tue Mar 17 11:47:01 2009 +0100
+++ b/CookBook/Intro.thy	Tue Mar 17 12:26:34 2009 +0100
@@ -109,6 +109,10 @@
   Further information or pointers to files.
   \end{readmore}
 
+  The pointers to Isabelle files are hyperlinked to the tip of the Mercurial
+  repository of Isabelle at \href{http://isabelle.in.tum.de/repos/isabelle/}
+  {http://isabelle.in.tum.de/repos/isabelle/}.
+
   A few exercises are scattered around the text. Their solutions are given 
   in Appendix~\ref{ch:solutions}. Of course, you learn most, if you first try
   to solve the exercises on your own, and then look at the solutions.
diff -r 5baaabe1ab92 -r 4d0e2edd476d CookBook/antiquote_setup.ML
--- a/CookBook/antiquote_setup.ML	Tue Mar 17 11:47:01 2009 +0100
+++ b/CookBook/antiquote_setup.ML	Tue Mar 17 12:26:34 2009 +0100
@@ -80,10 +80,18 @@
 val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake
 val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both
 
+fun href_link txt =
+let 
+  val raw = Symbol.encode_raw
+  val path = "http://isabelle.in.tum.de/repos/isabelle/raw-file/tip/src/"    
+in
+ (raw "\\href{") ^ (raw path) ^ (raw txt) ^ (raw "}{") ^ txt ^ (raw "}")
+end 
+
 (* checks whether a file exists in the Isabelle distribution *)
 fun check_file_exists _ txt =
   (if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) 
-   then output_fn (string_explode "" txt)
+   then output_fn [href_link txt]
    else error ("Source file " ^ (quote txt) ^ " does not exist."))
 
 val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists
diff -r 5baaabe1ab92 -r 4d0e2edd476d cookbook.pdf
Binary file cookbook.pdf has changed