author | wenzelm |
Wed, 12 Mar 2014 14:17:13 +0100 | |
changeset 56059 | 2390391584c2 |
parent 55997 | 9dc5ce83202c |
child 56060 | 61f319bebb7a |
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 = |
81 |
(#1 (Symbol_Pos.source_content source), ML_Lex.read_source source); |
|
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 |
|
102 |
val _ = ML_Context.eval_in (SOME ctxt) false (#pos source1) (ml (toks1, toks2)); |
|
30394 | 103 |
val kind' = if kind = "" then "ML" else "ML " ^ kind; |
104 |
in |
|
39869
c269f6bd0a1f
more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
wenzelm
parents:
39858
diff
changeset
|
105 |
"\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^ |
30394 | 106 |
(txt' |
38767
d8da44a8dd25
proper context for various Thy_Output options, via official configuration options in ML and Isar;
wenzelm
parents:
37982
diff
changeset
|
107 |
|> (if Config.get ctxt Thy_Output.quotes then quote else I) |
55831 | 108 |
|> (if Config.get ctxt Thy_Output.display |
109 |
then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" |
|
30394 | 110 |
else split_lines #> map verbatim #> space_implode "\\isasep\\isanewline%\n")) |
111 |
end); |
|
26742 | 112 |
|
113 |
in |
|
21375 | 114 |
|
56059
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
115 |
val _ = |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
116 |
Theory.setup |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
117 |
(index_ml @{binding index_ML} "" ml_val #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
118 |
index_ml @{binding index_ML_op} "infix" ml_op #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
119 |
index_ml @{binding index_ML_type} "type" ml_type #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
120 |
index_ml @{binding index_ML_exception} "exception" ml_exception #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
121 |
index_ml @{binding index_ML_structure} "structure" ml_structure #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
122 |
index_ml @{binding index_ML_functor} "functor" ml_functor); |
21375 | 123 |
|
26742 | 124 |
end; |
21375 | 125 |
|
23846 | 126 |
|
30394 | 127 |
(* named theorems *) |
23846 | 128 |
|
56059
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
129 |
val _ = |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
130 |
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
|
131 |
(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
|
132 |
(fn {context = ctxt, ...} => |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
133 |
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
|
134 |
#> (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
|
135 |
#> (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
|
136 |
then |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
137 |
map (fn (p, name) => |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
138 |
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
|
139 |
"\\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
|
140 |
#> 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
|
141 |
#> 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
|
142 |
else |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
143 |
map (fn (p, name) => |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
144 |
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
|
145 |
"\\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
|
146 |
#> space_implode "\\par\\smallskip%\n" |
56059
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
147 |
#> enclose "\\isa{" "}"))); |
26742 | 148 |
|
149 |
||
30394 | 150 |
(* theory file *) |
26742 | 151 |
|
56059
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
152 |
val _ = |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
153 |
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
|
154 |
(fn {context = ctxt, ...} => |
56059
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
155 |
fn name => (Thy_Load.check_thy Path.current name; Thy_Output.output ctxt [Pretty.str name]))); |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
156 |
|
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 |
(* Isabelle/jEdit elements *) |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
159 |
|
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
160 |
local |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
161 |
|
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
162 |
fun parse_named a (XML.Elem ((b, props), _)) = |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
163 |
(case Properties.get props "NAME" of |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
164 |
SOME name => if a = b then [name] else [] |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
165 |
| NONE => []) |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
166 |
| parse_named _ _ = []; |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
167 |
|
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
168 |
fun parse_dockables [XML.Elem (("DOCKABLES", _), body)] = maps (parse_named "DOCKABLE") body |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
169 |
| parse_dockables _ = []; |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
170 |
|
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
171 |
val jedit_actions = |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
172 |
(case XML.parse (File.read (Path.explode "~~/src/Tools/jEdit/src/actions.xml")) of |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
173 |
XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
174 |
| _ => []); |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
175 |
|
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
176 |
val jedit_dockables = |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
177 |
(case XML.parse (File.read (Path.explode "~~/src/Tools/jEdit/src/dockables.xml")) of |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
178 |
XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
179 |
| _ => []); |
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 |
val all_actions = jedit_actions @ jedit_dockables; |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
182 |
|
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
183 |
in |
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 |
fun is_action (name, pos) = member (op =) all_actions name; |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
186 |
|
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
187 |
end; |
26742 | 188 |
|
26751 | 189 |
|
30394 | 190 |
(* Isabelle/Isar entities (with index) *) |
26751 | 191 |
|
192 |
local |
|
193 |
||
26894 | 194 |
fun no_check _ _ = true; |
195 |
||
53061 | 196 |
fun command_check (name, pos) = |
197 |
is_some (Keyword.command_keyword name) andalso |
|
198 |
let |
|
199 |
val markup = |
|
200 |
Outer_Syntax.scan Position.none name |
|
201 |
|> maps (Outer_Syntax.command_reports (#2 (Outer_Syntax.get_syntax ()))) |
|
202 |
|> map (snd o fst); |
|
203 |
val _ = List.app (Position.report pos) markup; |
|
204 |
in true end; |
|
205 |
||
53044 | 206 |
fun check_tool (name, pos) = |
207 |
let |
|
208 |
fun tool dir = |
|
209 |
let val path = Path.append dir (Path.basic name) |
|
210 |
in if File.exists path then SOME path else NONE end; |
|
211 |
in |
|
53045 | 212 |
(case get_first tool (Path.split (getenv "ISABELLE_TOOLS")) of |
53044 | 213 |
NONE => false |
214 |
| SOME path => (Position.report pos (Markup.path (Path.implode path)); true)) |
|
215 |
end; |
|
28237 | 216 |
|
26751 | 217 |
val arg = enclose "{" "}" o clean_string; |
218 |
||
30394 | 219 |
fun entity check markup kind index = |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37198
diff
changeset
|
220 |
Thy_Output.antiquotation |
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
221 |
(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
|
222 |
(case index of NONE => "" | SOME true => "_def" | SOME false => "_ref"))) |
53044 | 223 |
(Scan.lift (Scan.optional (Args.parens Args.name) "" -- Parse.position Args.name)) |
224 |
(fn {context = ctxt, ...} => fn (logic, (name, pos)) => |
|
30394 | 225 |
let |
226 |
val hyper_name = |
|
227 |
"{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}"; |
|
228 |
val hyper = |
|
229 |
enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #> |
|
230 |
index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}"; |
|
231 |
val idx = |
|
232 |
(case index of |
|
233 |
NONE => "" |
|
234 |
| SOME is_def => |
|
235 |
"\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name); |
|
236 |
in |
|
53044 | 237 |
if check ctxt (name, pos) then |
30394 | 238 |
idx ^ |
239 |
(Output.output name |
|
240 |
|> (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
|
241 |
|> (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
|
242 |
|> (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
|
243 |
then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
30394 | 244 |
else hyper o enclose "\\mbox{\\isa{" "}}")) |
53044 | 245 |
else error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos) |
30394 | 246 |
end); |
26897 | 247 |
|
26894 | 248 |
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
|
249 |
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
|
250 |
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
|
251 |
entity check markup kind (SOME false); |
26751 | 252 |
|
253 |
in |
|
254 |
||
56059
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
255 |
val _ = |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
256 |
Theory.setup |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
257 |
(entity_antiqs no_check "" "syntax" #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
258 |
entity_antiqs (K command_check) "isacommand" "command" #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
259 |
entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "keyword" #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
260 |
entity_antiqs (K (Keyword.is_keyword o #1)) "isakeyword" "element" #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
261 |
entity_antiqs (can o Method.check_name) "" "method" #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
262 |
entity_antiqs (can o Attrib.check_name) "" "attribute" #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
263 |
entity_antiqs no_check "" "fact" #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
264 |
entity_antiqs no_check "" "variable" #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
265 |
entity_antiqs no_check "" "case" #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
266 |
entity_antiqs (can o Thy_Output.check_command) "" "antiquotation" #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
267 |
entity_antiqs (can o Thy_Output.check_option) "" "antiquotation option" #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
268 |
entity_antiqs no_check "isatt" "setting" #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
269 |
entity_antiqs no_check "isatt" "system option" #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
270 |
entity_antiqs no_check "" "inference" #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
271 |
entity_antiqs no_check "isatt" "executable" #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
272 |
entity_antiqs (K check_tool) "isatool" "tool" #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
273 |
entity_antiqs (can o ML_Context.check_antiq) "" Markup.ML_antiquotationN #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
274 |
entity_antiqs (K is_action) "isatt" "action"); |
26751 | 275 |
|
26742 | 276 |
end; |
26751 | 277 |
|
278 |
end; |