maintain position of formal entities via name space;
authorwenzelm
Sat Oct 24 21:30:33 2009 +0200 (2009-10-24)
changeset 330979d501e11084a
parent 33096 db3c18fd9708
child 33103 9d7d0bef2a77
maintain position of formal entities via name space;
src/Pure/General/name_space.ML
src/Pure/General/position.ML
src/Pure/consts.ML
src/Pure/sign.ML
src/Pure/type.ML
     1.1 --- a/src/Pure/General/name_space.ML	Sat Oct 24 20:54:08 2009 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Sat Oct 24 21:30:33 2009 +0200
     1.3 @@ -42,8 +42,8 @@
     1.4    val define: bool -> naming -> binding * 'a -> 'a table -> string * 'a table
     1.5    val empty_table: string -> 'a table
     1.6    val merge_tables: 'a table * 'a table -> 'a table
     1.7 -  val join_tables:
     1.8 -    (string -> 'a * 'a -> 'a) (*Symtab.SAME*) -> 'a table * 'a table -> 'a table
     1.9 +  val join_tables: (string -> 'a * 'a -> 'a) (*Symtab.SAME*) ->
    1.10 +    'a table * 'a table -> 'a table
    1.11    val dest_table: 'a table -> (string * 'a) list
    1.12    val extern_table: 'a table -> (xstring * 'a) list
    1.13  end;
    1.14 @@ -282,7 +282,7 @@
    1.15      val entry =
    1.16       {externals = accs',
    1.17        is_system = false,
    1.18 -      pos = Binding.pos_of binding,
    1.19 +      pos = Position.default (Binding.pos_of binding),
    1.20        id = serial ()};
    1.21      val space' = space |> fold (add_name name) accs |> new_entry strict (name, entry);
    1.22    in (name, space') end;
     2.1 --- a/src/Pure/General/position.ML	Sat Oct 24 20:54:08 2009 +0200
     2.2 +++ b/src/Pure/General/position.ML	Sat Oct 24 21:30:33 2009 +0200
     2.3 @@ -37,6 +37,7 @@
     2.4    val range: T -> T -> range
     2.5    val thread_data: unit -> T
     2.6    val setmp_thread_data: T -> ('a -> 'b) -> 'a -> 'b
     2.7 +  val default: T -> T
     2.8  end;
     2.9  
    2.10  structure Position: POSITION =
    2.11 @@ -178,4 +179,8 @@
    2.12  
    2.13  end;
    2.14  
    2.15 +fun default pos =
    2.16 +  if pos = none then thread_data ()
    2.17 +  else pos;
    2.18 +
    2.19  end;
     3.1 --- a/src/Pure/consts.ML	Sat Oct 24 20:54:08 2009 +0200
     3.2 +++ b/src/Pure/consts.ML	Sat Oct 24 21:30:33 2009 +0200
     3.3 @@ -232,8 +232,7 @@
     3.4  fun declare authentic naming tags (b, declT) =
     3.5    map_consts (fn (decls, constraints, rev_abbrevs) =>
     3.6      let
     3.7 -      val tags' = tags |> Position.default_properties (Position.thread_data ());
     3.8 -      val decl = {T = declT, typargs = typargs_of declT, tags = tags', authentic = authentic};
     3.9 +      val decl = {T = declT, typargs = typargs_of declT, tags = tags, authentic = authentic};
    3.10        val (_, decls') = decls |> Name_Space.define true naming (b, (decl, NONE));
    3.11      in (decls', constraints, rev_abbrevs) end);
    3.12  
    3.13 @@ -284,8 +283,7 @@
    3.14    in
    3.15      consts |> map_consts (fn (decls, constraints, rev_abbrevs) =>
    3.16        let
    3.17 -        val tags' = tags |> Position.default_properties (Position.thread_data ());
    3.18 -        val decl = {T = T, typargs = typargs_of T, tags = tags', authentic = true};
    3.19 +        val decl = {T = T, typargs = typargs_of T, tags = tags, authentic = true};
    3.20          val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand};
    3.21          val (_, decls') = decls
    3.22            |> Name_Space.define true naming (b, (decl, SOME abbr));
     4.1 --- a/src/Pure/sign.ML	Sat Oct 24 20:54:08 2009 +0200
     4.2 +++ b/src/Pure/sign.ML	Sat Oct 24 21:30:33 2009 +0200
     4.3 @@ -526,8 +526,7 @@
     4.4  fun declare_const tags ((b, T), mx) thy =
     4.5    let
     4.6      val pos = Binding.pos_of b;
     4.7 -    val tags' = Position.default_properties pos tags;
     4.8 -    val ([const as Const (c, _)], thy') = gen_add_consts (K I) true tags' [(b, T, mx)] thy;
     4.9 +    val ([const as Const (c, _)], thy') = gen_add_consts (K I) true tags [(b, T, mx)] thy;
    4.10      val _ = Position.report (Markup.const_decl c) pos;
    4.11    in (const, thy') end;
    4.12  
     5.1 --- a/src/Pure/type.ML	Sat Oct 24 20:54:08 2009 +0200
     5.2 +++ b/src/Pure/type.ML	Sat Oct 24 21:30:33 2009 +0200
     5.3 @@ -556,10 +556,7 @@
     5.4  local
     5.5  
     5.6  fun new_decl naming tags (c, decl) types =
     5.7 -  let
     5.8 -    val tags' = tags |> Position.default_properties (Position.thread_data ());
     5.9 -    val (_, types') = Name_Space.define true naming (c, (decl, tags')) types;
    5.10 -  in types' end;
    5.11 +  #2 (Name_Space.define true naming (c, (decl, tags)) types);
    5.12  
    5.13  fun map_types f = map_tsig (fn (classes, default, types) =>
    5.14    let