# HG changeset patch
# User wenzelm
# Date 1209208816 -7200
# Node ID 2b97ea3130c291a603fcbd95c54bc566ecb7c7e6
# Parent  b53db47a43b4685b6f38854eaca404d700ddfed0
added setup for Isar entities;
tuned;

diff -r b53db47a43b4 -r 2b97ea3130c2 doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Sat Apr 26 08:49:31 2008 +0200
+++ b/doc-src/antiquote_setup.ML	Sat Apr 26 13:20:16 2008 +0200
@@ -13,6 +13,9 @@
 
 (* misc utils *)
 
+val clean_string =
+  translate_string (fn "_" => "-" | ">" => "$>$" | "#" => "\\#" | c => c);
+
 val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
 
 fun tweak_line s =
@@ -60,12 +63,11 @@
     val _ = writeln (ml (txt1, txt2));
     val _ = ML_Context.eval_in (SOME (Context.Proof ctxt)) false Position.none (ml (txt1, txt2));
   in
-    "\\indexml" ^ kind ^ enclose "{" "}"
-      (translate_string (fn "_" => "-" | ">" => "$>$" | "#" => "\\#" | c => c) txt1) ^
+    "\\indexml" ^ kind ^ enclose "{" "}" (clean_string txt1) ^
     ((if ! O.source then str_of_source src else txt')
     |> (if ! O.quotes then quote else I)
     |> (if ! O.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
-    else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
+        else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))
   end;
 
 fun output_ml ctxt src =
@@ -115,7 +117,7 @@
 
 val _ = O.add_commands
  [("named_thms", O.args (Scan.repeat (Attrib.thm --
-      Scan.lift (Args.$$$ "(" |-- Args.name --| Args.$$$ ")"))) output_named_thms)];
+      Scan.lift (Args.parens Args.name))) output_named_thms)];
 
 end;
 
@@ -126,4 +128,47 @@
  [("thy_file", O.args (Scan.lift Args.name) (O.output (fn _ => fn name =>
       (ThyLoad.check_thy Path.current name; Pretty.str name))))];
 
+
+(* Isar entities (with index) *)
+
+local
+
+val arg = enclose "{" "}" o clean_string;
+
+fun output_entity index kind src ctxt (logic, name) =
+  (case index of
+    NONE => ""
+  | SOME is_def =>
+      "\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name)
+  ^
+  (Output.output (if ! O.source then str_of_source src else name)
+    |> (if ! O.quotes then quote else I)
+    |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
+        else enclose "\\isa{" "}"));
+
+fun entity index kind =
+  O.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
+    (output_entity index kind);
+    
+fun entity_antiqs kind =
+ [(kind, entity NONE kind),
+  (kind ^ "_def", entity (SOME true) kind), 
+  (kind ^ "_ref", entity (SOME false) kind)];
+
+in
+
+val _ = O.add_commands
+ (entity_antiqs "syntax" @
+  entity_antiqs "command" @
+  entity_antiqs "keyword" @
+  entity_antiqs "element" @
+  entity_antiqs "method" @
+  entity_antiqs "attribute" @
+  entity_antiqs "fact" @
+  entity_antiqs "term" @
+  entity_antiqs "case" @
+  entity_antiqs "antiquotation");
+
 end;
+
+end;