author | wenzelm |
Thu, 06 Mar 2014 22:15:01 +0100 | |
changeset 55965 | 0c2c61a87a7d |
parent 55837 | 154855d9a564 |
child 55997 | 9dc5ce83202c |
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 |
||
50 |
(* ML text *) |
|
51 |
||
52 |
local |
|
53 |
||
55831 | 54 |
val ml_toks = ML_Lex.read Position.none; |
21375 | 55 |
|
55831 | 56 |
fun ml_val (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks ");" |
57 |
| ml_val (toks1, toks2) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : " @ toks2 @ ml_toks ");"; |
|
58 |
||
59 |
fun ml_op (toks1, []) = ml_toks "fn _ => (op " @ toks1 @ ml_toks ");" |
|
60 |
| ml_op (toks1, toks2) = ml_toks "fn _ => (op " @ toks1 @ ml_toks " : " @ toks2 @ ml_toks ");"; |
|
46261 | 61 |
|
55831 | 62 |
fun ml_type (toks1, []) = ml_toks "val _ = NONE : (" @ toks1 @ ml_toks ") option;" |
63 |
| ml_type (toks1, toks2) = |
|
64 |
ml_toks "val _ = [NONE : (" @ toks1 @ ml_toks ") option, NONE : (" @ |
|
65 |
toks2 @ ml_toks ") option];"; |
|
22289 | 66 |
|
55837 | 67 |
fun ml_exception (toks1, []) = ml_toks "fn _ => (" @ toks1 @ ml_toks " : exn);" |
68 |
| ml_exception (toks1, toks2) = |
|
55831 | 69 |
ml_toks "fn _ => (" @ toks1 @ ml_toks " : " @ toks2 @ ml_toks " -> exn);"; |
22289 | 70 |
|
55831 | 71 |
fun ml_structure (toks, _) = |
72 |
ml_toks "functor XXX() = struct structure XX = " @ toks @ ml_toks " end;"; |
|
21375 | 73 |
|
55831 | 74 |
fun ml_functor (Antiquote.Text tok :: _, _) = |
75 |
ml_toks "ML_Env.check_functor " @ ml_toks (ML_Syntax.print_string (ML_Lex.content_of tok)) |
|
76 |
| ml_functor _ = raise Fail "Bad ML functor specification"; |
|
21375 | 77 |
|
39869
c269f6bd0a1f
more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
wenzelm
parents:
39858
diff
changeset
|
78 |
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
|
79 |
|
c269f6bd0a1f
more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
wenzelm
parents:
39858
diff
changeset
|
80 |
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
|
81 |
(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
|
82 |
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
|
83 |
| _ => 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
|
84 |
|
55831 | 85 |
fun prep_ml source = |
86 |
(#1 (Symbol_Pos.source_content source), ML_Lex.read_source source); |
|
87 |
||
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37198
diff
changeset
|
88 |
fun index_ml name kind ml = Thy_Output.antiquotation name |
55831 | 89 |
(Scan.lift (Args.name_source_position -- Scan.option (Args.colon |-- Args.name_source_position))) |
90 |
(fn {context = ctxt, ...} => fn (source1, opt_source2) => |
|
30394 | 91 |
let |
55831 | 92 |
val (txt1, toks1) = prep_ml source1; |
93 |
val (txt2, toks2) = |
|
94 |
(case opt_source2 of |
|
95 |
SOME source => prep_ml source |
|
96 |
| NONE => ("", [])); |
|
97 |
||
30394 | 98 |
val txt = |
99 |
if txt2 = "" then txt1 |
|
100 |
else if kind = "type" then txt1 ^ " = " ^ txt2 |
|
101 |
else if kind = "exception" then txt1 ^ " of " ^ txt2 |
|
50239 | 102 |
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
|
103 |
then txt1 ^ ": " ^ txt2 |
39858
5be7a57c3b4e
more robust treatment of symbolic indentifiers (which may contain colons);
wenzelm
parents:
39829
diff
changeset
|
104 |
else txt1 ^ " : " ^ txt2; |
30394 | 105 |
val txt' = if kind = "" then txt else kind ^ " " ^ txt; |
55831 | 106 |
|
107 |
val _ = ML_Context.eval_in (SOME ctxt) false (#pos source1) (ml (toks1, toks2)); |
|
30394 | 108 |
val kind' = if kind = "" then "ML" else "ML " ^ kind; |
109 |
in |
|
39869
c269f6bd0a1f
more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
wenzelm
parents:
39858
diff
changeset
|
110 |
"\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^ |
30394 | 111 |
(txt' |
38767
d8da44a8dd25
proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents:
37982
diff
changeset
|
112 |
|> (if Config.get ctxt Thy_Output.quotes then quote else I) |
55831 | 113 |
|> (if Config.get ctxt Thy_Output.display |
114 |
then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
|
30394 | 115 |
else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")) |
116 |
end); |
|
26742 | 117 |
|
118 |
in |
|
21375 | 119 |
|
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
120 |
val index_ml_setup = |
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} "" ml_val #> |
46261 | 122 |
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
|
123 |
index_ml @{binding index_ML_type} "type" ml_type #> |
55837 | 124 |
index_ml @{binding index_ML_exception} "exception" ml_exception #> |
125 |
index_ml @{binding index_ML_structure} "structure" ml_structure #> |
|
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
126 |
index_ml @{binding index_ML_functor} "functor" ml_functor; |
21375 | 127 |
|
26742 | 128 |
end; |
21375 | 129 |
|
23846 | 130 |
|
30394 | 131 |
(* named theorems *) |
23846 | 132 |
|
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
133 |
val named_thms_setup = |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
134 |
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
|
135 |
(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
|
136 |
(fn {context = ctxt, ...} => |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
137 |
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
|
138 |
#> (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
|
139 |
#> (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
|
140 |
then |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
141 |
map (fn (p, name) => |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
142 |
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
|
143 |
"\\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
|
144 |
#> 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
|
145 |
#> 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
|
146 |
else |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
147 |
map (fn (p, name) => |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
148 |
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
|
149 |
"\\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
|
150 |
#> 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
|
151 |
#> enclose "\\isa{" "}")); |
26742 | 152 |
|
153 |
||
30394 | 154 |
(* theory file *) |
26742 | 155 |
|
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
156 |
val thy_file_setup = |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
157 |
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
|
158 |
(fn {context = ctxt, ...} => |
48899 | 159 |
fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name])); |
26742 | 160 |
|
26751 | 161 |
|
30394 | 162 |
(* Isabelle/Isar entities (with index) *) |
26751 | 163 |
|
164 |
local |
|
165 |
||
26894 | 166 |
fun no_check _ _ = true; |
167 |
||
53061 | 168 |
fun command_check (name, pos) = |
169 |
is_some (Keyword.command_keyword name) andalso |
|
170 |
let |
|
171 |
val markup = |
|
172 |
Outer_Syntax.scan Position.none name |
|
173 |
|> maps (Outer_Syntax.command_reports (#2 (Outer_Syntax.get_syntax ()))) |
|
174 |
|> map (snd o fst); |
|
175 |
val _ = List.app (Position.report pos) markup; |
|
176 |
in true end; |
|
177 |
||
53044 | 178 |
fun check_tool (name, pos) = |
179 |
let |
|
180 |
fun tool dir = |
|
181 |
let val path = Path.append dir (Path.basic name) |
|
182 |
in if File.exists path then SOME path else NONE end; |
|
183 |
in |
|
53045 | 184 |
(case get_first tool (Path.split (getenv "ISABELLE_TOOLS")) of |
53044 | 185 |
NONE => false |
186 |
| SOME path => (Position.report pos (Markup.path (Path.implode path)); true)) |
|
187 |
end; |
|
28237 | 188 |
|
26751 | 189 |
val arg = enclose "{" "}" o clean_string; |
190 |
||
30394 | 191 |
fun entity check markup kind index = |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37198
diff
changeset
|
192 |
Thy_Output.antiquotation |
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
193 |
(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
|
194 |
(case index of NONE => "" | SOME true => "_def" | SOME false => "_ref"))) |
53044 | 195 |
(Scan.lift (Scan.optional (Args.parens Args.name) "" -- Parse.position Args.name)) |
196 |
(fn {context = ctxt, ...} => fn (logic, (name, pos)) => |
|
30394 | 197 |
let |
198 |
val hyper_name = |
|
199 |
"{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}"; |
|
200 |
val hyper = |
|
201 |
enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #> |
|
202 |
index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}"; |
|
203 |
val idx = |
|
204 |
(case index of |
|
205 |
NONE => "" |
|
206 |
| SOME is_def => |
|
207 |
"\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name); |
|
208 |
in |
|
53044 | 209 |
if check ctxt (name, pos) then |
30394 | 210 |
idx ^ |
211 |
(Output.output name |
|
212 |
|> (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
|
213 |
|> (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
|
214 |
|> (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
|
215 |
then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
30394 | 216 |
else hyper o enclose "\\mbox{\\isa{" "}}")) |
53044 | 217 |
else error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos) |
30394 | 218 |
end); |
26897 | 219 |
|
26894 | 220 |
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
|
221 |
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
|
222 |
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
|
223 |
entity check markup kind (SOME false); |
26751 | 224 |
|
225 |
in |
|
226 |
||
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
227 |
val entity_setup = |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
228 |
entity_antiqs no_check "" "syntax" #> |
53061 | 229 |
entity_antiqs (K command_check) "isacommand" "command" #> |
53044 | 230 |
entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #> |
231 |
entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #> |
|
55742
a989bdaf8121
modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
wenzelm
parents:
54705
diff
changeset
|
232 |
entity_antiqs (can o Method.check_name) "" "method" #> |
55743 | 233 |
entity_antiqs (can o Attrib.check o Proof_Context.theory_of) "" "attribute" #> |
43564
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 "" "fact" #> |
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 "" "variable" #> |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
236 |
entity_antiqs no_check "" "case" #> |
55743 | 237 |
entity_antiqs (can o Thy_Output.check_command) "" "antiquotation" #> |
238 |
entity_antiqs (can o 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
|
239 |
entity_antiqs no_check "isatt" "setting" #> |
48578 | 240 |
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
|
241 |
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
|
242 |
entity_antiqs no_check "isatt" "executable" #> |
48602 | 243 |
entity_antiqs (K check_tool) "isatool" "tool" #> |
55743 | 244 |
entity_antiqs (can o ML_Context.check_antiq) "" Markup.ML_antiquotationN; |
26751 | 245 |
|
26742 | 246 |
end; |
26751 | 247 |
|
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
248 |
|
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
249 |
(* theory setup *) |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
250 |
|
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
251 |
val setup = |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
252 |
verbatim_setup #> |
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; |