author | wenzelm |
Sat, 05 Apr 2014 15:03:40 +0200 | |
changeset 56421 | 1ffd7eaa778b |
parent 56304 | 40274e4f5ebf |
child 56467 | 8d7d6f17c6a7 |
permissions | -rw-r--r-- |
48985 | 1 |
(* Title: Doc/antiquote_setup.ML |
21375 | 2 |
Author: Makarius |
3 |
||
26742 | 4 |
Auxiliary antiquotations for the Isabelle manuals. |
21375 | 5 |
*) |
6 |
||
56059
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
7 |
structure Antiquote_Setup: sig end = |
26742 | 8 |
struct |
21375 | 9 |
|
26742 | 10 |
(* misc utils *) |
11 |
||
29736
ec3fc818b82e
clean_string/clean_name: proper treatment of \<dash>;
wenzelm
parents:
29726
diff
changeset
|
12 |
fun translate f = Symbol.explode #> map f #> implode; |
ec3fc818b82e
clean_string/clean_name: proper treatment of \<dash>;
wenzelm
parents:
29726
diff
changeset
|
13 |
|
ec3fc818b82e
clean_string/clean_name: proper treatment of \<dash>;
wenzelm
parents:
29726
diff
changeset
|
14 |
val clean_string = translate |
26853
52cb0e965041
clean_string: map "_" to "\\_" (best used with underscore.sty);
wenzelm
parents:
26843
diff
changeset
|
15 |
(fn "_" => "\\_" |
30120
aaa4667285c8
uniform treatment of ML indexing, using general \indexdef macro for formal Isabelle/Isar entities;
wenzelm
parents:
29736
diff
changeset
|
16 |
| "#" => "\\#" |
52408 | 17 |
| "$" => "\\$" |
18 |
| "%" => "\\%" |
|
26897 | 19 |
| "<" => "$<$" |
26768 | 20 |
| ">" => "$>$" |
21 |
| "{" => "\\{" |
|
30120
aaa4667285c8
uniform treatment of ML indexing, using general \indexdef macro for formal Isabelle/Isar entities;
wenzelm
parents:
29736
diff
changeset
|
22 |
| "|" => "$\\mid$" |
26768 | 23 |
| "}" => "\\}" |
42666 | 24 |
| "\<hyphen>" => "-" |
26768 | 25 |
| c => c); |
26751 | 26 |
|
31546 | 27 |
fun clean_name "\<dots>" = "dots" |
26897 | 28 |
| clean_name ".." = "ddot" |
29 |
| clean_name "." = "dot" |
|
26910 | 30 |
| clean_name "_" = "underscore" |
26897 | 31 |
| clean_name "{" = "braceleft" |
32 |
| clean_name "}" = "braceright" |
|
42666 | 33 |
| clean_name s = s |> translate (fn "_" => "-" | "\<hyphen>" => "-" | c => c); |
26897 | 34 |
|
26742 | 35 |
|
36 |
(* verbatim text *) |
|
37 |
||
38 |
val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|"; |
|
39 |
||
56059
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
40 |
val _ = |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
41 |
Theory.setup (Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.name) |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
42 |
(K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n"))); |
26742 | 43 |
|
44 |
||
45 |
(* ML text *) |
|
46 |
||
47 |
local |
|
48 |
||
55831 | 49 |
val ml_toks = ML_Lex.read Position.none; |
21375 | 50 |
|
55831 | 51 |
fun ml_val (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks ");" |
52 |
| ml_val (toks1, toks2) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : " @ toks2 @ ml_toks ");"; |
|
53 |
||
54 |
fun ml_op (toks1, []) = ml_toks "fn _ => (op " @ toks1 @ ml_toks ");" |
|
55 |
| ml_op (toks1, toks2) = ml_toks "fn _ => (op " @ toks1 @ ml_toks " : " @ toks2 @ ml_toks ");"; |
|
46261 | 56 |
|
55831 | 57 |
fun ml_type (toks1, []) = ml_toks "val _ = NONE : (" @ toks1 @ ml_toks ") option;" |
58 |
| ml_type (toks1, toks2) = |
|
59 |
ml_toks "val _ = [NONE : (" @ toks1 @ ml_toks ") option, NONE : (" @ |
|
60 |
toks2 @ ml_toks ") option];"; |
|
22289 | 61 |
|
55837 | 62 |
fun ml_exception (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : exn);" |
63 |
| ml_exception (toks1, toks2) = |
|
55831 | 64 |
ml_toks "fn _ => (" @ toks1 @ ml_toks " : " @ toks2 @ ml_toks " -> exn);"; |
22289 | 65 |
|
55831 | 66 |
fun ml_structure (toks, _) = |
67 |
ml_toks "functor XXX() = struct structure XX = " @ toks @ ml_toks " end;"; |
|
21375 | 68 |
|
55831 | 69 |
fun ml_functor (Antiquote.Text tok :: _, _) = |
70 |
ml_toks "ML_Env.check_functor " @ ml_toks (ML_Syntax.print_string (ML_Lex.content_of tok)) |
|
71 |
| ml_functor _ = raise Fail "Bad ML functor specification"; |
|
21375 | 72 |
|
39869
c269f6bd0a1f
more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
wenzelm
parents:
39858
diff
changeset
|
73 |
val is_name = ML_Lex.kind_of #> (fn kind => kind = ML_Lex.Ident orelse kind = ML_Lex.LongIdent); |
c269f6bd0a1f
more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
wenzelm
parents:
39858
diff
changeset
|
74 |
|
c269f6bd0a1f
more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
wenzelm
parents:
39858
diff
changeset
|
75 |
fun ml_name txt = |
c269f6bd0a1f
more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
wenzelm
parents:
39858
diff
changeset
|
76 |
(case filter is_name (ML_Lex.tokenize txt) of |
c269f6bd0a1f
more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
wenzelm
parents:
39858
diff
changeset
|
77 |
toks as [_] => ML_Lex.flatten toks |
c269f6bd0a1f
more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
wenzelm
parents:
39858
diff
changeset
|
78 |
| _ => error ("Single ML name expected in input: " ^ quote txt)); |
c269f6bd0a1f
more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
wenzelm
parents:
39858
diff
changeset
|
79 |
|
55831 | 80 |
fun prep_ml source = |
56278
2576d3a40ed6
separate tokenization and language context for SML: no symbols, no antiquotes;
wenzelm
parents:
56275
diff
changeset
|
81 |
(#1 (Symbol_Pos.source_content source), ML_Lex.read_source false source); |
55831 | 82 |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37198
diff
changeset
|
83 |
fun index_ml name kind ml = Thy_Output.antiquotation name |
55831 | 84 |
(Scan.lift (Args.name_source_position -- Scan.option (Args.colon |-- Args.name_source_position))) |
85 |
(fn {context = ctxt, ...} => fn (source1, opt_source2) => |
|
30394 | 86 |
let |
55831 | 87 |
val (txt1, toks1) = prep_ml source1; |
88 |
val (txt2, toks2) = |
|
89 |
(case opt_source2 of |
|
90 |
SOME source => prep_ml source |
|
91 |
| NONE => ("", [])); |
|
92 |
||
30394 | 93 |
val txt = |
94 |
if txt2 = "" then txt1 |
|
95 |
else if kind = "type" then txt1 ^ " = " ^ txt2 |
|
96 |
else if kind = "exception" then txt1 ^ " of " ^ txt2 |
|
50239 | 97 |
else if Symbol_Pos.is_identifier (Long_Name.base_name (ml_name txt1)) |
42290
b1f544c84040
discontinued special treatment of structure Lexicon;
wenzelm
parents:
40801
diff
changeset
|
98 |
then txt1 ^ ": " ^ txt2 |
39858
5be7a57c3b4e
more robust treatment of symbolic indentifiers (which may contain colons);
wenzelm
parents:
39829
diff
changeset
|
99 |
else txt1 ^ " : " ^ txt2; |
30394 | 100 |
val txt' = if kind = "" then txt else kind ^ " " ^ txt; |
55831 | 101 |
|
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56208
diff
changeset
|
102 |
val _ = |
56304
40274e4f5ebf
redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands);
wenzelm
parents:
56294
diff
changeset
|
103 |
ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (#pos source1) (ml (toks1, toks2)); |
30394 | 104 |
val kind' = if kind = "" then "ML" else "ML " ^ kind; |
105 |
in |
|
39869
c269f6bd0a1f
more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
wenzelm
parents:
39858
diff
changeset
|
106 |
"\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^ |
30394 | 107 |
(txt' |
38767
d8da44a8dd25
proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents:
37982
diff
changeset
|
108 |
|> (if Config.get ctxt Thy_Output.quotes then quote else I) |
55831 | 109 |
|> (if Config.get ctxt Thy_Output.display |
110 |
then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
|
30394 | 111 |
else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")) |
112 |
end); |
|
26742 | 113 |
|
114 |
in |
|
21375 | 115 |
|
56059
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
116 |
val _ = |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
117 |
Theory.setup |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
118 |
(index_ml @{binding index_ML} "" ml_val #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
119 |
index_ml @{binding index_ML_op} "infix" ml_op #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
120 |
index_ml @{binding index_ML_type} "type" ml_type #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
121 |
index_ml @{binding index_ML_exception} "exception" ml_exception #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
122 |
index_ml @{binding index_ML_structure} "structure" ml_structure #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
123 |
index_ml @{binding index_ML_functor} "functor" ml_functor); |
21375 | 124 |
|
26742 | 125 |
end; |
21375 | 126 |
|
23846 | 127 |
|
30394 | 128 |
(* named theorems *) |
23846 | 129 |
|
56059
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
130 |
val _ = |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
131 |
Theory.setup (Thy_Output.antiquotation @{binding named_thms} |
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
132 |
(Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name))) |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
133 |
(fn {context = ctxt, ...} => |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
134 |
map (apfst (Thy_Output.pretty_thm ctxt)) |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
135 |
#> (if Config.get ctxt Thy_Output.quotes then map (apfst Pretty.quote) else I) |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
136 |
#> (if Config.get ctxt Thy_Output.display |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
137 |
then |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
138 |
map (fn (p, name) => |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
139 |
Output.output (Pretty.string_of (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^ |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
140 |
"\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}") |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
141 |
#> space_implode "\\par\\smallskip%\n" |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
142 |
#> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
143 |
else |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
144 |
map (fn (p, name) => |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
145 |
Output.output (Pretty.str_of p) ^ |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
146 |
"\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}") |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
147 |
#> space_implode "\\par\\smallskip%\n" |
56059
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
148 |
#> enclose "\\isa{" "}"))); |
26742 | 149 |
|
150 |
||
30394 | 151 |
(* theory file *) |
26742 | 152 |
|
56059
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
153 |
val _ = |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
154 |
Theory.setup (Thy_Output.antiquotation @{binding thy_file} (Scan.lift Args.name) |
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
155 |
(fn {context = ctxt, ...} => |
56208 | 156 |
fn name => (Resources.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name]))); |
56059
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
157 |
|
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
158 |
|
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
159 |
(* Isabelle/jEdit elements *) |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
160 |
|
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
161 |
local |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
162 |
|
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
163 |
fun parse_named a (XML.Elem ((b, props), _)) = |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
164 |
(case Properties.get props "NAME" of |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
165 |
SOME name => if a = b then [name] else [] |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
166 |
| NONE => []) |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
167 |
| parse_named _ _ = []; |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
168 |
|
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
169 |
val jedit_actions = |
56135 | 170 |
(case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/actions.xml"}) of |
56059
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
171 |
XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
172 |
| _ => []); |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
173 |
|
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
174 |
val jedit_dockables = |
56135 | 175 |
(case XML.parse (File.read @{path "~~/src/Tools/jEdit/src/dockables.xml"}) of |
56059
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
176 |
XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
177 |
| _ => []); |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
178 |
|
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
179 |
val all_actions = jedit_actions @ jedit_dockables; |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
180 |
|
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
181 |
in |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
182 |
|
56060 | 183 |
val is_action = member (op =) all_actions; |
56059
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
184 |
|
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
185 |
end; |
26742 | 186 |
|
26751 | 187 |
|
30394 | 188 |
(* Isabelle/Isar entities (with index) *) |
26751 | 189 |
|
190 |
local |
|
191 |
||
26894 | 192 |
fun no_check _ _ = true; |
193 |
||
56294
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
56278
diff
changeset
|
194 |
fun check_command ctxt (name, pos) = |
53061 | 195 |
is_some (Keyword.command_keyword name) andalso |
196 |
let |
|
197 |
val markup = |
|
198 |
Outer_Syntax.scan Position.none name |
|
199 |
|> maps (Outer_Syntax.command_reports (#2 (Outer_Syntax.get_syntax ()))) |
|
200 |
|> map (snd o fst); |
|
56294
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
56278
diff
changeset
|
201 |
val _ = Context_Position.reports ctxt (map (pair pos) markup); |
53061 | 202 |
in true end; |
203 |
||
56294
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
56278
diff
changeset
|
204 |
fun check_tool ctxt (name, pos) = |
53044 | 205 |
let |
206 |
fun tool dir = |
|
207 |
let val path = Path.append dir (Path.basic name) |
|
208 |
in if File.exists path then SOME path else NONE end; |
|
209 |
in |
|
53045 | 210 |
(case get_first tool (Path.split (getenv "ISABELLE_TOOLS")) of |
53044 | 211 |
NONE => false |
56294
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
56278
diff
changeset
|
212 |
| SOME path => (Context_Position.report ctxt pos (Markup.path (Path.implode path)); true)) |
53044 | 213 |
end; |
28237 | 214 |
|
26751 | 215 |
val arg = enclose "{" "}" o clean_string; |
216 |
||
56185 | 217 |
fun entity check markup binding index = |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37198
diff
changeset
|
218 |
Thy_Output.antiquotation |
56185 | 219 |
(binding |> Binding.map_name (fn name => name ^ |
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
220 |
(case index of NONE => "" | SOME true => "_def" | SOME false => "_ref"))) |
53044 | 221 |
(Scan.lift (Scan.optional (Args.parens Args.name) "" -- Parse.position Args.name)) |
222 |
(fn {context = ctxt, ...} => fn (logic, (name, pos)) => |
|
30394 | 223 |
let |
56185 | 224 |
val kind = translate (fn "_" => " " | c => c) (Binding.name_of binding); |
30394 | 225 |
val hyper_name = |
226 |
"{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}"; |
|
227 |
val hyper = |
|
228 |
enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #> |
|
229 |
index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}"; |
|
230 |
val idx = |
|
231 |
(case index of |
|
232 |
NONE => "" |
|
233 |
| SOME is_def => |
|
234 |
"\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name); |
|
235 |
in |
|
53044 | 236 |
if check ctxt (name, pos) then |
30394 | 237 |
idx ^ |
238 |
(Output.output name |
|
239 |
|> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}") |
|
38767
d8da44a8dd25
proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents:
37982
diff
changeset
|
240 |
|> (if Config.get ctxt Thy_Output.quotes then quote else I) |
d8da44a8dd25
proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents:
37982
diff
changeset
|
241 |
|> (if Config.get ctxt Thy_Output.display |
d8da44a8dd25
proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents:
37982
diff
changeset
|
242 |
then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
30394 | 243 |
else hyper o enclose "\\mbox{\\isa{" "}}")) |
53044 | 244 |
else error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos) |
30394 | 245 |
end); |
26897 | 246 |
|
26894 | 247 |
fun entity_antiqs check markup kind = |
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
248 |
entity check markup kind NONE #> |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
249 |
entity check markup kind (SOME true) #> |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
250 |
entity check markup kind (SOME false); |
26751 | 251 |
|
252 |
in |
|
253 |
||
56059
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
254 |
val _ = |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
255 |
Theory.setup |
56185 | 256 |
(entity_antiqs no_check "" @{binding syntax} #> |
56294
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
56278
diff
changeset
|
257 |
entity_antiqs check_command "isacommand" @{binding command} #> |
56185 | 258 |
entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" @{binding keyword} #> |
259 |
entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" @{binding element} #> |
|
260 |
entity_antiqs (can o Method.check_name) "" @{binding method} #> |
|
261 |
entity_antiqs (can o Attrib.check_name) "" @{binding attribute} #> |
|
262 |
entity_antiqs no_check "" @{binding fact} #> |
|
263 |
entity_antiqs no_check "" @{binding variable} #> |
|
264 |
entity_antiqs no_check "" @{binding case} #> |
|
265 |
entity_antiqs (can o Thy_Output.check_command) "" @{binding antiquotation} #> |
|
266 |
entity_antiqs (can o Thy_Output.check_option) "" @{binding antiquotation_option} #> |
|
267 |
entity_antiqs no_check "isatt" @{binding setting} #> |
|
268 |
entity_antiqs no_check "isatt" @{binding system_option} #> |
|
269 |
entity_antiqs no_check "" @{binding inference} #> |
|
270 |
entity_antiqs no_check "isatt" @{binding executable} #> |
|
56294
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
56278
diff
changeset
|
271 |
entity_antiqs check_tool "isatool" @{binding tool} #> |
56185 | 272 |
entity_antiqs (can o ML_Context.check_antiquotation) "" @{binding ML_antiquotation} #> |
273 |
entity_antiqs (K (is_action o #1)) "isatt" @{binding action}); |
|
26751 | 274 |
|
26742 | 275 |
end; |
26751 | 276 |
|
277 |
end; |