--- a/src/Pure/Isar/outer_syntax.ML Thu Apr 17 11:40:00 2008 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Thu Apr 17 16:30:45 2008 +0200
@@ -43,12 +43,12 @@
(* diagnostics *)
fun report_keyword name =
- Pretty.markup (Markup.keyword_decl name)
- [Pretty.str ("Outer syntax keyword: " ^ quote name)];
+ Pretty.mark (Markup.keyword_decl name)
+ (Pretty.str ("Outer syntax keyword: " ^ quote name));
fun report_command name kind =
- Pretty.markup (Markup.command_decl name kind)
- [Pretty.str ("Outer syntax command: " ^ quote name ^ " (" ^ kind ^ ")")];
+ Pretty.mark (Markup.command_decl name kind)
+ (Pretty.str ("Outer syntax command: " ^ quote name ^ " (" ^ kind ^ ")"));
(* parsers *)
--- a/src/Pure/codegen.ML Thu Apr 17 11:40:00 2008 +0200
+++ b/src/Pure/codegen.ML Thu Apr 17 16:30:45 2008 +0200
@@ -1018,7 +1018,7 @@
NONE => state
| SOME NONE => state
| SOME cex => Proof.goal_message (fn () => Pretty.chunks [Pretty.str "",
- Pretty.markup Markup.hilite [pretty_counterex ctxt cex]]) state
+ Pretty.mark Markup.hilite (pretty_counterex ctxt cex)]) state
end handle TimeLimit.TimeOut => (warning "Auto quickcheck: timeout."; state);
in
if int andalso !auto_quickcheck andalso not (!Toplevel.quiet)