1.1 --- a/doc-src/antiquote_setup.ML	Thu May 15 12:47:19 2008 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Thu May 15 17:37:17 2008 +0200
     1.3 @@ -15,12 +15,20 @@
     1.4  
     1.5  val clean_string = translate_string
     1.6    (fn "_" => "\\_"
     1.7 +    | "<" => "$<$"
     1.8      | ">" => "$>$"
     1.9      | "#" => "\\#"
    1.10      | "{" => "\\{"
    1.11      | "}" => "\\}"
    1.12      | c => c);
    1.13  
    1.14 +fun clean_name "\\<dots>" = "dots"
    1.15 +  | clean_name ".." = "ddot"
    1.16 +  | clean_name "." = "dot"
    1.17 +  | clean_name "{" = "braceleft"
    1.18 +  | clean_name "}" = "braceright"
    1.19 +  | clean_name s = s;
    1.20 +
    1.21  val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
    1.22  
    1.23  fun tweak_line s =
    1.24 @@ -147,26 +155,34 @@
    1.25  val arg = enclose "{" "}" o clean_string;
    1.26  
    1.27  fun output_entity check markup index kind ctxt (logic, name) =
    1.28 -  if check ctxt name then
    1.29 -    (case index of
    1.30 -      NONE => ""
    1.31 -    | SOME is_def =>
    1.32 -        "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name)
    1.33 -    ^
    1.34 -    (Output.output name
    1.35 -      |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")                                    
    1.36 -      |> (if ! O.quotes then quote else I)
    1.37 -      |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    1.38 -          else enclose "\\mbox{\\isa{" "}}"))
    1.39 -  else error ("Undefined " ^ kind ^ " " ^ quote name);
    1.40 +  let
    1.41 +    val hyper_name = "{" ^ NameSpace.append kind (NameSpace.append logic (clean_name name)) ^ "}";
    1.42 +    val hyper =
    1.43 +      enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #>
    1.44 +      index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}";
    1.45 +    val idx =
    1.46 +      (case index of
    1.47 +        NONE => ""
    1.48 +      | SOME is_def =>
    1.49 +          "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name);
    1.50 +  in
    1.51 +    if check ctxt name then
    1.52 +      idx ^
    1.53 +      (Output.output name
    1.54 +        |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
    1.55 +        |> (if ! O.quotes then quote else I)
    1.56 +        |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
    1.57 +            else hyper o enclose "\\mbox{\\isa{" "}}"))
    1.58 +    else error ("Undefined " ^ kind ^ " " ^ quote name)
    1.59 +  end;
    1.60  
    1.61  fun entity check markup index kind =
    1.62    O.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
    1.63      (K (output_entity check markup index kind));
    1.64 -    
    1.65 +
    1.66  fun entity_antiqs check markup kind =
    1.67   [(kind, entity check markup NONE kind),
    1.68 -  (kind ^ "_def", entity check markup (SOME true) kind), 
    1.69 +  (kind ^ "_def", entity check markup (SOME true) kind),
    1.70    (kind ^ "_ref", entity check markup (SOME false) kind)];
    1.71  
    1.72  in