author | boehmes |
Mon, 29 Dec 2014 22:14:13 +0100 | |
changeset 59215 | 35c13f4995b1 |
parent 59175 | bf465f335e85 |
child 59809 | 87641097d0f3 |
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 |
(* ML text *) |
|
37 |
||
38 |
local |
|
39 |
||
59067 | 40 |
fun ml_val (toks1, []) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read ");" |
41 |
| ml_val (toks1, toks2) = |
|
42 |
ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read ");"; |
|
21375 | 43 |
|
59067 | 44 |
fun ml_op (toks1, []) = ML_Lex.read "fn _ => (op " @ toks1 @ ML_Lex.read ");" |
45 |
| ml_op (toks1, toks2) = |
|
46 |
ML_Lex.read "fn _ => (op " @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read ");"; |
|
46261 | 47 |
|
59067 | 48 |
fun ml_type (toks1, []) = ML_Lex.read "val _ = NONE : (" @ toks1 @ ML_Lex.read ") option;" |
55831 | 49 |
| ml_type (toks1, toks2) = |
59067 | 50 |
ML_Lex.read "val _ = [NONE : (" @ toks1 @ ML_Lex.read ") option, NONE : (" @ |
51 |
toks2 @ ML_Lex.read ") option];"; |
|
22289 | 52 |
|
59067 | 53 |
fun ml_exception (toks1, []) = ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : exn);" |
55837 | 54 |
| ml_exception (toks1, toks2) = |
59067 | 55 |
ML_Lex.read "fn _ => (" @ toks1 @ ML_Lex.read " : " @ toks2 @ ML_Lex.read " -> exn);"; |
22289 | 56 |
|
55831 | 57 |
fun ml_structure (toks, _) = |
59067 | 58 |
ML_Lex.read "functor XXX() = struct structure XX = " @ toks @ ML_Lex.read " end;"; |
21375 | 59 |
|
55831 | 60 |
fun ml_functor (Antiquote.Text tok :: _, _) = |
59067 | 61 |
ML_Lex.read "ML_Env.check_functor " @ |
62 |
ML_Lex.read (ML_Syntax.print_string (ML_Lex.content_of tok)) |
|
55831 | 63 |
| ml_functor _ = raise Fail "Bad ML functor specification"; |
21375 | 64 |
|
59082 | 65 |
val is_name = |
66 |
ML_Lex.kind_of #> (fn kind => kind = ML_Lex.Ident orelse kind = ML_Lex.Long_Ident); |
|
39869
c269f6bd0a1f
more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
wenzelm
parents:
39858
diff
changeset
|
67 |
|
c269f6bd0a1f
more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
wenzelm
parents:
39858
diff
changeset
|
68 |
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
|
69 |
(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
|
70 |
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
|
71 |
| _ => 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
|
72 |
|
55831 | 73 |
fun prep_ml source = |
59066 | 74 |
(Input.source_content source, ML_Lex.read_source false source); |
55831 | 75 |
|
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37198
diff
changeset
|
76 |
fun index_ml name kind ml = Thy_Output.antiquotation name |
58069
0255436b3d85
more liberal embedded "text", which includes cartouches;
wenzelm
parents:
57918
diff
changeset
|
77 |
(Scan.lift (Args.text_source_position -- Scan.option (Args.colon |-- Args.text_source_position))) |
55831 | 78 |
(fn {context = ctxt, ...} => fn (source1, opt_source2) => |
30394 | 79 |
let |
55831 | 80 |
val (txt1, toks1) = prep_ml source1; |
81 |
val (txt2, toks2) = |
|
82 |
(case opt_source2 of |
|
83 |
SOME source => prep_ml source |
|
84 |
| NONE => ("", [])); |
|
85 |
||
30394 | 86 |
val txt = |
87 |
if txt2 = "" then txt1 |
|
88 |
else if kind = "type" then txt1 ^ " = " ^ txt2 |
|
89 |
else if kind = "exception" then txt1 ^ " of " ^ txt2 |
|
50239 | 90 |
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
|
91 |
then txt1 ^ ": " ^ txt2 |
39858
5be7a57c3b4e
more robust treatment of symbolic indentifiers (which may contain colons);
wenzelm
parents:
39829
diff
changeset
|
92 |
else txt1 ^ " : " ^ txt2; |
30394 | 93 |
val txt' = if kind = "" then txt else kind ^ " " ^ txt; |
55831 | 94 |
|
59064 | 95 |
val pos = Input.pos_of source1; |
56275
600f432ab556
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
wenzelm
parents:
56208
diff
changeset
|
96 |
val _ = |
57477
c3b5cb53ea79
redundant error position, to ensure the message is attached somewhere, despite the distortion of positions due to glued tokens;
wenzelm
parents:
57334
diff
changeset
|
97 |
ML_Context.eval_in (SOME ctxt) ML_Compiler.flags pos (ml (toks1, toks2)) |
c3b5cb53ea79
redundant error position, to ensure the message is attached somewhere, despite the distortion of positions due to glued tokens;
wenzelm
parents:
57334
diff
changeset
|
98 |
handle ERROR msg => error (msg ^ Position.here pos); |
30394 | 99 |
val kind' = if kind = "" then "ML" else "ML " ^ kind; |
100 |
in |
|
39869
c269f6bd0a1f
more robust index_ML antiquotations: guess name from text (affects infixes and type constructors in particular);
wenzelm
parents:
39858
diff
changeset
|
101 |
"\\indexdef{}{" ^ kind' ^ "}{" ^ clean_string (ml_name txt1) ^ "}" ^ |
58716
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
58069
diff
changeset
|
102 |
(Thy_Output.verbatim_text ctxt txt') |
30394 | 103 |
end); |
26742 | 104 |
|
105 |
in |
|
21375 | 106 |
|
56059
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
107 |
val _ = |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
108 |
Theory.setup |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
109 |
(index_ml @{binding index_ML} "" ml_val #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
110 |
index_ml @{binding index_ML_op} "infix" ml_op #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
111 |
index_ml @{binding index_ML_type} "type" ml_type #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
112 |
index_ml @{binding index_ML_exception} "exception" ml_exception #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
113 |
index_ml @{binding index_ML_structure} "structure" ml_structure #> |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
114 |
index_ml @{binding index_ML_functor} "functor" ml_functor); |
21375 | 115 |
|
26742 | 116 |
end; |
21375 | 117 |
|
23846 | 118 |
|
30394 | 119 |
(* named theorems *) |
23846 | 120 |
|
56059
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
121 |
val _ = |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
122 |
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
|
123 |
(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
|
124 |
(fn {context = ctxt, ...} => |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
125 |
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
|
126 |
#> (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
|
127 |
#> (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
|
128 |
then |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
129 |
map (fn (p, name) => |
59175
bf465f335e85
system option "pretty_margin" is superseded by "thy_output_margin";
wenzelm
parents:
59083
diff
changeset
|
130 |
Output.output |
bf465f335e85
system option "pretty_margin" is superseded by "thy_output_margin";
wenzelm
parents:
59083
diff
changeset
|
131 |
(Thy_Output.string_of_margin ctxt |
bf465f335e85
system option "pretty_margin" is superseded by "thy_output_margin";
wenzelm
parents:
59083
diff
changeset
|
132 |
(Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^ |
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43563
diff
changeset
|
133 |
"\\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
|
134 |
#> 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
|
135 |
#> 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
|
136 |
else |
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.str_of 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" |
56059
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
141 |
#> enclose "\\isa{" "}"))); |
26742 | 142 |
|
143 |
||
30394 | 144 |
(* theory file *) |
26742 | 145 |
|
56059
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
146 |
val _ = |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
147 |
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
|
148 |
(fn {context = ctxt, ...} => |
56208 | 149 |
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
|
150 |
|
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
151 |
|
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
152 |
(* Isabelle/jEdit elements *) |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
153 |
|
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
154 |
local |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
155 |
|
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
156 |
fun parse_named a (XML.Elem ((b, props), _)) = |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
157 |
(case Properties.get props "NAME" of |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
158 |
SOME name => if a = b then [name] else [] |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
159 |
| NONE => []) |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
160 |
| parse_named _ _ = []; |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
161 |
|
57334 | 162 |
val isabelle_jedit_actions = |
56135 | 163 |
(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
|
164 |
XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
165 |
| _ => []); |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
166 |
|
57334 | 167 |
val isabelle_jedit_dockables = |
56135 | 168 |
(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
|
169 |
XML.Elem (("DOCKABLES", _), body) => maps (parse_named "DOCKABLE") body |
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 |
|
57334 | 172 |
val jedit_actions = |
173 |
Lazy.lazy (fn () => |
|
174 |
(case Isabelle_System.bash_output |
|
175 |
"unzip -p \"$JEDIT_HOME/dist/jedit.jar\" org/gjt/sp/jedit/actions.xml" of |
|
176 |
(txt, 0) => |
|
177 |
(case XML.parse txt of |
|
178 |
XML.Elem (("ACTIONS", _), body) => maps (parse_named "ACTION") body |
|
179 |
| _ => []) |
|
180 |
| (_, rc) => error ("Cannot unzip jedit.jar\nreturn code = " ^ string_of_int rc))); |
|
56059
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
181 |
|
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
182 |
in |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
183 |
|
57334 | 184 |
fun is_action a = |
185 |
member (op =) isabelle_jedit_actions a orelse |
|
186 |
member (op =) isabelle_jedit_dockables a orelse |
|
187 |
member (op =) (Lazy.force jedit_actions) a; |
|
56059
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
188 |
|
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
189 |
end; |
26742 | 190 |
|
26751 | 191 |
|
30394 | 192 |
(* Isabelle/Isar entities (with index) *) |
26751 | 193 |
|
194 |
local |
|
195 |
||
26894 | 196 |
fun no_check _ _ = true; |
197 |
||
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58923
diff
changeset
|
198 |
fun is_keyword ctxt (name, _) = |
58931 | 199 |
Keyword.is_keyword (Thy_Header.get_keywords' ctxt) name; |
58919 | 200 |
|
56294
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
56278
diff
changeset
|
201 |
fun check_command ctxt (name, pos) = |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58923
diff
changeset
|
202 |
let |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58923
diff
changeset
|
203 |
val thy = Proof_Context.theory_of ctxt; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58923
diff
changeset
|
204 |
val keywords = Thy_Header.get_keywords thy; |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58923
diff
changeset
|
205 |
in |
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58923
diff
changeset
|
206 |
Keyword.is_command keywords name andalso |
58923 | 207 |
let |
208 |
val markup = |
|
59083 | 209 |
Token.explode keywords Position.none name |
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58923
diff
changeset
|
210 |
|> maps (Outer_Syntax.command_reports thy) |
58923 | 211 |
|> map (snd o fst); |
212 |
val _ = Context_Position.reports ctxt (map (pair pos) markup); |
|
213 |
in true end |
|
214 |
end; |
|
53061 | 215 |
|
56467 | 216 |
fun check_system_option ctxt (name, pos) = |
217 |
(Context_Position.report ctxt pos (Options.default_markup (name, pos)); true) |
|
218 |
handle ERROR _ => false; |
|
219 |
||
56294
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
56278
diff
changeset
|
220 |
fun check_tool ctxt (name, pos) = |
53044 | 221 |
let |
222 |
fun tool dir = |
|
223 |
let val path = Path.append dir (Path.basic name) |
|
224 |
in if File.exists path then SOME path else NONE end; |
|
225 |
in |
|
53045 | 226 |
(case get_first tool (Path.split (getenv "ISABELLE_TOOLS")) of |
53044 | 227 |
NONE => false |
56294
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
56278
diff
changeset
|
228 |
| SOME path => (Context_Position.report ctxt pos (Markup.path (Path.implode path)); true)) |
53044 | 229 |
end; |
28237 | 230 |
|
26751 | 231 |
val arg = enclose "{" "}" o clean_string; |
232 |
||
56185 | 233 |
fun entity check markup binding index = |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37198
diff
changeset
|
234 |
Thy_Output.antiquotation |
56185 | 235 |
(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
|
236 |
(case index of NONE => "" | SOME true => "_def" | SOME false => "_ref"))) |
53044 | 237 |
(Scan.lift (Scan.optional (Args.parens Args.name) "" -- Parse.position Args.name)) |
238 |
(fn {context = ctxt, ...} => fn (logic, (name, pos)) => |
|
30394 | 239 |
let |
56185 | 240 |
val kind = translate (fn "_" => " " | c => c) (Binding.name_of binding); |
30394 | 241 |
val hyper_name = |
242 |
"{" ^ Long_Name.append kind (Long_Name.append logic (clean_name name)) ^ "}"; |
|
243 |
val hyper = |
|
244 |
enclose ("\\hyperlink" ^ hyper_name ^ "{") "}" #> |
|
245 |
index = SOME true ? enclose ("\\hypertarget" ^ hyper_name ^ "{") "}"; |
|
246 |
val idx = |
|
247 |
(case index of |
|
248 |
NONE => "" |
|
249 |
| SOME is_def => |
|
250 |
"\\index" ^ (if is_def then "def" else "ref") ^ arg logic ^ arg kind ^ arg name); |
|
251 |
in |
|
53044 | 252 |
if check ctxt (name, pos) then |
30394 | 253 |
idx ^ |
254 |
(Output.output name |
|
255 |
|> (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
|
256 |
|> (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
|
257 |
|> (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
|
258 |
then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" |
30394 | 259 |
else hyper o enclose "\\mbox{\\isa{" "}}")) |
53044 | 260 |
else error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos) |
30394 | 261 |
end); |
26897 | 262 |
|
26894 | 263 |
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
|
264 |
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
|
265 |
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
|
266 |
entity check markup kind (SOME false); |
26751 | 267 |
|
268 |
in |
|
269 |
||
56059
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
270 |
val _ = |
2390391584c2
some document antiquotations for Isabelle/jEdit elements;
wenzelm
parents:
55997
diff
changeset
|
271 |
Theory.setup |
56185 | 272 |
(entity_antiqs no_check "" @{binding syntax} #> |
56294
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
56278
diff
changeset
|
273 |
entity_antiqs check_command "isacommand" @{binding command} #> |
58919 | 274 |
entity_antiqs is_keyword "isakeyword" @{binding keyword} #> |
275 |
entity_antiqs is_keyword "isakeyword" @{binding element} #> |
|
56185 | 276 |
entity_antiqs (can o Method.check_name) "" @{binding method} #> |
277 |
entity_antiqs (can o Attrib.check_name) "" @{binding attribute} #> |
|
278 |
entity_antiqs no_check "" @{binding fact} #> |
|
279 |
entity_antiqs no_check "" @{binding variable} #> |
|
280 |
entity_antiqs no_check "" @{binding case} #> |
|
281 |
entity_antiqs (can o Thy_Output.check_command) "" @{binding antiquotation} #> |
|
282 |
entity_antiqs (can o Thy_Output.check_option) "" @{binding antiquotation_option} #> |
|
58716
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
58069
diff
changeset
|
283 |
entity_antiqs no_check "isasystem" @{binding setting} #> |
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
58069
diff
changeset
|
284 |
entity_antiqs check_system_option "isasystem" @{binding system_option} #> |
56185 | 285 |
entity_antiqs no_check "" @{binding inference} #> |
58716
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
58069
diff
changeset
|
286 |
entity_antiqs no_check "isasystem" @{binding executable} #> |
56294
85911b8a6868
prefer Context_Position where a context is available;
wenzelm
parents:
56278
diff
changeset
|
287 |
entity_antiqs check_tool "isatool" @{binding tool} #> |
56185 | 288 |
entity_antiqs (can o ML_Context.check_antiquotation) "" @{binding ML_antiquotation} #> |
58716
23a380cc45f4
official support for "tt" style variants, avoid fragile \verb in LaTeX;
wenzelm
parents:
58069
diff
changeset
|
289 |
entity_antiqs (K (is_action o #1)) "isasystem" @{binding action}); |
26751 | 290 |
|
26742 | 291 |
end; |
26751 | 292 |
|
293 |
end; |