author  berghofe 
Fri, 26 Aug 2005 19:47:23 +0200  
changeset 17151  bc97adfeeaa7 
parent 17089  f708a31fa8bb 
child 17185  5140808111d1 
permissions  rwrr 
9140  1 
(* Title: Pure/Isar/isar_output.ML 
2 
ID: $Id$ 

16002  3 
Author: Markus Wenzel, TU Muenchen 
9140  4 

5 
Isar theory output. 

6 
*) 

7 

8 
signature ISAR_OUTPUT = 

9 
sig 

14899  10 
val display: bool ref 
11 
val quotes: bool ref 

12 
val indent: int ref 

13 
val source: bool ref 

10321  14 
val add_commands: (string * (Args.src > Toplevel.state > string)) list > unit 
9140  15 
val add_options: (string * (string > (unit > string) > unit > string)) list > unit 
9220  16 
val print_antiquotations: unit > unit 
9140  17 
val boolean: string > bool 
18 
val integer: string > int 

19 
val args: (Proof.context * Args.T list > 'a * (Proof.context * Args.T list)) > 

10321  20 
(Args.src > Proof.context > 'a > string) > Args.src > Toplevel.state > string 
9140  21 
datatype markup = Markup  MarkupEnv  Verbatim 
11714  22 
val modes: string list ref 
12939  23 
val eval_antiquote: Scan.lexicon > Toplevel.state > string * Position.T > string 
17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

24 
val present_thy: Scan.lexicon > (string > string list) > (markup > string > bool) > 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

25 
Toplevel.transition list > (OuterLex.token, 'a) Source.source > Buffer.T 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

26 
val output_list: (Proof.context > 'a > Pretty.T) > Args.src > 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

27 
Proof.context > 'a list > string 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

28 
val output: (Proof.context > 'a > Pretty.T) > Args.src > Proof.context > 'a > string 
9140  29 
end; 
30 

31 
structure IsarOutput: ISAR_OUTPUT = 

32 
struct 

33 

34 
structure T = OuterLex; 

35 
structure P = OuterParse; 

36 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

37 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

38 
(** global options **) 
14899  39 

40 
val locale = ref ""; 

41 
val display = ref false; 

42 
val quotes = ref false; 

43 
val indent = ref 0; 

44 
val source = ref false; 

45 
val break = ref false; 

46 

47 

48 

9140  49 
(** maintain global commands **) 
50 

51 
local 

52 

53 
val global_commands = 

10321  54 
ref (Symtab.empty: (Args.src > Toplevel.state > string) Symtab.table); 
9140  55 

56 
val global_options = 

57 
ref (Symtab.empty: (string > (unit > string) > unit > string) Symtab.table); 

58 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

59 
fun add_item kind (name, x) tab = 
16894  60 
(if not (Symtab.defined tab name) then () 
17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

61 
else warning ("Redefined antiquotation " ^ kind ^ ": " ^ quote name); 
9140  62 
Symtab.update ((name, x), tab)); 
63 

64 
in 

65 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

66 
val add_commands = Library.change global_commands o fold (add_item "command"); 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

67 
val add_options = Library.change global_options o fold (add_item "option"); 
9140  68 

69 
fun command src = 

70 
let val ((name, _), pos) = Args.dest_src src in 

71 
(case Symtab.lookup (! global_commands, name) of 

15531  72 
NONE => error ("Unknown antiquotation command: " ^ quote name ^ Position.str_of pos) 
73 
 SOME f => transform_failure (curry Antiquote.ANTIQUOTE_FAIL (name, pos)) (f src)) 

9140  74 
end; 
75 

76 
fun option (name, s) f () = 

77 
(case Symtab.lookup (! global_options, name) of 

15531  78 
NONE => error ("Unknown antiquotation option: " ^ quote name) 
79 
 SOME opt => opt s f ()); 

9140  80 

81 
fun options [] f = f 

82 
 options (opt :: opts) f = option opt (options opts f); 

83 

9213  84 

9220  85 
fun print_antiquotations () = 
86 
[Pretty.big_list "antiquotation commands:" (map Pretty.str (Symtab.keys (! global_commands))), 

87 
Pretty.big_list "antiquotation options:" (map Pretty.str (Symtab.keys (! global_options)))] 

88 
> Pretty.chunks > Pretty.writeln; 

9213  89 

9140  90 
end; 
91 

92 

93 

94 
(** syntax of antiquotations **) 

95 

96 
(* option values *) 

97 

98 
fun boolean "" = true 

99 
 boolean "true" = true 

100 
 boolean "false" = false 

101 
 boolean s = error ("Bad boolean value: " ^ quote s); 

102 

103 
fun integer s = 

104 
let 

105 
fun int ss = 

14899  106 
(case Library.read_int ss of (i, []) => i 
107 
 _ => error ("Bad integer value: " ^ quote s)); 

9140  108 
in (case Symbol.explode s of "" :: ss => ~ (int ss)  ss => int ss) end; 
109 

110 

111 
(* args syntax *) 

112 

113 
fun syntax (scan: (Proof.context * Args.T list > 'a * (Proof.context * Args.T list))) = 

114 
Args.syntax "antiquotation" scan; 

115 

10321  116 
fun args scan f src state : string = 
14899  117 
let 
118 
val ctxt0 = 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

119 
if ! locale = "" then Toplevel.body_context_of state 
15531  120 
else #3 (Locale.read_context_statement (SOME (! locale)) [] [] 
14899  121 
(ProofContext.init (Toplevel.theory_of state))); 
122 
val (ctxt, x) = syntax scan src ctxt0; 

10321  123 
in f src ctxt x end; 
9140  124 

125 

126 
(* outer syntax *) 

127 

128 
local 

129 

130 
val property = P.xname  Scan.optional (P.$$$ "="  P.!!! P.xname) ""; 

131 
val properties = Scan.optional (P.$$$ "["  P.!!! (P.enum "," property  P.$$$ "]")) []; 

132 

133 
val antiq = P.position P.xname  properties  P.arguments  Scan.ahead P.eof 

134 
>> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos))); 

135 

136 
fun antiq_args_aux keyword_lexicon (str, pos) = 

137 
Source.of_string str 

138 
> Symbol.source false 

139 
> T.source false (K (keyword_lexicon, Scan.empty_lexicon)) pos 

140 
> T.source_proper 

15531  141 
> Source.source T.stopper (Scan.error (Scan.bulk (P.!!! antiq))) NONE 
9140  142 
> Source.exhaust; 
143 

144 
in 

145 

146 
fun antiq_args lex (s, pos) = 

147 
(case antiq_args_aux lex (s, pos) of [x] => x  _ => raise ERROR) handle ERROR => 

148 
error ("Malformed antiquotation: " ^ quote ("@{" ^ s ^ "}") ^ Position.str_of pos); 

149 

150 
end; 

151 

152 

153 
(* eval_antiquote *) 

154 

11714  155 
val modes = ref ([]: string list); 
156 

9140  157 
fun eval_antiquote lex state (str, pos) = 
158 
let 

159 
fun expand (Antiquote.Text s) = s 

160 
 expand (Antiquote.Antiq x) = 

161 
let val (opts, src) = antiq_args lex x in 

10739  162 
options opts (fn () => command src state) (); (*preview errors!*) 
11714  163 
Library.setmp print_mode (! modes @ Latex.modes @ ! print_mode) 
16194  164 
(Output.no_warnings (options opts (fn () => command src state))) () 
10321  165 
end; 
9140  166 
val ants = Antiquote.antiquotes_of (str, pos); 
167 
in 

168 
if Toplevel.is_toplevel state andalso exists Antiquote.is_antiq ants then 

169 
error ("Cannot expand antiquotations at toplevel" ^ Position.str_of pos) 

170 
else implode (map expand ants) 

171 
end; 

172 

173 

174 

175 
(** present theory source **) 

176 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

177 
(* presentation tokens *) 
9140  178 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

179 
datatype token = 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

180 
NoToken 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

181 
 BasicToken of T.token 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

182 
 MarkupToken of string * (string * Position.T) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

183 
 MarkupEnvToken of string * (string * Position.T) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

184 
 VerbatimToken of string * Position.T; 
15430
1e1aeaf1dec3
Implemented hiding of proofs and other commands.
berghofe
parents:
15349
diff
changeset

185 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

186 
fun output_token lex state = 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

187 
let 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

188 
val eval = eval_antiquote lex state 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

189 
in 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

190 
fn NoToken => "" 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

191 
 BasicToken tok => Latex.output_basic tok 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

192 
 MarkupToken (cmd, txt) => Latex.output_markup cmd (eval txt) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

193 
 MarkupEnvToken (cmd, txt) => Latex.output_markup_env cmd (eval txt) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

194 
 VerbatimToken txt => Latex.output_verbatim (eval txt) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

195 
end; 
15430
1e1aeaf1dec3
Implemented hiding of proofs and other commands.
berghofe
parents:
15349
diff
changeset

196 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

197 
fun basic_token pred (BasicToken tok) = pred tok 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

198 
 basic_token _ _ = false; 
15430
1e1aeaf1dec3
Implemented hiding of proofs and other commands.
berghofe
parents:
15349
diff
changeset

199 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

200 
val improper_token = basic_token (not o T.is_proper); 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

201 
val comment_token = basic_token T.is_comment; 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

202 
val blank_token = basic_token T.is_blank; 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

203 
val newline_token = basic_token T.is_newline; 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

204 

15430
1e1aeaf1dec3
Implemented hiding of proofs and other commands.
berghofe
parents:
15349
diff
changeset

205 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

206 
(* command spans *) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

207 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

208 
type command = string * Position.T * string list; (*name, position, tags*) 
17089  209 
type tok = string * token * int; (*raw text, token, metacomment depth*) 
210 
type source = tok list; 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

211 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

212 
datatype span = Span of command * (source * source * source * source) * bool; 
15529
b86d5c84a9a7
Optimized present_tokens to produce fewer newlines when hiding proofs.
berghofe
parents:
15473
diff
changeset

213 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

214 
fun make_span cmd src = 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

215 
let 
17089  216 
fun take_newline ((tok: tok) :: toks) = 
17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

217 
if newline_token (#2 tok) then ([tok], toks, true) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

218 
else ([], tok :: toks, false) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

219 
 take_newline [] = ([], [], false); 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

220 
val (((src_prefix, src_main), src_suffix1), (src_suffix2, src_appendix, newline)) = 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

221 
src 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

222 
> take_prefix (improper_token o #2) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

223 
>> take_suffix (improper_token o #2) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

224 
>> take_prefix (comment_token o #2) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

225 
> take_newline; 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

226 
in Span (cmd, (src_prefix, src_main, src_suffix1 @ src_suffix2, src_appendix), newline) end; 
9140  227 

228 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

229 
(* present spans *) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

230 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

231 
local 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

232 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

233 
fun err_bad_nesting pos = 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

234 
error ("Bad nesting of commands in presentation" ^ pos); 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

235 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

236 
fun edge1 f (x, y) = if_none (Option.map (Buffer.add o f) (if x = y then NONE else x)) I; 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

237 
fun edge2 f (x, y) = if_none (Option.map (Buffer.add o f) (if x = y then NONE else y)) I; 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

238 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

239 
val begin_tag = edge2 Latex.begin_tag; 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

240 
val end_tag = edge1 Latex.end_tag; 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

241 
fun open_delim delim e = edge2 Latex.begin_delim e #> delim #> edge2 Latex.end_delim e; 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

242 
fun close_delim delim e = edge1 Latex.begin_delim e #> delim #> edge1 Latex.end_delim e; 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

243 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

244 
in 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

245 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

246 
fun present_span lex default_tags span state state' 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

247 
(tag_stack, active_tag, newline, buffer, present_cont) = 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

248 
let 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

249 
val present = fold (fn (raw, tok, d) => 
17151  250 
Buffer.add raw o (if d > 0 then I else Buffer.add (output_token lex state' tok))); 
17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

251 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

252 
val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span; 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

253 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

254 
val (tag, tags) = tag_stack; 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

255 
val tag' = 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

256 
(case tag of NONE => []  SOME tg => [tg]) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

257 
> fold OuterKeyword.update_tags cmd_tags 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

258 
> try hd; 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

259 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

260 
val active_tag' = 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

261 
if is_some tag' then tag' 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

262 
else try hd (default_tags cmd_name); 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

263 
val edge = (active_tag, active_tag'); 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

264 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

265 
val newline' = 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

266 
if is_none active_tag' then span_newline else newline; 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

267 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

268 
val nesting = Toplevel.level state'  Toplevel.level state; 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

269 
val tag_stack' = 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

270 
if nesting = 0 andalso not (Toplevel.is_proof state) then tag_stack 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

271 
else if nesting >= 0 then (tag', replicate nesting tag @ tags) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

272 
else 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

273 
(case Library.drop (~ nesting  1, tags) of 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

274 
tgs :: tgss => (tgs, tgss) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

275 
 [] => err_bad_nesting (Position.str_of cmd_pos)); 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

276 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

277 
val buffer' = 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

278 
buffer 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

279 
> end_tag edge 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

280 
> close_delim (fst present_cont) edge 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

281 
> snd present_cont 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

282 
> open_delim (present (#1 srcs)) edge 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

283 
> begin_tag edge 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

284 
> present (#2 srcs); 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

285 
val present_cont' = 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

286 
if newline then (present (#3 srcs), present (#4 srcs)) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

287 
else (I, present (#3 srcs) #> present (#4 srcs)); 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

288 
in (tag_stack', active_tag', newline', buffer', present_cont') end; 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

289 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

290 
fun present_trailer ((_, tags), active_tag, _, buffer, present_cont) = 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

291 
if not (null tags) then err_bad_nesting " at end of theory" 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

292 
else 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

293 
buffer 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

294 
> end_tag (active_tag, NONE) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

295 
> close_delim (fst present_cont) (active_tag, NONE) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

296 
> snd present_cont; 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

297 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

298 
end; 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

299 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

300 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

301 
(* present_thy *) 
9140  302 

303 
datatype markup = Markup  MarkupEnv  Verbatim; 

304 

305 
local 

306 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

307 
val space_proper = 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

308 
Scan.one T.is_blank  Scan.any T.is_comment  Scan.one T.is_proper; 
9140  309 

310 
val is_improper = not o (T.is_proper orf T.is_begin_ignore orf T.is_end_ignore); 

311 
val improper = Scan.any is_improper; 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

312 
val improper_end = Scan.repeat (Scan.unless space_proper (Scan.one is_improper)); 
9140  313 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

314 
val opt_newline = Scan.option (Scan.one T.is_newline); 
9140  315 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

316 
val ignore = 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

317 
Scan.depend (fn d => opt_newline  Scan.one T.is_begin_ignore 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

318 
>> pair (d + 1))  
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

319 
Scan.depend (fn d => Scan.one T.is_end_ignore  
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

320 
(if d = 0 then Scan.fail_with (K "Bad nesting of metacomments") else opt_newline) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

321 
>> pair (d  1)); 
9140  322 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

323 
val tag = (improper  P.$$$ "%"  improper)  P.!!! (P.tag_name  improper_end); 
9140  324 

325 
in 

326 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

327 
fun present_thy lex default_tags is_markup trs src = 
9140  328 
let 
17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

329 
(* tokens *) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

330 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

331 
val ignored = Scan.state  ignore 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

332 
>> (fn d => (NONE, ("", NoToken, d))); 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

333 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

334 
fun markup flag mark mk = Scan.peek (fn d => 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

335 
improper  
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

336 
P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.val_of))  
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

337 
Scan.repeat tag  
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

338 
P.!!!! (improper  P.position P.text  improper_end) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

339 
>> (fn (((tok, pos), tags), txt) => 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

340 
let val name = T.val_of tok 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

341 
in (SOME (name, pos, tags), (flag, mk (name, txt), d)) end)); 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

342 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

343 
val command = Scan.peek (fn d => 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

344 
P.position (Scan.one (T.is_kind T.Command))  
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

345 
Scan.repeat tag 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

346 
>> (fn ((tok, pos), tags) => 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

347 
let val name = T.val_of tok 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

348 
in (SOME (name, pos, tags), (Latex.markup_false, BasicToken tok, d)) end)); 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

349 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

350 
val cmt = Scan.peek (fn d => 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

351 
P.$$$ ""  P.!!!! (improper  P.position P.text) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

352 
>> (fn txt => (NONE, ("", MarkupToken ("cmt", txt), d)))); 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

353 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

354 
val other = Scan.peek (fn d => 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

355 
Scan.one T.not_eof >> (fn tok => (NONE, ("", BasicToken tok, d)))); 
9140  356 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

357 
val token = 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

358 
ignored  
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

359 
markup Latex.markup_true Markup MarkupToken  
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

360 
markup Latex.markup_true MarkupEnv MarkupEnvToken  
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

361 
markup "" Verbatim (VerbatimToken o #2)  
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

362 
command  cmt  other; 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

363 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

364 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

365 
(* spans *) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

366 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

367 
val stopper = 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

368 
((NONE, ("", BasicToken (#1 T.stopper), 0)), 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

369 
fn (_, (_, BasicToken x, _)) => #2 T.stopper x  _ => false); 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

370 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

371 
val cmd = Scan.one (is_some o #1); 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

372 
val non_cmd = Scan.one (is_none o #1 andf not o #2 stopper) >> #2; 
9140  373 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

374 
val comments = Scan.any (comment_token o #2 o #2); 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

375 
val blank = Scan.one (blank_token o #2 o #2); 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

376 
val newline = Scan.one (newline_token o #2 o #2); 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

377 
val before_cmd = 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

378 
Scan.option (newline  comments)  
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

379 
Scan.option (newline  comments)  
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

380 
Scan.option (blank  comments)  cmd; 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

381 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

382 
val span = 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

383 
Scan.repeat non_cmd  cmd  
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

384 
Scan.repeat (Scan.unless before_cmd non_cmd)  
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

385 
Scan.option (newline >> (single o #2)) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

386 
>> (fn (((toks1, (cmd, tok2)), toks3), tok4) => 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

387 
make_span (the cmd) (toks1 @ tok2 :: toks3 @ if_none tok4 [])); 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

388 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

389 
val spans = 
9140  390 
src 
391 
> Source.filter (not o T.is_semicolon) 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

392 
> Source.source' 0 T.stopper (Scan.error (Scan.bulk token)) NONE 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

393 
> Source.source stopper (Scan.error (Scan.bulk span)) NONE 
9140  394 
> Source.exhaust; 
395 
in 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

396 
if length trs = length spans then 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

397 
((NONE, []), NONE, true, Buffer.empty, (I, I)) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

398 
> Toplevel.present_excursion (trs ~~ map (present_span lex default_tags) spans) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

399 
> present_trailer 
11861  400 
else error "Messedup outer syntax for presentation" 
9140  401 
end; 
402 

403 
end; 

404 

405 

406 

407 
(** setup default output **) 

408 

409 
(* options *) 

410 

411 
val _ = add_options 

9220  412 
[("show_types", Library.setmp Syntax.show_types o boolean), 
413 
("show_sorts", Library.setmp Syntax.show_sorts o boolean), 

14707  414 
("show_structs", Library.setmp show_structs o boolean), 
15988  415 
("show_question_marks", Library.setmp show_question_marks o boolean), 
14696  416 
("long_names", Library.setmp NameSpace.long_names o boolean), 
16142  417 
("short_names", Library.setmp NameSpace.short_names o boolean), 
418 
("unique_names", Library.setmp NameSpace.unique_names o boolean), 

9220  419 
("eta_contract", Library.setmp Syntax.eta_contract o boolean), 
14899  420 
("locale", Library.setmp locale), 
9140  421 
("display", Library.setmp display o boolean), 
13929
21615e44ba88
Added "break" flag to allow line breaks within \isa{...}
berghofe
parents:
13775
diff
changeset

422 
("break", Library.setmp break o boolean), 
9140  423 
("quotes", Library.setmp quotes o boolean), 
424 
("mode", fn s => fn f => fn () => Library.setmp print_mode (s :: ! print_mode) f ()), 

9732  425 
("margin", Pretty.setmp_margin o integer), 
9750  426 
("indent", Library.setmp indent o integer), 
10321  427 
("source", Library.setmp source o boolean), 
428 
("goals_limit", Library.setmp goals_limit o integer)]; 

9140  429 

16002  430 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

431 
(* basic pretty printing *) 
9140  432 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

433 
val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src; 
14345  434 

11011
14b78c0c9f05
pretty_text: tweak_lines handles linebreaks gracefully;
wenzelm
parents:
10739
diff
changeset

435 
fun tweak_line s = 
14b78c0c9f05
pretty_text: tweak_lines handles linebreaks gracefully;
wenzelm
parents:
10739
diff
changeset

436 
if ! display then s else Symbol.strip_blanks s; 
9750  437 

11011
14b78c0c9f05
pretty_text: tweak_lines handles linebreaks gracefully;
wenzelm
parents:
10739
diff
changeset

438 
val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines; 
9140  439 

12055  440 
fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.extern_skolem ctxt; 
9140  441 

16002  442 
fun pretty_term_typ ctxt t = 
443 
(Syntax.const Syntax.constrainC $ 

444 
ProofContext.extern_skolem ctxt t $ 

445 
Syntax.term_of_typ (! show_sorts) (Term.fastype_of t)) 

446 
> ProofContext.pretty_term ctxt; 

15880
d6aa6c707acf
added antiquotations typeof, const, term_style, thm_style, term_type (something still to be done)
haftmann
parents:
15666
diff
changeset

447 

16002  448 
fun pretty_term_typeof ctxt = ProofContext.pretty_typ ctxt o Term.fastype_of; 
15880
d6aa6c707acf
added antiquotations typeof, const, term_style, thm_style, term_type (something still to be done)
haftmann
parents:
15666
diff
changeset

449 

16002  450 
fun pretty_term_const ctxt t = 
451 
if Term.is_Const t then pretty_term ctxt t 

452 
else error ("Logical constant expected: " ^ ProofContext.string_of_term ctxt t); 

15880
d6aa6c707acf
added antiquotations typeof, const, term_style, thm_style, term_type (something still to be done)
haftmann
parents:
15666
diff
changeset

453 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

454 
fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of; 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

455 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

456 
fun pretty_term_style ctxt (name, t) = 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

457 
pretty_term ctxt (TermStyle.the_style (ProofContext.theory_of ctxt) name ctxt t); 
9140  458 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

459 
fun pretty_thm_style ctxt (name, th) = 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

460 
pretty_term_style ctxt (name, Thm.full_prop_of th); 
15880
d6aa6c707acf
added antiquotations typeof, const, term_style, thm_style, term_type (something still to be done)
haftmann
parents:
15666
diff
changeset

461 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

462 
fun pretty_prf full ctxt thms = 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

463 
Pretty.chunks (map (ProofContext.pretty_proof_of ctxt full) thms); 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

464 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

465 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

466 
(* Isar output *) 
15880
d6aa6c707acf
added antiquotations typeof, const, term_style, thm_style, term_type (something still to be done)
haftmann
parents:
15666
diff
changeset

467 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

468 
fun output_list pretty src ctxt xs = 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

469 
map (pretty ctxt) xs (*always pretty in order to exhibit errors!*) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

470 
> (if ! source then K [pretty_text (str_of_source src)] else I) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

471 
> (if ! quotes then map Pretty.quote else I) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

472 
> (if ! display then 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

473 
map (Output.output o Pretty.string_of o Pretty.indent (! indent)) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

474 
#> space_implode "\\isasep\\isanewline%\n" 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

475 
#> enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}" 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

476 
else 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

477 
map (Output.output o (if ! break then Pretty.string_of else Pretty.str_of)) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

478 
#> space_implode "\\isasep\\isanewline%\n" 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

479 
#> enclose "\\isa{" "}"); 
11524
197f2e14a714
Added functions for printing primitive proof terms.
berghofe
parents:
11240
diff
changeset

480 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

481 
fun output pretty src ctxt = output_list pretty src ctxt o single; 
9732  482 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

483 
fun output_goals main_goal src state = args (Scan.succeed ()) (output (fn _ => fn _ => 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

484 
Pretty.chunks (Proof.pretty_goals main_goal (Toplevel.proof_of state 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

485 
handle Toplevel.UNDEF => error "No proof state")))) src state; 
14345  486 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

487 
fun output_ml src ctxt txt = 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

488 
(Context.use_mltext ("fn _ => (" ^ txt ^ ")") false (SOME (ProofContext.theory_of ctxt)); 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

489 
(if ! source then str_of_source src else txt) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

490 
> (if ! quotes then quote else I) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

491 
> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}" 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

492 
else 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

493 
split_lines 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

494 
#> map (space_implode "\\verb,," o map (enclose "\\verb" "") o space_explode "") 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

495 
#> space_implode "\\isasep\\isanewline%\n")); 
10360  496 

17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

497 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

498 
(* commands *) 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

499 

eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

500 
val _ = add_commands 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

501 
[("thm", args Attrib.local_thmss (output_list pretty_thm)), 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

502 
("thm_style", args (Scan.lift Args.liberal_name  Attrib.local_thm) (output pretty_thm_style)), 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

503 
("prop", args Args.local_prop (output pretty_term)), 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

504 
("term", args Args.local_term (output pretty_term)), 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

505 
("term_style", args (Scan.lift Args.liberal_name  Args.local_term) (output pretty_term_style)), 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

506 
("term_type", args Args.local_term (output pretty_term_typ)), 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

507 
("typeof", args Args.local_term (output pretty_term_typeof)), 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

508 
("const", args Args.local_term (output pretty_term_const)), 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

509 
("typ", args Args.local_typ_abbrev (output ProofContext.pretty_typ)), 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

510 
("text", args (Scan.lift Args.name) (output (K pretty_text))), 
10360  511 
("goals", output_goals true), 
14696  512 
("subgoals", output_goals false), 
17067
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

513 
("prf", args Attrib.local_thmss (output (pretty_prf false))), 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

514 
("full_prf", args Attrib.local_thmss (output (pretty_prf true))), 
eb07469a4cdd
reimplemented theory presentation, with support for tagged command regions;
wenzelm
parents:
17030
diff
changeset

515 
("ML", args (Scan.lift Args.name) output_ml)]; 
9140  516 

517 
end; 