# HG changeset patch # User wenzelm # Date 1236372598 -3600 # Node ID 159bab53b40d9dd6ac892e0ea5345e8b8ef894a5 # Parent 379d6f06cdb2ec78b1d22129e2363dc8cf9e3a98 improved error handling for document antiquotations; diff -r 379d6f06cdb2 -r 159bab53b40d src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Fri Mar 06 19:38:03 2009 +0100 +++ b/src/Pure/Thy/thy_output.ML Fri Mar 06 21:49:58 2009 +0100 @@ -78,8 +78,12 @@ fun command src = let val ((name, _), pos) = Args.dest_src src in (case Symtab.lookup (! global_commands) name of - NONE => error ("Unknown document antiquotation command: " ^ quote name ^ Position.str_of pos) - | SOME f => (Position.report (Markup.doc_antiq name) pos; f src)) + NONE => error ("Unknown document antiquotation: " ^ quote name ^ Position.str_of pos) + | SOME f => + (Position.report (Markup.doc_antiq name) pos; + (fn node => f src node handle ERROR msg => + cat_error msg ("The error(s) above occurred in document antiquotation: " ^ + quote name ^ Position.str_of pos)))) end; fun option (name, s) f () =