improved error handling for document antiquotations;
authorwenzelm
Fri Mar 06 21:49:58 2009 +0100 (2009-03-06)
changeset 30317159bab53b40d
parent 30316 379d6f06cdb2
child 30318 3d03190d2864
child 30322 90e309d20d58
improved error handling for document antiquotations;
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Thy/thy_output.ML	Fri Mar 06 19:38:03 2009 +0100
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Mar 06 21:49:58 2009 +0100
     1.3 @@ -78,8 +78,12 @@
     1.4  fun command src =
     1.5    let val ((name, _), pos) = Args.dest_src src in
     1.6      (case Symtab.lookup (! global_commands) name of
     1.7 -      NONE => error ("Unknown document antiquotation command: " ^ quote name ^ Position.str_of pos)
     1.8 -    | SOME f => (Position.report (Markup.doc_antiq name) pos; f src))
     1.9 +      NONE => error ("Unknown document antiquotation: " ^ quote name ^ Position.str_of pos)
    1.10 +    | SOME f =>
    1.11 +       (Position.report (Markup.doc_antiq name) pos;
    1.12 +        (fn node => f src node handle ERROR msg =>
    1.13 +          cat_error msg ("The error(s) above occurred in document antiquotation: " ^
    1.14 +            quote name ^ Position.str_of pos))))
    1.15    end;
    1.16  
    1.17  fun option (name, s) f () =