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