--- a/src/Pure/ML/ml_env.ML Mon Jun 01 15:26:00 2009 +0200
+++ b/src/Pure/ML/ml_env.ML Mon Jun 01 16:12:42 2009 +0200
@@ -1,12 +1,15 @@
(* Title: Pure/ML/ml_env.ML
Author: Makarius
-Local environment of ML results.
+Local environment of ML sources and results.
*)
signature ML_ENV =
sig
val inherit: Context.generic -> Context.generic -> Context.generic
+ val register_tokens: ML_Lex.token list -> Context.generic ->
+ (serial * ML_Lex.token) list * Context.generic
+ val token_position: Proof.context -> serial -> Position.T option
val name_space: ML_Name_Space.T
val local_context: use_context
end
@@ -14,46 +17,67 @@
structure ML_Env: ML_ENV =
struct
+(* context data *)
+
structure Env = GenericDataFun
(
type T =
- ML_Name_Space.valueVal Symtab.table *
- ML_Name_Space.typeVal Symtab.table *
- ML_Name_Space.fixityVal Symtab.table *
- ML_Name_Space.structureVal Symtab.table *
- ML_Name_Space.signatureVal Symtab.table *
- ML_Name_Space.functorVal Symtab.table;
- val empty = (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty);
+ Position.T Inttab.table *
+ (ML_Name_Space.valueVal Symtab.table *
+ ML_Name_Space.typeVal Symtab.table *
+ ML_Name_Space.fixityVal Symtab.table *
+ ML_Name_Space.structureVal Symtab.table *
+ ML_Name_Space.signatureVal Symtab.table *
+ ML_Name_Space.functorVal Symtab.table);
+ val empty =
+ (Inttab.empty,
+ (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty));
val extend = I;
fun merge _
- ((val1, type1, fixity1, structure1, signature1, functor1),
- (val2, type2, fixity2, structure2, signature2, functor2)) : T =
- (Symtab.merge (K true) (val1, val2),
- Symtab.merge (K true) (type1, type2),
- Symtab.merge (K true) (fixity1, fixity2),
- Symtab.merge (K true) (structure1, structure2),
- Symtab.merge (K true) (signature1, signature2),
- Symtab.merge (K true) (functor1, functor2));
+ ((toks1, (val1, type1, fixity1, structure1, signature1, functor1)),
+ (toks2, (val2, type2, fixity2, structure2, signature2, functor2))) : T =
+ (Inttab.merge (K true) (toks1, toks2),
+ (Symtab.merge (K true) (val1, val2),
+ Symtab.merge (K true) (type1, type2),
+ Symtab.merge (K true) (fixity1, fixity2),
+ Symtab.merge (K true) (structure1, structure2),
+ Symtab.merge (K true) (signature1, signature2),
+ Symtab.merge (K true) (functor1, functor2)));
);
val inherit = Env.put o Env.get;
+
+(* source tokens *)
+
+fun register_tokens toks context =
+ let
+ val regs = map (fn tok => (serial (), tok)) toks;
+ val context' = context
+ |> Env.map (apfst (fold (fn (i, tok) => Inttab.update (i, ML_Lex.pos_of tok)) regs));
+ in (regs, context') end;
+
+val token_position = Inttab.lookup o #1 o Env.get o Context.Proof;
+
+
+(* results *)
+
val name_space: ML_Name_Space.T =
let
fun lookup sel1 sel2 name =
Context.thread_data ()
- |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (Env.get context)) name)
+ |> (fn NONE => NONE | SOME context => Symtab.lookup (sel1 (#2 (Env.get context))) name)
|> (fn NONE => sel2 ML_Name_Space.global name | some => some);
fun all sel1 sel2 () =
Context.thread_data ()
- |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (Env.get context)))
+ |> (fn NONE => [] | SOME context => Symtab.dest (sel1 (#2 (Env.get context))))
|> append (sel2 ML_Name_Space.global ())
|> sort_distinct (string_ord o pairself #1);
fun enter ap1 sel2 entry =
if is_some (Context.thread_data ()) then
- Context.>> (Env.map (ap1 (Symtab.update entry)))
+ Context.>> (Env.map (apsnd (ap1 (Symtab.update entry))))
else sel2 ML_Name_Space.global entry;
in
{lookupVal = lookup #1 #lookupVal,
--- a/src/Pure/ML/ml_test.ML Mon Jun 01 15:26:00 2009 +0200
+++ b/src/Pure/ML/ml_test.ML Mon Jun 01 16:12:42 2009 +0200
@@ -1,7 +1,7 @@
(* Title: Pure/ML/ml_test.ML
Author: Makarius
-Test of advanced ML compiler invocation in Poly/ML 5.3 (SVN 744).
+Test of advanced ML compiler invocation in Poly/ML 5.3 (SVN 762).
*)
signature ML_TEST =
@@ -15,28 +15,9 @@
(* extra ML environment *)
-structure Extra_Env = GenericDataFun
-(
- type T = Position.T Inttab.table; (*position of registered tokens*)
- val empty = Inttab.empty;
- val extend = I;
- fun merge _ = Inttab.merge (K true);
-);
-
-fun inherit_env context =
- ML_Env.inherit context #>
- Extra_Env.put (Extra_Env.get context);
-
-fun register_tokens toks context =
- let
- val regs = map (fn tok => (serial (), tok)) toks;
- val context' = context
- |> Extra_Env.map (fold (fn (i, tok) => Inttab.update (i, ML_Lex.pos_of tok)) regs);
- in (regs, context') end;
-
fun position_of ctxt
({file, startLine = line, startPosition = i, endPosition = j, ...}: PolyML.location) =
- (case pairself (Inttab.lookup (Extra_Env.get (Context.Proof ctxt))) (i, j) of
+ (case pairself (ML_Env.token_position ctxt) (i, j) of
(SOME pos1, SOME pos2) => Position.encode_range (pos1, pos2)
| (SOME pos, NONE) => pos
| _ => Position.line_file line file);
@@ -67,7 +48,7 @@
let
(* input *)
- val input = Context.>>> (register_tokens toks);
+ val input = Context.>>> (ML_Env.register_tokens toks);
val input_buffer = ref (map (apsnd (String.explode o ML_Lex.text_of)) input);
val current_line = ref (the_default 1 (Position.line_of pos));
@@ -168,7 +149,7 @@
val _ = Context.setmp_thread_data env_ctxt
(fn () => (eval false Position.none env; Context.thread_data ())) ()
- |> (fn NONE => () | SOME context' => Context.>> (inherit_env context'));
+ |> (fn NONE => () | SOME context' => Context.>> (ML_Env.inherit context'));
val _ = eval true pos body;
val _ = eval false Position.none (ML_Lex.tokenize "structure Isabelle = struct end");
in () end;
@@ -177,7 +158,7 @@
local structure P = OuterParse and K = OuterKeyword in
fun propagate_env (context as Context.Proof lthy) =
- Context.Proof (LocalTheory.map_contexts (inherit_env context) lthy)
+ Context.Proof (LocalTheory.map_contexts (ML_Env.inherit context) lthy)
| propagate_env context = context;
val _ =