equal
deleted
inserted
replaced
7 signature ML_ENV = |
7 signature ML_ENV = |
8 sig |
8 sig |
9 val inherit: Context.generic -> Context.generic -> Context.generic |
9 val inherit: Context.generic -> Context.generic -> Context.generic |
10 val register_tokens: ML_Lex.token list -> Context.generic -> |
10 val register_tokens: ML_Lex.token list -> Context.generic -> |
11 (serial * ML_Lex.token) list * Context.generic |
11 (serial * ML_Lex.token) list * Context.generic |
12 val token_position: Proof.context -> serial -> Position.T option |
12 val token_position: Context.generic -> serial -> Position.T option |
13 val name_space: ML_Name_Space.T |
13 val name_space: ML_Name_Space.T |
14 val local_context: use_context |
14 val local_context: use_context |
15 end |
15 end |
16 |
16 |
17 structure ML_Env: ML_ENV = |
17 structure ML_Env: ML_ENV = |
55 val regs = map (fn tok => (serial (), tok)) toks; |
55 val regs = map (fn tok => (serial (), tok)) toks; |
56 val context' = context |
56 val context' = context |
57 |> Env.map (apfst (fold (fn (i, tok) => Inttab.update (i, ML_Lex.pos_of tok)) regs)); |
57 |> Env.map (apfst (fold (fn (i, tok) => Inttab.update (i, ML_Lex.pos_of tok)) regs)); |
58 in (regs, context') end; |
58 in (regs, context') end; |
59 |
59 |
60 val token_position = Inttab.lookup o #1 o Env.get o Context.Proof; |
60 val token_position = Inttab.lookup o #1 o Env.get; |
61 |
61 |
62 |
62 |
63 (* results *) |
63 (* results *) |
64 |
64 |
65 val name_space: ML_Name_Space.T = |
65 val name_space: ML_Name_Space.T = |