src/Pure/General/name_space.ML
changeset 55922 710bc66f432c
parent 55845 a05413276a0d
child 55923 4bdae9403baf
equal deleted inserted replaced
55921:22e9fc998d65 55922:710bc66f432c
    53   val alias: naming -> binding -> string -> T -> T
    53   val alias: naming -> binding -> string -> T -> T
    54   val naming_of: Context.generic -> naming
    54   val naming_of: Context.generic -> naming
    55   val map_naming: (naming -> naming) -> Context.generic -> Context.generic
    55   val map_naming: (naming -> naming) -> Context.generic -> Context.generic
    56   val declare: Context.generic -> bool -> binding -> T -> string * T
    56   val declare: Context.generic -> bool -> binding -> T -> string * T
    57   type 'a table = T * 'a Symtab.table
    57   type 'a table = T * 'a Symtab.table
       
    58   val check_reports: Context.generic -> 'a table ->
       
    59     xstring * Position.T -> (string * Position.report list) * 'a
    58   val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a
    60   val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a
    59   val get: 'a table -> string -> 'a
    61   val get: 'a table -> string -> 'a
    60   val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table
    62   val define: Context.generic -> bool -> binding * 'a -> 'a table -> string * 'a table
    61   val empty_table: string -> 'a table
    63   val empty_table: string -> 'a table
    62   val merge_tables: 'a table * 'a table -> 'a table
    64   val merge_tables: 'a table * 'a table -> 'a table
   443 
   445 
   444 (* definition in symbol table *)
   446 (* definition in symbol table *)
   445 
   447 
   446 type 'a table = T * 'a Symtab.table;
   448 type 'a table = T * 'a Symtab.table;
   447 
   449 
   448 fun check context (space, tab) (xname, pos) =
   450 fun check_reports context (space, tab) (xname, pos) =
   449   let val name = intern space xname in
   451   let val name = intern space xname in
   450     (case Symtab.lookup tab name of
   452     (case Symtab.lookup tab name of
   451       SOME x =>
   453       SOME x =>
   452        (Context_Position.report_generic context pos (markup space name);
   454         let
   453         (name, x))
   455           val reports =
       
   456             if Context_Position.is_visible_generic context andalso Position.is_reported pos
       
   457             then [(pos, markup space name)] else [];
       
   458         in ((name, reports), x) end
   454     | NONE =>
   459     | NONE =>
   455         error (undefined (kind_of space) name ^ Position.here pos ^
   460         error (undefined (kind_of space) name ^ Position.here pos ^
   456           Markup.markup Markup.report
   461           Markup.markup Markup.report
   457             (Completion.reported_text (completion context space (xname, pos)))))
   462             (Completion.reported_text (completion context space (xname, pos)))))
   458   end;
   463   end;
   459 
   464 
       
   465 fun check context table arg =
       
   466   let
       
   467     val ((name, reports), x) = check_reports context table arg;
       
   468     val _ = Position.reports reports;
       
   469   in (name, x) end;
       
   470 
   460 fun get (space, tab) name =
   471 fun get (space, tab) name =
   461   (case Symtab.lookup tab name of
   472   (case Symtab.lookup tab name of
   462     SOME x => x
   473     SOME x => x
   463   | NONE => error (undefined (kind_of space) name));
   474   | NONE => error (undefined (kind_of space) name));
   464 
   475