blob: 4afd7120b450c7b941d51e5820df05727bf864fb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
(* Testing different kinds of markup in Isabelle output *)
(* ordinary output between prompts *)
print "ordinary";
print "ordinary\n"; (* final newline no difference *)
(* eager annotation: displayed as soon as it's seen *)
writeln "eager to be seen!";
print "more ordinary\n";
Goal "P-->P";
(* C-c RET to here should show eager annotation, as well as
updating goals buffer properly. *)
error "something went wrong";
|
