1.1 --- a/doc-src/antiquote_setup.ML	Sat Apr 26 08:49:31 2008 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Sat Apr 26 13:20:16 2008 +0200
     1.3 @@ -13,6 +13,9 @@
     1.4  
     1.5  (* misc utils *)
     1.6  
     1.7 +val clean_string =
     1.8 +  translate_string (fn "_" => "-" | ">" => "$>$" | "#" => "\\#" | c => c);
     1.9 +
    1.10  val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
    1.11  
    1.12  fun tweak_line s =
    1.13 @@ -60,12 +63,11 @@
    1.14      val _ = writeln (ml (txt1, txt2));
    1.15      val _ = ML_Context.eval_in (SOME (Context.Proof ctxt)) false Position.none (ml (txt1, txt2));
    1.16    in
    1.17 -    "\\indexml" ^ kind ^ enclose "{" "}"
    1.18 -      (translate_string (fn "_" => "-" | ">" => "$>$" | "#" => "\\#" | c => c) txt1) ^
    1.19 +    "\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^
    1.20      ((if ! O.source then str_of_source src else txt')
    1.21      |> (if ! O.quotes then quote else I)
    1.22      |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
    1.23 -    else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
    1.24 +        else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
    1.25    end;
    1.26  
    1.27  fun output_ml ctxt src =
    1.28 @@ -115,7 +117,7 @@
    1.29  
    1.30  val _ = O.add_commands
    1.31   [("named_thms", O.args (Scan.repeat (Attrib.thm --
    1.32 -      Scan.lift (Args.$$$ "(" |-- Args.name --| Args.$$$ ")"))) output_named_thms)];
    1.33 +      Scan.lift (Args.parens Args.name))) output_named_thms)];
    1.34  
    1.35  end;
    1.36  
    1.37 @@ -126,4 +128,47 @@
    1.38   [("thy_file", O.args (Scan.lift Args.name) (O.output (fn _ => fn name =>
    1.39        (ThyLoad.check_thy Path.current name; Pretty.str name))))];
    1.40  
    1.41 +
    1.42 +(* Isar entities (with index) *)
    1.43 +
    1.44 +local
    1.45 +
    1.46 +val arg = enclose "{" "}" o clean_string;
    1.47 +
    1.48 +fun output_entity index kind src ctxt (logic, name) =
    1.49 +  (case index of
    1.50 +    NONE => ""
    1.51 +  | SOME is_def =>
    1.52 +      "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name)
    1.53 +  ^
    1.54 +  (Output.output (if ! O.source then str_of_source src else name)
    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 enclose "\\isa{" "}"));
    1.58 +
    1.59 +fun entity index kind =
    1.60 +  O.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
    1.61 +    (output_entity index kind);
    1.62 +    
    1.63 +fun entity_antiqs kind =
    1.64 + [(kind, entity NONE kind),
    1.65 +  (kind ^ "_def", entity (SOME true) kind), 
    1.66 +  (kind ^ "_ref", entity (SOME false) kind)];
    1.67 +
    1.68 +in
    1.69 +
    1.70 +val _ = O.add_commands
    1.71 + (entity_antiqs "syntax" @
    1.72 +  entity_antiqs "command" @
    1.73 +  entity_antiqs "keyword" @
    1.74 +  entity_antiqs "element" @
    1.75 +  entity_antiqs "method" @
    1.76 +  entity_antiqs "attribute" @
    1.77 +  entity_antiqs "fact" @
    1.78 +  entity_antiqs "term" @
    1.79 +  entity_antiqs "case" @
    1.80 +  entity_antiqs "antiquotation");
    1.81 +
    1.82  end;
    1.83 +
    1.84 +end;