author | wenzelm |
Thu, 07 Nov 2013 13:34:04 +0100 | |
changeset 54372 | 2d61935eed4a |
parent 53061 | 417cb0f713e0 |
child 54705 | 0dff3326d12a |
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 |
||
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
7 |
signature ANTIQUOTE_SETUP = |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
8 |
sig |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
9 |
val setup: theory -> theory |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
10 |
end; |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
11 |
|
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
12 |
structure Antiquote_Setup: ANTIQUOTE_SETUP = |
26742 | 13 |
struct |
21375 | 14 |
|
26742 | 15 |
(* misc utils *) |
16 |
||
29736
ec3fc818b82e
clean_string/clean_name: proper treatment of \<dash>;
wenzelm
parents:
29726
diff
changeset
|
17 |
fun translate f = Symbol.explode #> map f #> implode; |
ec3fc818b82e
clean_string/clean_name: proper treatment of \<dash>;
wenzelm
parents:
29726
diff
changeset
|
18 |
|
ec3fc818b82e
clean_string/clean_name: proper treatment of \<dash>;
wenzelm
parents:
29726
diff
changeset
|
19 |
val clean_string = translate |
26853
52cb0e965041
clean_string: map "_" to "\\_" (best used with underscore.sty);
wenzelm
parents:
26843
diff
changeset
|
20 |
(fn "_" => "\\_" |
30120
aaa4667285c8
uniform treatment of ML indexing, using general \indexdef macro for formal Isabelle/Isar entities;
wenzelm
parents:
29736
diff
changeset
|
21 |
| "#" => "\\#" |
52408 | 22 |
| "$" => "\\$" |
23 |
| "%" => "\\%" |
|
26897 | 24 |
| "<" => "$<$" |
26768 | 25 |
| ">" => "$>$" |
26 |
| "{" => "\\{" |
|
30120
aaa4667285c8
uniform treatment of ML indexing, using general \indexdef macro for formal Isabelle/Isar entities;
wenzelm
parents:
29736
diff
changeset
|
27 |
| "|" => "$\\mid$" |
26768 | 28 |
| "}" => "\\}" |
42666 | 29 |
| "\<hyphen>" => "-" |
26768 | 30 |
| c => c); |
26751 | 31 |
|
31546 | 32 |
fun clean_name "\<dots>" = "dots" |
26897 | 33 |
| clean_name ".." = "ddot" |
34 |
| clean_name "." = "dot" |
|
26910 | 35 |
| clean_name "_" = "underscore" |
26897 | 36 |
| clean_name "{" = "braceleft" |
37 |
| clean_name "}" = "braceright" |
|
42666 | 38 |
| clean_name s = s |> translate (fn "_" => "-" | "\<hyphen>" => "-" | c => c); |
26897 | 39 |
|
26742 | 40 |
|
41 |
(* verbatim text *) |
|
42 |
||
43 |
val verbatim = space_implode "\\verb,|," o map (enclose "\\verb|" "|") o space_explode "|"; |
|
44 |
||
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
45 |
val verbatim_setup = |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
46 |
Thy_Output.antiquotation @{binding verbatim} (Scan.lift Args.name) |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
47 |
(K (split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")); |
26742 | 48 |
|
49 |
||
54372 | 50 |
(* unchecked file *) |
51 |
||
52 |
val file_unchecked_setup = |
|
53 |
Thy_Output.antiquotation @{binding file_unchecked} (Scan.lift (Parse.position Parse.path)) |
|
54 |
(fn {context = ctxt, ...} => fn (name, pos) => |
|
55 |
let |
|
56 |
val dir = Thy_Load.master_directory (Proof_Context.theory_of ctxt); |
|
57 |
val path = Path.append dir (Path.explode name); |
|
58 |
val _ = Position.report pos (Markup.path name); |
|
59 |
in |
|
60 |
space_explode "/" name |
|
61 |
|> map Thy_Output.verb_text |
|
62 |
|> space_implode (Thy_Output.verb_text "/" ^ "\\discretionary{}{}{}") |
|
63 |
end); |
|
64 |
||
65 |
||
26742 | 66 |
(* ML text *) |
67 |
||
68 |
local |
|
69 |
||
21375 | 70 |
fun ml_val (txt1, "") = "fn _ => (" ^ txt1 ^ ");" |
39858
5be7a57c3b4e
more robust treatment of symbolic indentifiers (which may contain colons);
wenzelm
parents:
39829
diff
changeset
|
71 |
| ml_val (txt1, txt2) = "fn _ => (" ^ txt1 ^ " : " ^ txt2 ^ ");"; |
21375 | 72 |
|
46261 | 73 |
fun ml_op (txt1, "") = "fn _ => (op " ^ txt1 ^ ");" |
74 |
| ml_op (txt1, txt2) = "fn _ => (op " ^ txt1 ^ " : " ^ txt2 ^ ");"; |
|
75 |
||
21375 | 76 |
fun ml_type (txt1, "") = "val _ = NONE : (" ^ txt1 ^ ") option;" |
77 |
| ml_type (txt1, txt2) = "val _ = [NONE : (" ^ txt1 ^ ") option, NONE : (" ^ txt2 ^ ") option];"; |
|
22289 | 78 |
|
39858
5be7a57c3b4e
more robust treatment of symbolic indentifiers (which may contain colons);
wenzelm
parents:
39829
diff
changeset
|
79 |
fun ml_exn (txt1, "") = "fn _ => (" ^ txt1 ^ " : exn);" |
5be7a57c3b4e
more robust treatment of symbolic indentifiers (which may contain colons);
wenzelm
parents:
39829
diff
changeset
|
80 |
| ml_exn (txt1, txt2) = "fn _ => (" ^ txt1 ^ " : " ^ txt2 ^ " -> exn);"; |
22289 | 81 |
|
30394 | 82 |
fun ml_structure (txt, _) = "functor XXX() = struct structure XX = " ^ txt ^ " end;"; |
21375 | 83 |
|
36163
823c9400eb62
proper checking of ML functors (in Poly/ML 5.2 or later);
wenzelm
parents:
31546
diff
changeset
|
84 |
fun ml_functor (txt, _) = "ML_Env.check_functor " ^ ML_Syntax.print_string txt; |
21375 | 85 |
|
39869
c269f6bd0a1f
more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
wenzelm
parents:
39858
diff
changeset
|
86 |
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
|
87 |
|
c269f6bd0a1f
more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
wenzelm
parents:
39858
diff
changeset
|
88 |
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
|
89 |
(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
|
90 |
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
|
91 |
| _ => 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
|
92 |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37198
diff
changeset
|
93 |
fun index_ml name kind ml = Thy_Output.antiquotation name |
30394 | 94 |
(Scan.lift (Args.name -- Scan.optional (Args.colon |-- Args.name) "")) |
95 |
(fn {context = ctxt, ...} => fn (txt1, txt2) => |
|
96 |
let |
|
97 |
val txt = |
|
98 |
if txt2 = "" then txt1 |
|
99 |
else if kind = "type" then txt1 ^ " = " ^ txt2 |
|
100 |
else if kind = "exception" then txt1 ^ " of " ^ txt2 |
|
50239 | 101 |
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
|
102 |
then txt1 ^ ": " ^ txt2 |
39858
5be7a57c3b4e
more robust treatment of symbolic indentifiers (which may contain colons);
wenzelm
parents:
39829
diff
changeset
|
103 |
else txt1 ^ " : " ^ txt2; |
30394 | 104 |
val txt' = if kind = "" then txt else kind ^ " " ^ txt; |
37198
3af985b10550
replaced ML_Lex.read_antiq by more concise ML_Lex.read, which includes full read/report with explicit position information;
wenzelm
parents:
36973
diff
changeset
|
105 |
val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none (ml (txt1, txt2)); (* ML_Lex.read (!?) *) |
30394 | 106 |
val kind' = if kind = "" then "ML" else "ML " ^ kind; |
107 |
in |
|
39869
c269f6bd0a1f
more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
wenzelm
parents:
39858
diff
changeset
|
108 |
"\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^ |
30394 | 109 |
(txt' |
38767
d8da44a8dd25
proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents:
37982
diff
changeset
|
110 |
|> (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
|
111 |
|> (if Config.get ctxt Thy_Output.display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
30394 | 112 |
else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")) |
113 |
end); |
|
26742 | 114 |
|
115 |
in |
|
21375 | 116 |
|
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
117 |
val index_ml_setup = |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
118 |
index_ml @{binding index_ML} "" ml_val #> |
46261 | 119 |
index_ml @{binding index_ML_op} "infix" ml_op #> |
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
120 |
index_ml @{binding index_ML_type} "type" ml_type #> |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
121 |
index_ml @{binding index_ML_exn} "exception" ml_exn #> |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
122 |
index_ml @{binding index_ML_structure} "structure" ml_structure #> |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
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 |
|
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
130 |
val named_thms_setup = |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
131 |
Thy_Output.antiquotation @{binding named_thms} |
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" |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
148 |
#> enclose "\\isa{" "}")); |
26742 | 149 |
|
150 |
||
30394 | 151 |
(* theory file *) |
26742 | 152 |
|
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
153 |
val thy_file_setup = |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
154 |
Thy_Output.antiquotation @{binding thy_file} (Scan.lift Args.name) |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
155 |
(fn {context = ctxt, ...} => |
48899 | 156 |
fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name])); |
26742 | 157 |
|
26751 | 158 |
|
30394 | 159 |
(* Isabelle/Isar entities (with index) *) |
26751 | 160 |
|
161 |
local |
|
162 |
||
26894 | 163 |
fun no_check _ _ = true; |
164 |
||
53061 | 165 |
fun command_check (name, pos) = |
166 |
is_some (Keyword.command_keyword name) andalso |
|
167 |
let |
|
168 |
val markup = |
|
169 |
Outer_Syntax.scan Position.none name |
|
170 |
|> maps (Outer_Syntax.command_reports (#2 (Outer_Syntax.get_syntax ()))) |
|
171 |
|> map (snd o fst); |
|
172 |
val _ = List.app (Position.report pos) markup; |
|
173 |
in true end; |
|
174 |
||
53044 | 175 |
fun thy_check check ctxt = can (check (Proof_Context.theory_of ctxt)); |
26894 | 176 |
|
53044 | 177 |
fun check_tool (name, pos) = |
178 |
let |
|
179 |
fun tool dir = |
|
180 |
let val path = Path.append dir (Path.basic name) |
|
181 |
in if File.exists path then SOME path else NONE end; |
|
182 |
in |
|
53045 | 183 |
(case get_first tool (Path.split (getenv "ISABELLE_TOOLS")) of |
53044 | 184 |
NONE => false |
185 |
| SOME path => (Position.report pos (Markup.path (Path.implode path)); true)) |
|
186 |
end; |
|
28237 | 187 |
|
26751 | 188 |
val arg = enclose "{" "}" o clean_string; |
189 |
||
30394 | 190 |
fun entity check markup kind index = |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37198
diff
changeset
|
191 |
Thy_Output.antiquotation |
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
192 |
(Binding.name (translate (fn " " => "_" | c => c) kind ^ |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
193 |
(case index of NONE => "" | SOME true => "_def" | SOME false => "_ref"))) |
53044 | 194 |
(Scan.lift (Scan.optional (Args.parens Args.name) "" -- Parse.position Args.name)) |
195 |
(fn {context = ctxt, ...} => fn (logic, (name, pos)) => |
|
30394 | 196 |
let |
197 |
val hyper_name = |
|
198 |
"{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}"; |
|
199 |
val hyper = |
|
200 |
enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #> |
|
201 |
index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}"; |
|
202 |
val idx = |
|
203 |
(case index of |
|
204 |
NONE => "" |
|
205 |
| SOME is_def => |
|
206 |
"\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name); |
|
207 |
in |
|
53044 | 208 |
if check ctxt (name, pos) then |
30394 | 209 |
idx ^ |
210 |
(Output.output name |
|
211 |
|> (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
|
212 |
|> (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
|
213 |
|> (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
|
214 |
then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
30394 | 215 |
else hyper o enclose "\\mbox{\\isa{" "}}")) |
53044 | 216 |
else error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos) |
30394 | 217 |
end); |
26897 | 218 |
|
26894 | 219 |
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
|
220 |
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
|
221 |
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
|
222 |
entity check markup kind (SOME false); |
26751 | 223 |
|
224 |
in |
|
225 |
||
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
226 |
val entity_setup = |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
227 |
entity_antiqs no_check "" "syntax" #> |
53061 | 228 |
entity_antiqs (K command_check) "isacommand" "command" #> |
53044 | 229 |
entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #> |
230 |
entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #> |
|
231 |
entity_antiqs (thy_check Method.check) "" "method" #> |
|
232 |
entity_antiqs (thy_check Attrib.check) "" "attribute" #> |
|
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
233 |
entity_antiqs no_check "" "fact" #> |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
234 |
entity_antiqs no_check "" "variable" #> |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
235 |
entity_antiqs no_check "" "case" #> |
53044 | 236 |
entity_antiqs (thy_check Thy_Output.check_command) "" "antiquotation" #> |
237 |
entity_antiqs (thy_check Thy_Output.check_option) "" "antiquotation option" #> |
|
48554
011cbb395d46
no_check for @{setting} antiquotations -- empty values are treated as undefined on Cygwin;
wenzelm
parents:
47825
diff
changeset
|
238 |
entity_antiqs no_check "isatt" "setting" #> |
48578 | 239 |
entity_antiqs no_check "isatt" "system option" #> |
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
240 |
entity_antiqs no_check "" "inference" #> |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
241 |
entity_antiqs no_check "isatt" "executable" #> |
48602 | 242 |
entity_antiqs (K check_tool) "isatool" "tool" #> |
53044 | 243 |
entity_antiqs (thy_check ML_Context.check_antiq) "" Markup.ML_antiquotationN; |
26751 | 244 |
|
26742 | 245 |
end; |
26751 | 246 |
|
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
247 |
|
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
248 |
(* theory setup *) |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
249 |
|
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
250 |
val setup = |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
251 |
verbatim_setup #> |
54372 | 252 |
file_unchecked_setup #> |
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
253 |
index_ml_setup #> |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
254 |
named_thms_setup #> |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
255 |
thy_file_setup #> |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
256 |
entity_setup; |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
257 |
|
26751 | 258 |
end; |