blob: 0dd41e4256b283025036721818b00e70c8c58242 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
(* See http://proofgeneral.inf.ed.ac.uk/trac/ticket/274 *)
theory BigErrors imports Pure
begin
consts foo :: 'a
consts bar :: 'a
ML {* warning (cat_lines (replicate 300 "This is a big warning message")); *}
(* Attempt to get a big error with "error" fails, but we can use printing function
(see FaultyErrors.thy) *)
ML {* Output.error_msg (cat_lines (replicate 10000 "This is a big error message")); *}
(* Note about FaultyErrors: the above generates an error
interactively but does *not* generate an error when
required by another theory, see, BigErrorsNested *)
end
|
