author  wenzelm 
Thu, 25 Jan 2018 16:30:20 +0100  
changeset 67508  189ab2c3026b 
parent 67506  30233285270a 
child 67522  9e712280cc37 
permissions  rwrr 
22124  1 
(* Title: Pure/Thy/thy_output.ML 
67386  2 
Author: Makarius 
22124  3 

67386  4 
Theory document output. 
22124  5 
*) 
6 

7 
signature THY_OUTPUT = 

8 
sig 

67381  9 
val output_text: Proof.context > {markdown: bool} > Input.source > Latex.text list 
10 
val check_comments: Proof.context > Symbol_Pos.T list > unit 

11 
val check_token_comments: Proof.context > Token.T > unit 

12 
val output_token: Proof.context > Token.T > Latex.text list 

67474
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67465
diff
changeset

13 
val output_source: Proof.context > string > Latex.text list 
67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %forms into main tex source;
wenzelm
parents:
67191
diff
changeset

14 
val present_thy: theory > (Toplevel.transition * Toplevel.state) list > 
1c0a6a957114
positions as postlude: avoid intrusion of odd %forms into main tex source;
wenzelm
parents:
67191
diff
changeset

15 
Token.T list > Latex.text list 
28644  16 
val pretty_term: Proof.context > term > Pretty.T 
17 
val pretty_thm: Proof.context > thm > Pretty.T 

67508  18 
val lines: Latex.text list > Latex.text list 
67505
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67475
diff
changeset

19 
val items: Latex.text list > Latex.text list 
67463  20 
val isabelle: Proof.context > Latex.text list > Latex.text 
21 
val isabelle_typewriter: Proof.context > Latex.text list > Latex.text 

22 
val typewriter: Proof.context > string > Latex.text 

23 
val verbatim: Proof.context > string > Latex.text 

67474
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67465
diff
changeset

24 
val source: Proof.context > Token.src > Latex.text 
67505
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67475
diff
changeset

25 
val pretty: Proof.context > Pretty.T > Latex.text 
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67475
diff
changeset

26 
val pretty_source: Proof.context > Token.src > Pretty.T > Latex.text 
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67475
diff
changeset

27 
val pretty_items: Proof.context > Pretty.T list > Latex.text 
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67475
diff
changeset

28 
val pretty_items_source: Proof.context > Token.src > Pretty.T list > Latex.text 
67463  29 
val antiquotation_pretty: 
67505
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67475
diff
changeset

30 
binding > 'a context_parser > (Proof.context > 'a > Pretty.T) > theory > theory 
67463  31 
val antiquotation_pretty_source: 
67505
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67475
diff
changeset

32 
binding > 'a context_parser > (Proof.context > 'a > Pretty.T) > theory > theory 
67463  33 
val antiquotation_raw: 
34 
binding > 'a context_parser > (Proof.context > 'a > Latex.text) > theory > theory 

35 
val antiquotation_verbatim: 

36 
binding > 'a context_parser > (Proof.context > 'a > string) > theory > theory 

22124  37 
end; 
38 

37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37198
diff
changeset

39 
structure Thy_Output: THY_OUTPUT = 
22124  40 
struct 
41 

61457  42 
(* output text *) 
56548  43 

67381  44 
fun output_text ctxt {markdown} source = 
61457  45 
let 
46 
val pos = Input.pos_of source; 

47 
val syms = Input.source_explode source; 

48 

67381  49 
val _ = Context_Position.report ctxt pos (Markup.language_document (Input.is_delimited source)); 
62749  50 

67463  51 
val output_antiquotes = maps (Document_Antiquotation.evaluate ctxt); 
61036
f6f2959bed67
clarified language context, e.g. relevant for symbols;
wenzelm
parents:
60100
diff
changeset

52 

61461  53 
fun output_line line = 
67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %forms into main tex source;
wenzelm
parents:
67191
diff
changeset

54 
(if Markdown.line_is_item line then [Latex.string "\\item "] else []) @ 
61461  55 
output_antiquotes (Markdown.line_content line); 
56 

67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %forms into main tex source;
wenzelm
parents:
67191
diff
changeset

57 
fun output_block (Markdown.Par lines) = 
1c0a6a957114
positions as postlude: avoid intrusion of odd %forms into main tex source;
wenzelm
parents:
67191
diff
changeset

58 
Latex.block (separate (Latex.string "\n") (map (Latex.block o output_line) lines)) 
61459
5f2ddeb15c06
clarified nesting of paragraphs: indentation is taken into account more uniformly;
wenzelm
parents:
61458
diff
changeset

59 
 output_block (Markdown.List {kind, body, ...}) = 
67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %forms into main tex source;
wenzelm
parents:
67191
diff
changeset

