src/Pure/General/name_space.ML
changeset 55956 94d384d621b0
parent 55923 4bdae9403baf
child 55957 cffb46aea3d1
equal deleted inserted replaced
55955:e8f1bf005661 55956:94d384d621b0
    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 ->
    58   val check_reports: Context.generic -> 'a table ->
    59     xstring * Position.T -> (string * Position.report list) * 'a
    59     xstring * Position.T list -> (string * Position.report list) * 'a
    60   val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a
    60   val check: Context.generic -> 'a table -> xstring * Position.T -> string * 'a
    61   val get: 'a table -> string -> 'a
    61   val get: 'a table -> string -> 'a
    62   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
    63   val empty_table: string -> 'a table
    63   val empty_table: string -> 'a table
    64   val merge_tables: 'a table * 'a table -> 'a table
    64   val merge_tables: 'a table * 'a table -> 'a table
   444 
   444 
   445 (* definition in symbol table *)
   445 (* definition in symbol table *)
   446 
   446 
   447 type 'a table = T * 'a Symtab.table;
   447 type 'a table = T * 'a Symtab.table;
   448 
   448 
   449 fun check_reports context (space, tab) (xname, pos) =
   449 fun check_reports context (space, tab) (xname, ps) =
   450   let val name = intern space xname in
   450   let val name = intern space xname in
   451     (case Symtab.lookup tab name of
   451     (case Symtab.lookup tab name of
   452       SOME x =>
   452       SOME x =>
   453         let
   453         let
   454           val reports =
   454           val reports =
   455             if Context_Position.is_reported_generic context pos
   455             filter (Context_Position.is_reported_generic context) ps
   456             then [(pos, markup space name)] else [];
   456             |> map (fn pos => (pos, markup space name));
   457         in ((name, reports), x) end
   457         in ((name, reports), x) end
   458     | NONE =>
   458     | NONE =>
   459         error (undefined (kind_of space) name ^ Position.here pos ^
   459         let
   460           Markup.markup Markup.report
   460           val completions = map (fn pos => completion context space (xname, pos)) ps;
   461             (Completion.reported_text (completion context space (xname, pos)))))
   461         in
       
   462           error (undefined (kind_of space) name ^ Position.here_list ps ^
       
   463             implode (map (Markup.markup_report o Completion.reported_text) completions))
       
   464         end)
   462   end;
   465   end;
   463 
   466 
   464 fun check context table arg =
   467 fun check context table (xname, pos) =
   465   let
   468   let
   466     val ((name, reports), x) = check_reports context table arg;
   469     val ((name, reports), x) = check_reports context table (xname, [pos]);
   467     val _ = Position.reports reports;
   470     val _ = Position.reports reports;
   468   in (name, x) end;
   471   in (name, x) end;
   469 
   472 
   470 fun get (space, tab) name =
   473 fun get (space, tab) name =
   471   (case Symtab.lookup tab name of
   474   (case Symtab.lookup tab name of