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