60 
Latex.environment_block (Markdown.print_kind kind) (output_blocks body) 
1c0a6a957114
positions as postlude: avoid intrusion of odd %forms into main tex source;
wenzelm
parents:
67191
diff
changeset

61 
and output_blocks blocks = separate (Latex.string "\n\n") (map output_block blocks); 
67184  62 
in 
67381  63 
if Toplevel.is_skipped_proof (Toplevel.presentation_state ctxt) then [] 
67184  64 
else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms 
65 
then 

66 
let 

67 
val ants = Antiquote.parse pos syms; 

68 
val reports = Antiquote.antiq_reports ants; 

69 
val blocks = Markdown.read_antiquotes ants; 

67381  70 
val _ = Context_Position.reports ctxt (reports @ Markdown.reports blocks); 
67186
a58bbe66ac81
avoid excessive whitespace between antiquotations and text;
wenzelm
parents:
67184
diff
changeset

71 
in output_blocks blocks end 
67184  72 
else 
73 
let 

67463  74 
val ants = Antiquote.parse pos (trim (Symbol.is_blank o Symbol_Pos.symbol) syms); 
67184  75 
val reports = Antiquote.antiq_reports ants; 
67381  76 
val _ = Context_Position.reports ctxt (reports @ Markdown.text_reports ants); 
67186
a58bbe66ac81
avoid excessive whitespace between antiquotations and text;
wenzelm
parents:
67184
diff
changeset

77 
in output_antiquotes ants end 
67184  78 
end; 
48918
6e5fd4585512
check sidecomments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents:
47005
diff
changeset

79 

6e5fd4585512
check sidecomments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents:
47005
diff
changeset

80 

67425
7d4a088dbc0e
clarified modules: uniform notion of formal comments;
wenzelm
parents:
67421
diff
changeset

81 
(* output tokens with formal comments *) 
22124  82 

67353  83 
local 
84 

67461  85 
val output_symbols = single o Latex.symbols_output; 
67356
ba226b87c69e
output token content with formal comments and antiquotations;
wenzelm
parents:
67354
diff
changeset

86 

67358  87 
val output_symbols_antiq = 
88 
(fn Antiquote.Text syms => output_symbols syms 

67353  89 
 Antiquote.Control {name = (name, _), body, ...} => 
67374
5a049cf98438
clarified output (see also 909dcdec2122, 34d1913f0b20);
wenzelm
parents:
67372
diff
changeset

90 
Latex.string (Latex.output_symbols [Symbol.encode (Symbol.Control name)]) :: 
67358  91 
output_symbols body 
67353  92 
 Antiquote.Antiq {body, ...} => 
67358  93 
Latex.enclose_body "%\n\\isaantiq\n" "{}%\n\\endisaantiq\n" (output_symbols body)); 
67353  94 

67425
7d4a088dbc0e
clarified modules: uniform notion of formal comments;
wenzelm
parents:
67421
diff
changeset

95 
fun output_symbols_comment ctxt {antiq} (comment, syms) = 
7d4a088dbc0e
clarified modules: uniform notion of formal comments;
wenzelm
parents:
67421
diff
changeset

