# HG changeset patch
# User wenzelm
# Date 1236630220 -3600
# Node ID 841ce0fcbe144f6222685b8366a763dd5dbc6718
# Parent  f3103bd2b167c5ea2ceca4f79ede69c0b4d68b9a
fornal markup for antiquotation options;

diff -r f3103bd2b167 -r 841ce0fcbe14 doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Mon Mar 09 21:12:14 2009 +0100
+++ b/doc-src/antiquote_setup.ML	Mon Mar 09 21:23:40 2009 +0100
@@ -132,7 +132,8 @@
 
 fun entity check markup kind index =
   ThyOutput.antiquotation
-    (case index of NONE => kind | SOME true => kind ^ "_def" | SOME false => kind ^ "_ref")
+    (translate (fn " " => "_" | c => c) kind ^
+      (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref"))
     (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))
     (fn {context = ctxt, ...} => fn (logic, name) =>
       let
@@ -174,6 +175,7 @@
 val _ = entity_antiqs no_check "" "variable";
 val _ = entity_antiqs no_check "" "case";
 val _ = entity_antiqs (K ThyOutput.defined_command) "" "antiquotation";
+val _ = entity_antiqs (K ThyOutput.defined_option) "" "antiquotation option";
 val _ = entity_antiqs (fn _ => fn name => is_some (OS.Process.getEnv name)) "isatt" "setting";
 val _ = entity_antiqs no_check "" "inference";
 val _ = entity_antiqs no_check "isatt" "executable";