equal
deleted
inserted
replaced
445 type 'a table = T * 'a Symtab.table; |
445 type 'a table = T * 'a Symtab.table; |
446 |
446 |
447 fun check context (space, tab) (xname, pos) = |
447 fun check context (space, tab) (xname, pos) = |
448 let val name = intern space xname in |
448 let val name = intern space xname in |
449 (case Symtab.lookup tab name of |
449 (case Symtab.lookup tab name of |
450 SOME x => (Context_Position.report_generic context pos (markup space name); (name, x)) |
450 SOME x => |
|
451 (Context_Position.report_generic context pos (markup space name); |
|
452 (name, x)) |
451 | NONE => |
453 | NONE => |
452 (Completion.report (completion context space (xname, pos)); |
454 (Completion.report (completion context space (xname, pos)); |
453 error (undefined (kind_of space) name ^ Position.here pos))) |
455 error (undefined (kind_of space) name ^ Position.here pos))) |
454 end; |
456 end; |
455 |
457 |