96 
(case (comment, antiq) of 
7d4a088dbc0e
clarified modules: uniform notion of formal comments;
wenzelm
parents:
67421
diff
changeset

97 
(NONE, false) => output_symbols syms 
7d4a088dbc0e
clarified modules: uniform notion of formal comments;
wenzelm
parents:
67421
diff
changeset

98 
 (NONE, true) => 
67413  99 
Antiquote.parse (#1 (Symbol_Pos.range syms)) syms 
100 
> maps output_symbols_antiq 

67425
7d4a088dbc0e
clarified modules: uniform notion of formal comments;
wenzelm
parents:
67421
diff
changeset

101 
 (SOME Comment.Comment, _) => 
67413  102 
let 
103 
val body = Symbol_Pos.cartouche_content syms; 

104 
val source = Input.source true (Symbol_Pos.implode body) (Symbol_Pos.range body); 

67475
1a279ad4c6a4
disable "display" style in marginal (line) comment;
wenzelm
parents:
67474
diff
changeset

105 
val ctxt' = ctxt 
1a279ad4c6a4
disable "display" style in marginal (line) comment;
wenzelm
parents:
67474
diff
changeset

106 
> Config.put Document_Antiquotation.thy_output_display false; 
67413  107 
in 
67475
1a279ad4c6a4
disable "display" style in marginal (line) comment;
wenzelm
parents:
67474
diff
changeset

108 
output_text ctxt' {markdown = false} source 
67421
c4a10621c72e
allow TeX comment % in formal comment body, but avoid extra space (cf. d7c6054b2ab1);
wenzelm
parents:
67413
diff
changeset

109 
> Latex.enclose_body "%\n\\isamarkupcmt{" "%\n}" 
67425
7d4a088dbc0e
clarified modules: uniform notion of formal comments;
wenzelm
parents:
67421
diff
changeset

110 
end 
7d4a088dbc0e
clarified modules: uniform notion of formal comments;
wenzelm
parents:
67421
diff
changeset

111 
 (SOME Comment.Cancel, _) => 
7d4a088dbc0e
clarified modules: uniform notion of formal comments;
wenzelm
parents:
67421
diff
changeset

112 
output_symbols (Symbol_Pos.cartouche_content syms) 
67429  113 
> Latex.enclose_body "%\n\\isamarkupcancel{" "}" 
114 
 (SOME Comment.Latex, _) => 

67461  115 
[Latex.symbols (Symbol_Pos.cartouche_content syms)]); 
67372  116 

67353  117 
in 
118 

67381  119 
fun output_body ctxt antiq bg en syms = 
67425
7d4a088dbc0e
clarified modules: uniform notion of formal comments;
wenzelm
parents:
67421
diff
changeset

120 
(case Comment.read_body syms of 
7d4a088dbc0e
clarified modules: uniform notion of formal comments;
wenzelm
parents:
67421
diff
changeset

121 
SOME res => maps (output_symbols_comment ctxt {antiq = antiq}) res 
67375  122 
 NONE => output_symbols syms) > Latex.enclose_body bg en 
67381  123 
and output_token ctxt tok = 
67353  124 
let 
67378  125 
fun output antiq bg en = 
67381  126 
output_body ctxt antiq bg en (Input.source_explode (Token.input_of tok)); 
67378  127 
in 
128 
(case Token.kind_of tok of 

67439
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
67429
diff
changeset

129 
Token.Comment NONE => [] 
67378  130 
 Token.Command => output false "\\isacommand{" "}" 
131 
 Token.Keyword => 

132 
if Symbol.is_ascii_identifier (Token.content_of tok) 

133 
then output false "\\isakeyword{" "}" 

134 
else output false "" "" 

135 
 Token.String => output false "{\\isachardoublequoteopen}" "{\\isachardoublequoteclose}" 

136 
 Token.Alt_String => output false "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}" 

137 
 Token.Verbatim => output true "{\\isacharverbatimopen}" "{\\isacharverbatimclose}" 

138 
 Token.Cartouche => output false "{\\isacartoucheopen}" "{\\isacartoucheclose}" 

139 
 _ => output false "" "") 

140 
end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok)); 

67353  141 

67474
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67465
diff
changeset

142 
fun output_source ctxt s = 
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67465
diff
changeset

143 
output_body ctxt false "" "" (Symbol_Pos.explode (s, Position.none)); 
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67465
diff
changeset

144 

67381  145 
fun check_comments ctxt = 
67425
7d4a088dbc0e
clarified modules: uniform notion of formal comments;
wenzelm
parents:
67421
diff
changeset

146 
Comment.read_body #> (Option.app o List.app) (fn (comment, syms) => 
67388
5fc0b0c9a735
clarified markup: more like outer syntax sidecomment;
wenzelm
parents:
67386
diff
changeset

147 
let 
5fc0b0c9a735
clarified markup: more like outer syntax sidecomment;
wenzelm
parents:
67386
diff
changeset

148 
val pos = #1 (Symbol_Pos.range syms); 
5fc0b0c9a735
clarified markup: more like outer syntax sidecomment;
wenzelm
parents:
67386
diff
changeset

149 
val _ = 
67429  150 
comment > Option.app (fn kind => 
67506
30233285270a
more markup: disable spellchecker for raw latex;
wenzelm
parents:
67505
diff
changeset

151 
Context_Position.reports ctxt (map (pair pos) (Markup.cartouche :: Comment.markups kind))); 
67425
7d4a088dbc0e
clarified modules: uniform notion of formal comments;
wenzelm
parents:
67421
diff
changeset

152 
val _ = output_symbols_comment ctxt {antiq = false} (comment, syms); 
7d4a088dbc0e
clarified modules: uniform notion of formal comments;
wenzelm
parents:
67421
diff
changeset

153 
in if comment = SOME Comment.Comment then check_comments ctxt syms else () end); 
67377
143665524d8e
check formal comments recursively, within arbitrary cartouches (unknown sublanguages);
wenzelm
parents:
67375
diff
changeset

154 

67381  155 
fun check_token_comments ctxt tok = 
156 
check_comments ctxt (Input.source_explode (Token.input_of tok)); 

67377
143665524d8e
check formal comments recursively, within arbitrary cartouches (unknown sublanguages);
wenzelm
parents:
67375
diff
changeset

