# HG changeset patch # User wenzelm # Date 1217974222 -7200 # Node ID 22c32eb18c23c2ddd62f0ffd82f85897c0619023 # Parent 7f5fb39c63628eef484361bb684f05b1fa6ebb34 report markup; diff -r 7f5fb39c6362 -r 22c32eb18c23 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Wed Aug 06 00:10:18 2008 +0200 +++ b/src/Pure/Isar/attrib.ML Wed Aug 06 00:10:22 2008 +0200 @@ -99,7 +99,7 @@ let val ((name, _), pos) = Args.dest_src src in (case Symtab.lookup attrs name of NONE => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos) - | SOME ((att, _), _) => att src) + | SOME ((att, _), _) => (Position.report (Markup.attribute name) pos; att src)) end; in attr end; diff -r 7f5fb39c6362 -r 22c32eb18c23 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Wed Aug 06 00:10:18 2008 +0200 +++ b/src/Pure/Isar/method.ML Wed Aug 06 00:10:22 2008 +0200 @@ -437,7 +437,7 @@ let val ((name, _), pos) = Args.dest_src src in (case Symtab.lookup meths name of NONE => error ("Unknown proof method: " ^ quote name ^ Position.str_of pos) - | SOME ((mth, _), _) => mth src) + | SOME ((mth, _), _) => (Position.report (Markup.method name) pos; mth src)) end; in meth end;