src/Pure/ML/ml_context.ML
changeset 59067 dd8ec9138112
parent 59064 a8bcb5a446c8
child 59112 e670969f34df
--- a/src/Pure/ML/ml_context.ML	Sun Nov 30 13:15:04 2014 +0100
+++ b/src/Pure/ML/ml_context.ML	Sun Nov 30 14:02:48 2014 +0100
@@ -170,7 +170,7 @@
 
 fun eval_file flags path =
   let val pos = Path.position path
-  in eval flags pos (ML_Lex.read pos (File.read path)) end;
+  in eval flags pos (ML_Lex.read_pos pos (File.read path)) end;
 
 fun eval_source flags source =
   eval flags (Input.pos_of source) (ML_Lex.read_source (#SML flags) source);
@@ -184,16 +184,11 @@
     (fn () => eval_source flags source) ();
 
 fun expression range name constraint body ants =
-  let
-    val hidden = ML_Lex.read Position.none;
-    val visible = ML_Lex.read_set_range range;
-  in
-    exec (fn () =>
-      eval ML_Compiler.flags (#1 range)
-       (hidden "Context.set_thread_data (SOME (let val " @ visible name @
-        hidden (": " ^ constraint ^ " =") @ ants @
-        hidden ("in " ^ body ^ " end (ML_Context.the_generic_context ())));")))
-  end;
+  exec (fn () =>
+    eval ML_Compiler.flags (#1 range)
+     (ML_Lex.read "Context.set_thread_data (SOME (let val " @ ML_Lex.read_set_range range name @
+      ML_Lex.read (": " ^ constraint ^ " =") @ ants @
+      ML_Lex.read ("in " ^ body ^ " end (ML_Context.the_generic_context ())));")));
 
 end;