157 

67353  158 
end; 
159 

160 

67356
ba226b87c69e
output token content with formal comments and antiquotations;
wenzelm
parents:
67354
diff
changeset

161 

ba226b87c69e
output token content with formal comments and antiquotations;
wenzelm
parents:
67354
diff
changeset

162 
(** present theory source **) 
ba226b87c69e
output token content with formal comments and antiquotations;
wenzelm
parents:
67354
diff
changeset

163 

ba226b87c69e
output token content with formal comments and antiquotations;
wenzelm
parents:
67354
diff
changeset

164 
(*NB: arranging white space around command spans is a black art*) 
ba226b87c69e
output token content with formal comments and antiquotations;
wenzelm
parents:
67354
diff
changeset

165 

67439
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
67429
diff
changeset

166 
val is_white = Token.is_space orf Token.is_informal_comment; 
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
67429
diff
changeset

167 
val is_black = not o is_white; 
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
67429
diff
changeset

168 

78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
67429
diff
changeset

169 
val is_white_comment = Token.is_informal_comment; 
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
67429
diff
changeset

170 
val is_black_comment = Token.is_formal_comment; 
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
67429
diff
changeset

171 

67356
ba226b87c69e
output token content with formal comments and antiquotations;
wenzelm
parents:
67354
diff
changeset

172 

22124  173 
(* presentation tokens *) 
174 

175 
datatype token = 

67360  176 
Ignore_Token 
59065  177 
 Basic_Token of Token.T 
178 
 Markup_Token of string * Input.source 

179 
 Markup_Env_Token of string * Input.source 

61456  180 
 Raw_Token of Input.source; 
22124  181 

59065  182 
fun basic_token pred (Basic_Token tok) = pred tok 
22124  183 
 basic_token _ _ = false; 
184 

67439
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
67429
diff
changeset

185 
val white_token = basic_token is_white; 
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
67429
diff
changeset

186 
val white_comment_token = basic_token is_white_comment; 
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36950
diff
changeset

187 
val blank_token = basic_token Token.is_blank; 
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36950
diff
changeset

188 
val newline_token = basic_token Token.is_newline; 
22124  189 

67381  190 
fun present_token ctxt tok = 
61457  191 
(case tok of 
67360  192 
Ignore_Token => [] 
67381  193 
 Basic_Token tok => output_token ctxt tok 
67357  194 
 Markup_Token (cmd, source) => 
195 
Latex.enclose_body ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n" 

67381  196 
(output_text ctxt {markdown = false} source) 
61457  197 
 Markup_Env_Token (cmd, source) => 
67381  198 
[Latex.environment_block ("isamarkup" ^ cmd) (output_text ctxt {markdown = true} source)] 
67186
a58bbe66ac81
avoid excessive whitespace between antiquotations and text;
wenzelm
parents:
67184
diff
changeset

199 
 Raw_Token source => 
67381  200 
Latex.string "%\n" :: output_text ctxt {markdown = true} source @ [Latex.string "\n"]); 
61455  201 

202 

22124  203 
(* command spans *) 
204 

205 
type command = string * Position.T * string list; (*name, position, tags*) 

206 
type source = (token * (string * int)) list; (*token, markup flag, metacomment depth*) 

207 

208 
datatype span = Span of command * (source * source * source * source) * bool; 

209 

210 
fun make_span cmd src = 

211 
let 

212 
fun take_newline (tok :: toks) = 

213 
if newline_token (fst tok) then ([tok], toks, true) 

214 
else ([], tok :: toks, false) 

215 
 take_newline [] = ([], [], false); 

216 
val (((src_prefix, src_main), src_suffix1), (src_suffix2, src_appendix, newline)) = 

217 
src 

67439
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
67429
diff
changeset

218 
> take_prefix (white_token o fst) 
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
67429
diff
changeset

219 
>> take_suffix (white_token o fst) 
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
67429
diff
changeset

220 
>> take_prefix (white_comment_token o fst) 
22124  221 
> take_newline; 
222 
in Span (cmd, (src_prefix, src_main, src_suffix1 @ src_suffix2, src_appendix), newline) end; 

223 

224 

225 
(* present spans *) 

226 

227 
local 

228 

229 
fun err_bad_nesting pos = 

230 
error ("Bad nesting of commands in presentation" ^ pos); 

231 

232 
fun edge which f (x: string option, y) = 

233 
if x = y then I 

67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %forms into main tex source;
wenzelm
parents:
67191
diff
changeset

234 
else (case which (x, y) of NONE => I  SOME txt => cons (Latex.string (f txt))); 
22124  235 

236 
val begin_tag = edge #2 Latex.begin_tag; 

237 
val end_tag = edge #1 Latex.end_tag; 

238 
fun open_delim delim e = edge #2 Latex.begin_delim e #> delim #> edge #2 Latex.end_delim e; 

239 
fun close_delim delim e = edge #1 Latex.begin_delim e #> delim #> edge #1 Latex.end_delim e; 

240 

241 
in 

242 

67381  243 
fun present_span thy keywords document_tags span state state' 
67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %forms into main tex source;
wenzelm
parents:
67191
diff
changeset

244 
(tag_stack, active_tag, newline, latex, present_cont) = 
22124  245 
let 
67381  246 
val ctxt' = 
247 
Toplevel.presentation_context state' 

248 
handle Toplevel.UNDEF => Proof_Context.init_global (Context.get_theory thy Context.PureN); 

22124  249 
val present = fold (fn (tok, (flag, 0)) => 
67381  250 
fold cons (present_token ctxt' tok) 
67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %forms into main tex source;
wenzelm
parents:
67191
diff
changeset

251 
#> cons (Latex.string flag) 
22124  252 
 _ => I); 
253 

254 
val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span; 

255 

256 
val (tag, tags) = tag_stack; 

46924  257 
val tag' = try hd (fold (update (op =)) cmd_tags (the_list tag)); 
22124  258 

58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58992
diff
changeset

259 
val nesting = Toplevel.level state'  Toplevel.level state; 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58992
diff
changeset

260 

22124  261 
val active_tag' = 
262 
if is_some tag' then tag' 

263 
else if cmd_name = "end" andalso not (Toplevel.is_toplevel state') then NONE 

58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58992
diff
changeset

264 
else 
67138  265 
(case Keyword.command_tags keywords cmd_name @ document_tags of 
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58992
diff
changeset

266 
default_tag :: _ => SOME default_tag 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58992
diff
changeset

267 
 [] => 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58992
diff
changeset

268 
if Keyword.is_vacuous keywords cmd_name andalso Toplevel.is_proof state 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58992
diff
changeset

269 
then active_tag 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58992
diff
changeset

270 
else NONE); 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58992
diff
changeset

271 

22124  272 
val edge = (active_tag, active_tag'); 
273 

274 
val newline' = 

275 
if is_none active_tag' then span_newline else newline; 

276 

277 
val tag_stack' = 

278 
if nesting = 0 andalso not (Toplevel.is_proof state) then tag_stack 

279 
else if nesting >= 0 then (tag', replicate nesting tag @ tags) 

280 
else 

33957  281 
(case drop (~ nesting  1) tags of 
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58992
diff
changeset

282 
tg :: tgs => (tg, tgs) 
48992  283 
 [] => err_bad_nesting (Position.here cmd_pos)); 
22124  284 

67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %forms into main tex source;
wenzelm
parents:
67191
diff
changeset

285 
val latex' = 
1c0a6a957114
positions as postlude: avoid intrusion of odd %forms into main tex source;
wenzelm
parents:
67191
diff
changeset

286 
latex 
22124  287 
> end_tag edge 
288 
> close_delim (fst present_cont) edge 

289 
> snd present_cont 

290 
> open_delim (present (#1 srcs)) edge 

291 
> begin_tag edge 

292 
> present (#2 srcs); 

293 
val present_cont' = 

294 
if newline then (present (#3 srcs), present (#4 srcs)) 

295 
else (I, present (#3 srcs) #> present (#4 srcs)); 

67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %forms into main tex source;
wenzelm
parents:
67191
diff
changeset

296 
in (tag_stack', active_tag', newline', latex', present_cont') end; 
22124  297 

67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %forms into main tex source;
wenzelm
parents:
67191
diff
changeset

298 
fun present_trailer ((_, tags), active_tag, _, latex, present_cont) = 
22124  299 
if not (null tags) then err_bad_nesting " at end of theory" 
300 
else 

67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %forms into main tex source;
wenzelm
parents:
67191
diff
changeset

301 
latex 
22124  302 
> end_tag (active_tag, NONE) 
303 
> close_delim (fst present_cont) (active_tag, NONE) 

304 
> snd present_cont; 

305 

306 
end; 

307 

308 

28427
cc9f7d99fb73
turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents:
28273
diff
changeset

309 
(* present_thy *) 
22124  310 

311 
local 

312 

61455  313 
val markup_true = "\\isamarkuptrue%\n"; 
314 
val markup_false = "\\isamarkupfalse%\n"; 

315 

22124  316 
val space_proper = 
67439
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
67429
diff
changeset

317 
Scan.one Token.is_blank  Scan.many is_white_comment  Scan.one is_black; 
22124  318 

67439
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
67429
diff
changeset

319 
val is_improper = not o (is_black orf Token.is_begin_ignore orf Token.is_end_ignore); 
22124  320 
val improper = Scan.many is_improper; 
321 
val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper)); 

36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36950
diff
changeset

322 
val blank_end = Scan.repeat (Scan.unless space_proper (Scan.one Token.is_blank)); 
22124  323 

36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36950
diff
changeset

324 
val opt_newline = Scan.option (Scan.one Token.is_newline); 
22124  325 

326 
val ignore = 

36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36950
diff
changeset

327 
Scan.depend (fn d => opt_newline  Scan.one Token.is_begin_ignore 
22124  328 
>> pair (d + 1))  
36959
f5417836dbea
renamed structure OuterLex to Token and type token to Token.T, keeping legacy aliases for some time;
wenzelm
parents:
36950
diff
changeset

329 
Scan.depend (fn d => Scan.one Token.is_end_ignore  
43947
9b00f09f7721
defer evaluation of Scan.message, for improved performance in the frequent situation where failure is handled later (e.g. via );
wenzelm
parents:
43564
diff
changeset

330 
(if d = 0 then Scan.fail_with (K (fn () => "Bad nesting of metacomments")) else opt_newline) 
22124  331 
>> pair (d  1)); 
332 

36950  333 
val tag = (improper  Parse.$$$ "%"  improper)  Parse.!!! (Parse.tag_name  blank_end); 
22124  334 

335 
val locale = 

36950  336 
Scan.option ((Parse.$$$ "("  improper  Parse.$$$ "in")  
62969  337 
Parse.!!! (improper  Parse.name  (improper  Parse.$$$ ")"))); 
22124  338 

339 
in 

340 

58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58923
diff
changeset

341 
fun present_thy thy command_results toks = 
22124  342 
let 
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58923
diff
changeset

343 
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

344 

23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58923
diff
changeset

345 

22124  346 
(* tokens *) 
347 

348 
val ignored = Scan.state  ignore 

67360  349 
>> (fn d => (NONE, (Ignore_Token, ("", d)))); 
22124  350 

58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58992
diff
changeset

351 
fun markup pred mk flag = Scan.peek (fn d => 
36950  352 
improper  
58999
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58992
diff
changeset

353 
Parse.position (Scan.one (fn tok => 
ed09ae4ea2d8
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
wenzelm
parents:
58992
diff
changeset

354 
Token.is_command tok andalso pred keywords (Token.content_of tok)))  
22124  355 
Scan.repeat tag  
51627
589daaf48dba
tuned signature  agree with markup terminology;
wenzelm
parents:
51626
diff
changeset

356 
Parse.!!!! ((improper  locale  improper)  Parse.document_source  improper_end) 
59064  357 
>> (fn (((tok, pos'), tags), source) => 
59065  358 
let val name = Token.content_of tok 
359 
in (SOME (name, pos', tags), (mk (name, source), (flag, d))) end)); 

22124  360 

361 
val command = Scan.peek (fn d => 

61814
1ca1142e1711
clarified type Token.src: plain token list, with usual implicit value assignment;
wenzelm
parents:
61748
diff
changeset

362 
Scan.optional (Scan.one Token.is_command_modifier ::: improper) []  
59924
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59917
diff
changeset

363 
Scan.one Token.is_command  Scan.repeat tag 
59939
7d46aa03696e
support for 'restricted' modifier: only qualified accesses outside the local scope;
wenzelm
parents:
59924
diff
changeset

364 
>> (fn ((cmd_mod, cmd), tags) => 
7d46aa03696e
support for 'restricted' modifier: only qualified accesses outside the local scope;
wenzelm
parents:
59924
diff
changeset

365 
map (fn tok => (NONE, (Basic_Token tok, ("", d)))) cmd_mod @ 
59924
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59917
diff
changeset

366 
[(SOME (Token.content_of cmd, Token.pos_of cmd, tags), 
61455  367 
(Basic_Token cmd, (markup_false, d)))])); 
22124  368 

369 
val cmt = Scan.peek (fn d => 

67446  370 
Scan.one is_black_comment >> (fn tok => (NONE, (Basic_Token tok, ("", d))))); 
22124  371 

372 
val other = Scan.peek (fn d => 

59065  373 
Parse.not_eof >> (fn tok => (NONE, (Basic_Token tok, ("", d))))); 
22124  374 

59924
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59917
diff
changeset

375 
val tokens = 
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59917
diff
changeset

376 
(ignored  
61455  377 
markup Keyword.is_document_heading Markup_Token markup_true  
378 
markup Keyword.is_document_body Markup_Env_Token markup_true  

61456  379 
markup Keyword.is_document_raw (Raw_Token o #2) "") >> single  
59924
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59917
diff
changeset

380 
command  
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59917
diff
changeset

381 
(cmt  other) >> single; 
22124  382 

383 

384 
(* spans *) 

385 

59065  386 
val is_eof = fn (_, (Basic_Token x, _)) => Token.is_eof x  _ => false; 
387 
val stopper = Scan.stopper (K (NONE, (Basic_Token Token.eof, ("", 0)))) is_eof; 

22124  388 

389 
val cmd = Scan.one (is_some o fst); 

27732  390 
val non_cmd = Scan.one (is_none o fst andf not o is_eof) >> #2; 
22124  391 

67439
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
67429
diff
changeset

392 
val white_comments = Scan.many (white_comment_token o fst o snd); 
22124  393 
val blank = Scan.one (blank_token o fst o snd); 
394 
val newline = Scan.one (newline_token o fst o snd); 

395 
val before_cmd = 

67439
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
67429
diff
changeset

396 
Scan.option (newline  white_comments)  
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
67429
diff
changeset

397 
Scan.option (newline  white_comments)  
78759a7bd874
more uniform support for formal comments in outer syntax, notably \<^cancel> and \<^latex>;
wenzelm
parents:
67429
diff
changeset

398 
Scan.option (blank  white_comments)  cmd; 
22124  399 

400 
val span = 

401 
Scan.repeat non_cmd  cmd  

402 
Scan.repeat (Scan.unless before_cmd non_cmd)  

403 
Scan.option (newline >> (single o snd)) 

404 
>> (fn (((toks1, (cmd, tok2)), toks3), tok4) => 

405 
make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4)))); 

406 

57080
0e5fa27d3293
strip trailing white space, to avoid notorious problems of jEdit with last line;
wenzelm
parents:
56548
diff
changeset

407 
val spans = toks 
0e5fa27d3293
strip trailing white space, to avoid notorious problems of jEdit with last line;
wenzelm
parents:
56548
diff
changeset

408 
> take_suffix Token.is_space > #1 
0e5fa27d3293
strip trailing white space, to avoid notorious problems of jEdit with last line;
wenzelm
parents:
56548
diff
changeset

409 
> Source.of_list 
59924
801b979ec0c2
more general notion of command span: command keyword not necessarily at start;
wenzelm
parents:
59917
diff
changeset

410 
> Source.source' 0 Token.stopper (Scan.error (Scan.bulk tokens >> flat)) 
58864  411 
> Source.source stopper (Scan.error (Scan.bulk span)) 
22124  412 
> Source.exhaust; 
28427
cc9f7d99fb73
turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents:
28273
diff
changeset

413 

cc9f7d99fb73
turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents:
28273
diff
changeset

414 

cc9f7d99fb73
turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents:
28273
diff
changeset

415 
(* present commands *) 
cc9f7d99fb73
turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents:
28273
diff
changeset

416 

67147  417 
val document_tags = space_explode "," (Options.default_string \<^system_option>\<open>document_tags\<close>); 
67138  418 

28427
cc9f7d99fb73
turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents:
28273
diff
changeset

419 
fun present_command tr span st st' = 
67191  420 
Toplevel.setmp_thread_position tr 
67381  421 
(present_span thy keywords document_tags span st st'); 
28427
cc9f7d99fb73
turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents:
28273
diff
changeset

422 

cc9f7d99fb73
turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents:
28273
diff
changeset

423 
fun present _ [] = I 
cc9f7d99fb73
turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents:
28273
diff
changeset

424 
 present st (((tr, st'), span) :: rest) = present_command tr span st st' #> present st' rest; 
22124  425 
in 
28427
cc9f7d99fb73
turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents:
28273
diff
changeset

426 
if length command_results = length spans then 
67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %forms into main tex source;
wenzelm
parents:
67191
diff
changeset

427 
((NONE, []), NONE, true, [], (I, I)) 
28427
cc9f7d99fb73
turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);
wenzelm
parents:
28273
diff
changeset

428 
> present Toplevel.toplevel (command_results ~~ spans) 
22124  429 
> present_trailer 
67194
1c0a6a957114
positions as postlude: avoid intrusion of odd %forms into main tex source;
wenzelm
parents:
67191
diff
changeset

430 
> rev 
22124  431 
else error "Messedup outer syntax for presentation" 
432 
end; 

433 

434 
end; 

435 

436 

437 

67386  438 
(** standard output operations **) 
22124  439 

67463  440 
(* pretty printing *) 
22124  441 

67463  442 
fun pretty_term ctxt t = 
443 
Syntax.pretty_term (Variable.auto_fixes t ctxt) t; 

24920  444 

32898
e871d897969c
term styles also cover antiquotations term_type and typeof
haftmann
parents:
32890
diff
changeset

445 
fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; 
e871d897969c
term styles also cover antiquotations term_type and typeof
haftmann
parents:
32890
diff
changeset

446 

22124  447 

30390
ad591ee76c78
simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents:
30381
diff
changeset

448 
(* default output *) 
ad591ee76c78
simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents:
30381
diff
changeset

449 

67508  450 
val lines = separate (Latex.string "\\isanewline%\n"); 
67505
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67475
diff
changeset

451 
val items = separate (Latex.string "\\isasep\\isanewline%\n"); 
22124  452 

67463  453 
fun isabelle ctxt body = 
454 
if Config.get ctxt Document_Antiquotation.thy_output_display 

455 
then Latex.environment_block "isabelle" body 

456 
else Latex.block (Latex.enclose_body "\\isa{" "}" body); 

59175
bf465f335e85
system option "pretty_margin" is superseded by "thy_output_margin";
wenzelm
parents:
59067
diff
changeset

457 

67463  458 
fun isabelle_typewriter ctxt body = 
459 
if Config.get ctxt Document_Antiquotation.thy_output_display 

460 
then Latex.environment_block "isabellett" body 

461 
else Latex.block (Latex.enclose_body "\\isatt{" "}" body); 

462 

463 
fun typewriter ctxt s = 

464 
isabelle_typewriter ctxt [Latex.string (Latex.output_ascii s)]; 

465 

466 
fun verbatim ctxt = 

467 
if Config.get ctxt Document_Antiquotation.thy_output_display 

468 
then Document_Antiquotation.indent_lines ctxt #> typewriter ctxt 

67508  469 
else split_lines #> map (typewriter ctxt) #> lines #> Latex.block; 
22124  470 

67474
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67465
diff
changeset

471 
fun source ctxt = 
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67465
diff
changeset

472 
Token.args_of_src 
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67465
diff
changeset

473 
#> map (Token.unparse #> Document_Antiquotation.prepare_lines ctxt) 
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67465
diff
changeset

474 
#> space_implode " " 
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67465
diff
changeset

475 
#> output_source ctxt 
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67465
diff
changeset

476 
#> isabelle ctxt; 
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67465
diff
changeset

477 

67463  478 
fun pretty ctxt = 
67505
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67475
diff
changeset

479 
Document_Antiquotation.output ctxt #> Latex.string #> single #> isabelle ctxt; 
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67475
diff
changeset

480 

ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67475
diff
changeset

481 
fun pretty_source ctxt src prt = 
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67475
diff
changeset

482 
if Config.get ctxt Document_Antiquotation.thy_output_source 
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67475
diff
changeset

483 
then source ctxt src else pretty ctxt prt; 
67463  484 

67505
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67475
diff
changeset

485 
fun pretty_items ctxt = 
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67475
diff
changeset

486 
map (Document_Antiquotation.output ctxt #> Latex.string) #> items #> isabelle ctxt; 
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67475
diff
changeset

487 

ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67475
diff
changeset

488 
fun pretty_items_source ctxt src prts = 
67474
90def2b06305
more uniform output of source / text / theory_text, with handling of formal comments etc.;
wenzelm
parents:
67465
diff
changeset

489 
if Config.get ctxt Document_Antiquotation.thy_output_source 
67505
ceb324e34c14
clarified signature: items with \isasep are special;
wenzelm
parents:
67475
diff
changeset

490 
then source ctxt src else pretty_items ctxt prts; 
61473
34d1913f0b20
clarified control antiquotations: decode control symbol to get name;
wenzelm
parents:
61471
diff
changeset

491 

67465  492 

493 
(* antiquotation variants *) 

494 

67463  495 
fun antiquotation_pretty name scan f = 
496 
Document_Antiquotation.setup name scan 

497 
(fn {context = ctxt, argument = x, ...} => pretty ctxt (f ctxt x)); 

498 

499 
fun antiquotation_pretty_source name scan f = 

500 
Document_Antiquotation.setup name scan 

501 
(fn {context = ctxt, source = src, argument = x} => pretty_source ctxt src (f ctxt x)); 

502 

503 
fun antiquotation_raw name scan f = 

504 
Document_Antiquotation.setup name scan 

505 
(fn {context = ctxt, argument = x, ...} => f ctxt x); 

506 

507 
fun antiquotation_verbatim name scan f = 

508 
antiquotation_raw name scan (fn ctxt => verbatim ctxt o f ctxt); 

61491
97261e6c1d42
another antiquotation short form: undecorated cartouche as alias for @{text};
wenzelm
parents:
61473
diff
changeset

509 

30390
ad591ee76c78
simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
wenzelm
parents:
30381
diff
changeset

510 
end; 